Analysis of Android Bluetooth Security Manager Protocol

Restricted (Penn State Only)
- Author:
- Wang, Weixuan
- Graduate Program:
- Computer Science and Engineering
- Degree:
- Master of Science
- Document Type:
- Master Thesis
- Date of Defense:
- November 08, 2024
- Committee Members:
- Syed Rafiul Hussain, Thesis Advisor/Co-Advisor
Sencun Zhu, Committee Member
Chitaranjan Das, Program Head/Chair - Keywords:
- Bluetooth
Security Manager Protocol
Software Testing
Symbolic Execution
Fuzzing - Abstract:
- In this work, we develop SMPAnalyzer, a principled technique to analyze the security and robustness of the Android Bluetooth Security Manager Protocol (SMP) implementation. At its core, SMPAnalyzer symbolically analyzes the Android Bluetooth SMP source code to extract states and transitions of the SMP protocol and then uses the extracted state machine in two ways to find potential logical and memory-related vulnerabilities in the SMP implementation. First, SMPAnalyzer compares the extracted states and transitions with the ones in the Bluetooth specifications to find deviant behavior. As deviant behavior indicates the presence of potential logical vulnerabilities (e.g., authentication bypass), SMPAnalyzer uses such indicators to detect logical vulnerabilities. For this, we manually extract the prescribed actions, i.e., outputs for a given input at each protocol state of SMP from the Bluetooth specification and compare the actions with that of the extracted state machine of the implementation. Second, to find memory bugs more effectively, we integrate the state machine of the SMP implementation with an existing general-purpose fuzzer called libFuzzer and develop a stateful fuzzer for the Android Bluetooth SMP. Our stateful fuzzer can quickly reach deeper states and find potential deeper memory bugs. To our knowledge, SMPAnalyzer is the first automated technique to analyze Bluetooth SMP implementation and can analyze both logical correctness and memory safety violations. With SMPAnalyzer, we confirmed four previous logical vulnerabilities and detected one new deviant behavior. We also detected four previous memory bugs and found manually introduced bugs in deeper states.