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.

In Voice Assistant (VA) platforms, when users add devices to their accounts and give voice commands, complex interactions occur between the devices, skills, VA clouds, and vendor clouds. These interactions are governed by the device management capabilities (DMC) of VA platforms, which rely on device names, types, and associated skills in the user account. Prior work studied vulnerabilities in specific VA components, such as hidden voice commands and bypassing skill vetting. However, the security and privacy implications of device management flaws have largely been unexplored. In this paper, we introduce DMC-Xplorer, a testing framework for the automated discovery of VA device management flaws. We first introduce VA description language (VDL), a new domain-specific language to create VA environments for testing, using VA and skill developer APIs. DMC-Xplorer then selects VA parameters (device names, types, vendors, actions, and skills) in a combinatorial approach and creates VA environments with VDL. It issues real voice commands to the environment via developer APIs and logs event traces. It validates the traces against three formal security properties that define the secure operation of VA platforms. Lastly, DMC-Xplorer identifies the root cause of property violations through intervention analysis to identify VA device management flaws. We exercised DMC-Xplorer on Amazon Alexa and Google Home and discovered two design flaws that can be exploited to launch four attacks. We show that malicious skills with default permissions can eavesdrop on privacy-sensitive device states, prevent users from controlling their devices, and disrupt the services on the VA cloud.

Named after the Viking King Harald Bluetooth, Bluetooth is the de facto standard for short-range wireless communications. The introduction of Bluetooth Low Energy (BLE) and Mesh protocols has further paved the way for its domination in the era of IoT and 5G. Meanwhile, attacks against Bluetooth, such as BlueBorne, BleedingBit, KNOB, BIAS, and BLESA, have been booming in the past fewyears, impacting billions of devices. While Bluetooth security has drawn significant attention from the security research community, a systematic understanding of this field is still missing, impeding the advancement of this field.In this paper, we first summarize the evolution of Bluetooth security in the specification in the past 24 years. Then, we provide a systematization of Bluetooth security by diving into 76 attacks and 33 defenses presented by previous research in this area. We first categorize attacks and defenses based on their affected layers and protocols in the Bluetooth stack as well as their threat models. Then, we cross-check the attacks and defenses to have a big picture of Bluetooth security. Based on the systematization, we find that the existing formal analyses of Bluetooth do not cover most of the security aspects of Bluetooth Mesh. Lastly, we take a step towards securing Bluetooth Mesh by designing and implementing a comprehensive formal model of Bluetooth Mesh covering all its security-related protocols. Our systematization reveals, for instance, that the security of Bluetooth pairing faces challenges caused by users’ mistakes, and that Bluetooth fuzzing is effective yet not comprehensive. Based on the systematization, we provide promising future directions to shed some light on future Bluetooth security research.

The Bluetooth protocol suite, including Bluetooth Classic, Bluetooth Low Energy, and Bluetooth Mesh, has become the de facto standard for short-range wireless communications. While formal methods have been applied to Bluetooth security, existing efforts either focus on one configuration of a protocol or one protocol of the suite, without considering other configurations or interactions among protocols. As a result, manual analysis still dominates the state-of-the-art security research of Bluetooth specification. To enable automatic Bluetooth security analysis with formal guarantees, we propose a comprehensive formal model for Bluetooth protocol suite covering both the key sharing phase and the data transmission phase, in all the three Bluetooth protocols, and detecting their design flaws automatically. Our formal model, written in ProVerif, adopts a modular design by abstracting each step within a protocol into an interface and implementing different methods in each step as modules to instantiate the interface, through which all possible configurations of a protocol could be examined. We further abstract different Bluetooth protocols into modules enabling the modeling of their interactions and relax the threat model to allow reasoning about semi-compromised devices. We use this model to formally verify 418 security properties and find 82 violations with attack examples capturing 5 known vulnerabilities and discovering 2 new security issues. Bluetooth SIG confirmed our independent discovery of these 2 new issues, with one issue assigned a CVE and the other issue acknowledged in a security notice. Our model provides one step towards formally verified Bluetooth security.

Today, there are many hybrid apps in which both native Android app UI and WebView UI are used. To protect the security and privacy of the communications, these hybrid apps all use HTTPS by WebView, a key component in modern web browser. In this paper, we show there is another type of SSL vulnerability that stems from the error-handling code in the hybrid mobile web apps. At a high level, this error-handling code should have stopped the communication but it still proceeds regardless of certificate errors, thereby leading to the MITM attacks. To automatically identify these vulnerable apps, we present a hybrid approach that combines both static analysis and dynamic analysis. We have implemented our approach and evaluated with 13,820 real world mobile web apps from a third party market, of which 645 are confirmed truly vulnerable, with an average overhead of 60.8 seconds per app.

Security of authentication protocols heavily relies on the confidentiality of credentials (or authenticators) like passwords and session IDs. However, unlike browser-based web applications for which highly evolved browsers manage the authenticators, Android apps have to construct their own management. We find that most apps simply locate their authenticators into the persistent storage and entrust underlying Android OS for mediation. Consequently, these authenticators can be leaked through compromised backup channels. In this work, we conduct the first systematic investigation on this previously overlooked attack vector. We find that nearly all backup apps on Google Play inadvertently expose backup data to any app with internet and SD card permissions. With this exposure, the malicious apps can steal other apps' authenticators and obtain complete control over the authenticated sessions. We show that this can be stealthily and efficiently done by building a proof-of-concept app named AuthSniffer. We find that 80 (68.4%) out of the 117 tested top-ranked apps which have implemented authentication schemes are subject to this threat. Our study should raise the awareness of app developers and protocol analysts about this attack vector.

An enormous number of applications have been developed for Android in recent years, making it one of the most popular mobile operating systems. However, it is obvious that more vulnerabilities would appear along with the booming amounts of applications. Poorly designed applications may contain security vulnerabilities that can dramatically undermine users' security and privacy. In this paper, we studied a kind of recently reported application vulnerability named confused deputy - a specific type of privilege escalation vulnerability, which can result in unauthorized operations, and so on. We proposed a novel system with code-level static analysis to analyze the applications and automatically detect possible confused deputy vulnerabilities. To tackle analysis challenges imposed by Android's component-based programming paradigm, we employed special control flow graph construction techniques to build call relations among components and function call graph within components. We developed a prototype of this system named PaddyFrog and evaluated with 7190 real world Android applications from two of the most popular markets in China. We found 1240 applications with confused deputy vulnerability and proved to be exploitable. The median execution time of this system on an application is 14.4s, which is fast enough to be used in volumes of applications testing scenarios. Copyright © 2015 John Wiley & Sons, Ltd.