This paper proposes Proteus, a protocol state machine, property-guided, and budget-aware automated testing approach for discovering logical vulnerabilities in wireless protocol implementations. Proteus maintains its budget awareness by generating test cases (i.e., each being a sequence of protocol messages) that are not only meaningful (i.e., the test case mostly follows the desirable protocol flow except for some controlled deviations) but also have a high probability of violating the desirable properties. To demonstrate its effectiveness, we evaluated Proteus in two different protocol implementations, namely 4G LTE and BLE, across 23 consumer devices (11 for 4G LTE and 12 for BLE). Proteus discovered 25 unique issues, including 112 instances. Affected vendors have positively acknowledged 14 vulnerabilities through 5 CVEs.

翻译：本文提出Proteus，一种面向协议状态机、属性引导且预算感知的自动化测试方法，用于发现无线协议实现中的逻辑漏洞。Proteus通过生成测试用例（即每条用例均为协议消息序列）来保持预算感知，这些测试用例不仅具有意义（即除部分受控偏离外，测试用例主要遵循期望的协议流程），而且具有较高的违反期望属性的概率。为验证其有效性，我们在两种不同的协议实现（即4G LTE和BLE）中对Proteus进行了评估，测试覆盖23款消费设备（11款用于4G LTE，12款用于BLE）。Proteus共发现25个独立问题，包含112个具体实例。受影响的厂商已通过5个CVE编号确认了其中14个漏洞。