HardaBLE: Hardening BLE against software compromise

Bluetooth Low Energy (BLE) is a ubiquitous wireless technology used by billions of devices and defined in an open standard. The BLE specification defines two security protocols: pairing, which establishes a trust relationship between two devices by deriving the Long-Term Key (LTK), and session establishment, which generates a fresh encryption key for each (re)connection. The BLE security model and prior research primarily consider wireless-only adversaries. However, real deployments increasingly face software compromise, where an attacker exploits a vulnerability to gain arbitrary code execution or memory read/write capabilities on the device. Under such a compromise, an attacker can extract the LTK and use it to impersonate trusted devices or decrypt/forge protected traffic.

To address the gap between BLE's wireless-only assumptions and practical system security, we present HardaBLE, a hardened BLE architecture designed to protect keys and prevent their use under software compromise. HardaBLE confines LTK storage and LTK-dependent cryptographic operations to a hardware-isolated secure environment, preventing key exfiltration. Furthermore, it enforces integrity-bound authorization by denying LTK-dependent operations if the secure environment cannot verify firmware integrity evidence against a stored reference. We formally model HardaBLE in TLA+ and verify it with TLC, demonstrating that our design prevents key exfiltration and denies key-dependent operations when firmware integrity evidence is invalid.

We implement HardaBLE by modifying the Zephyr BLE stack, and we evaluate it on nRF53 development boards. We also empirically validate our prototype under simulated software compromise, showing that it does not expose keys in plaintext and denies key-dependent operations when firmware integrity evidence verification fails. Our performance evaluation shows that hardware-isolated key handling adds negligible latency and energy overhead. Enabling integrity verification increases session establishment time by up to 18% and approximately doubles the per-reconnection charge-draw. However, the absolute overhead remains under 0.3 microampere-hours (µAh), making HardaBLE still practical for common BLE workloads with infrequent reconnections.