This research aims to deliver a comprehensive assessment of the fundamental security and privacy challenges and design flaws in BLE, providing novel formal models and techniques to systematically identify vulnerabilities and strengthen security and privacy assurance for stakeholders, including BLE manufacturers. We plan to collaborate closely with the Bluetooth Special Interest Group (SIG), keeping them informed of new threats and countermeasures.

Our ultimate goal is to develop mathematically grounded formal analysis methods that guarantee the safe and secure operation of Bluetooth IoT devices and support automated vulnerability discovery of protocol-level flaws in Bluetooth with integration into Bluetooth life cycle management and beyond. By addressing these issues, we strive to enhance the security and privacy of BLE technology, not only in the civilian use cases, but also in the government and military sectors.