An Automated and Principled Security Analysis Framework for Bluetooth LE Implementations
Primary Investigator:
Elisa Bertino
Syed Rafiul Hussain (Purdue Univ.), Victoria C. Moore (Intel Corporation), Elisa Bertino* (Purdue Univ.)
Abstract
Recent proximity-based communication protocols (e.g., Bluetooth Low Energy (BLE)) make it easy for two mobile devices to communicate with each other. Recently, many IoT systems (e.g., smart bulbs) rely on the BLE protocol for secure communications with the IoT gateways, e.g., a smart bulb system authenticating itself to the dedicated smart home hub. However, vulnerabilities in the BLE protocol implementation can be exploited by the attackers to disrupt secure communication. It is, therefore, critical to ensure that the existing BLE implementations (e.g., Bluedroid, BlueZ, and so on) are free from exploitable bugs. Bugs in the implementations can be due to four main reasons: (1) BLE packets are not correctly parsed and processed by implementations; (2) Implementations deviate from the Bluetooth standard specification and hence contain functional or semantic bugs (e.g., carrying out a wrong action); (3) Implementations have memory errors; (4) Cryptographic building blocks used in the protocol are prone to existing attacks. In this work, we develop a highly automated security evaluation framework that leverages techniques from formal verification (e.g., model checking) and software engineering (e.g., program analysis) to detect the first two types of bugs mentioned above. Our analysis framework will assume that the underlying cryptographic primitives have been implemented and used properly.