Formalization, Implementation, and Verification of the Bluetooth L2CAP State Machine

摘要

The Logical Link Control and Adaptation Protocol (L2CAP) is a core Bluetooth component, and verifying its correctness is crucial for reliable and secure connectivity. However, verification can be challenging due to the complexity and ambiguities in its natural language (English) specification. In this paper, we present a formally verified implementation of the L2CAP state machine. Our approach introduces the Specification State Machine (SSM) to formalize the L2CAP state machine in the specification and the Operational State Machine (OSM) as an abstraction of the implementation. We then formally prove that (i) OSM refines SSM, and (ii) our implementation semantically conforms to OSM. By combining these two proofs, we verify that our implementation complies with our formalization of the specification. Furthermore, we define critical safety and liveness properties and formally prove that our implementation satisfies these guarantees. To ensure practicality, we implement the L2CAP state machine in Dafny and integrate it into Android's Fluoride Bluetooth stack. Our evaluation demonstrates that our formally verified implementation maintains competitive performance while ensuring formal correctness.