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.

We present SymRustC, a hybrid fuzzer for Rust. SymRustC is hybrid in the sense that it combines fuzzing and concolic execution. SymRustC leverages an existing tool called SymCC for its concolic execution capability and another existing tool called LibAFL for its fuzzing capability. Since SymCC instruments LLVM IR (Intermediate Representation) for concolic execution and the Rust compiler uses LLVM as a backend, we integrate SymCC with the Rust compiler to instrument Rust programs for concolic execution. LibAFL provides a framework to develop a fuzzer, and we use it to develop a hybrid fuzzer that combines fuzzing and our concolic execution. We discuss our implementation as well as four case studies to demonstrate that SymRustC can generate inputs that discover errors in Rust programs.