{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T13:52:34Z","timestamp":1763733154649,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,3]]},"DOI":"10.1145\/3680207.3765254","type":"proceedings-article","created":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T13:19:18Z","timestamp":1763731158000},"page":"909-922","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalization, Implementation, and Verification of the Bluetooth L2CAP State Machine"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-1703-4066","authenticated-orcid":false,"given":"Tan Khang","family":"Le","sequence":"first","affiliation":[{"name":"Simon Fraser University, Vancouver, British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-0078-0366","authenticated-orcid":false,"given":"Mohammad Omidvar","family":"Tehrani","sequence":"additional","affiliation":[{"name":"Simon Fraser University, Vancouver, British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3370-2431","authenticated-orcid":false,"given":"Yuepeng","family":"Wang","sequence":"additional","affiliation":[{"name":"Simon Fraser University, Vancouver, British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4254-7261","authenticated-orcid":false,"given":"Jianliang","family":"Wu","sequence":"additional","affiliation":[{"name":"Simon Fraser University, Vancouver, British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3771-0156","authenticated-orcid":false,"given":"Steven Y.","family":"Ko","sequence":"additional","affiliation":[{"name":"Simon Fraser University, Vancouver, British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,11,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_1_2_1","unstructured":"Android Open Source Project. 2025. l2c_csm.cc. Google. https:\/\/android.googlesource.com\/platform\/system\/bt\/+\/refs\/heads\/android12-release\/stack\/l2cap\/l2c_csm.cc"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1113792.1113794"},{"key":"e_1_3_2_1_4_1","volume-title":"Bluetooth Core Specification 5.4. Bluetooth SIG","author":"Bluetooth SIG.","unstructured":"Bluetooth SIG. 2025. Bluetooth Core Specification 5.4. Bluetooth SIG, Inc. https:\/\/www.bluetooth.com\/specifications\/specs\/core-specification-5-4\/"},{"key":"e_1_3_2_1_5_1","volume-title":"L2CAP General Procedure -","author":"Bluetooth SIG.","unstructured":"Bluetooth SIG. 2025. L2CAP General Procedure - Vol. 3, Part A, Section 7. Bluetooth SIG, Inc. https:\/\/www.bluetooth.com\/specifications\/specs\/core-specification-5-4\/"},{"key":"e_1_3_2_1_6_1","volume-title":"L2CAP Signaling Packet Formats -","author":"Bluetooth SIG.","unstructured":"Bluetooth SIG. 2025. L2CAP Signaling Packet Formats - Vol. 3, Part A, Section 4. Bluetooth SIG, Inc. https:\/\/www.bluetooth.com\/specifications\/specs\/core-specification-5-4\/"},{"key":"e_1_3_2_1_7_1","volume-title":"L2CAP State Machine -","author":"Bluetooth SIG.","unstructured":"Bluetooth SIG. 2025. L2CAP State Machine - Vol. 3, Part A, Section 6. Bluetooth SIG, Inc. https:\/\/www.bluetooth.com\/specifications\/specs\/core-specification-5-4\/"},{"key":"e_1_3_2_1_8_1","volume-title":"Interactive Theorem Proving: First International Conference, ITP 2010, Edinburgh, UK, July 11\u201314, 2010. Proceedings 1. Springer","author":"B\u00f6hme Sascha","year":"2010","unstructured":"Sascha B\u00f6hme and Tjark Weber. 2010. Fast LCF-style proof reconstruction for Z3. In Interactive Theorem Proving: First International Conference, ITP 2010, Edinburgh, UK, July 11\u201314, 2010. Proceedings 1. Springer, Berlin, Heidelberg, 179\u2013194."},{"key":"e_1_3_2_1_9_1","volume-title":"Insights into States of LE Credit-Based Channel in L2CAP. https:\/\/github.com\/google\/bumble\/discussions\/627. [Online","year":"2025","unstructured":"Bumble. 2025. Insights into States of LE Credit-Based Channel in L2CAP. https:\/\/github.com\/google\/bumble\/discussions\/627. [Online; accessed 15-Jan-2025]."},{"key":"e_1_3_2_1_10_1","volume-title":"International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer","author":"Moura Leonardo De","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, Berlin, Heidelberg, 337\u2013340."},{"key":"e_1_3_2_1_11_1","volume-title":"Program Verification: Fundamental Issues in Computer Science","author":"Floyd Robert W","unstructured":"Robert W Floyd. 1993. Assigning meanings to programs. In Program Verification: Fundamental Issues in Computer Science. Springer, Berlin, Heidelberg, 65\u201381."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676975"},{"key":"e_1_3_2_1_13_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 653\u2013669."},{"key":"e_1_3_2_1_14_1","volume-title":"2003 IEEE Wireless Communications and Networking, 2003. WCNC 2003.","volume":"3","author":"Hager Creighton T","year":"2003","unstructured":"Creighton T Hager and Scott F MidKiff. 2003. An analysis of Bluetooth security vulnerabilities. In 2003 IEEE Wireless Communications and Networking, 2003. WCNC 2003., Vol. 3. IEEE, New York, NY, USA, 1825\u20131831."},{"key":"e_1_3_2_1_15_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Hance Travis","year":"2020","unstructured":"Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. 2020. Storage Systems are Distributed Systems (So Verify Them That Way!). In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, Savannah, GA, 99\u2013115."},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the 25th Symposium on Operating Systems Principles (SOSP). ACM","author":"Hawblitzel Chris","year":"2015","unstructured":"Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Michael L Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP). ACM, New York, NY, USA, 1\u201317."},{"key":"e_1_3_2_1_17_1","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). USENIX Association, Broomfield, CO, 165\u2013181. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458864.3466625"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534382"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_23_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA."},{"key":"e_1_3_2_1_24_1","volume-title":"International conference on logic for programming artificial intelligence and reasoning (LPAR). Springer","author":"Leino K Rustan M","year":"2010","unstructured":"K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning (LPAR). Springer, Berlin, Heidelberg, 348\u2013370."},{"key":"e_1_3_2_1_25_1","volume-title":"SETSS 2017","author":"Leino K Rustan M","year":"2018","unstructured":"K Rustan M Leino. 2018. Modeling concurrency in Dafny. In Engineering Trustworthy Software Systems: Third International School, SETSS 2017, Chongqing, China, April 17\u201322, 2017, Tutorial Lectures 3. Springer, Berlin, Heidelberg, 115\u2013142."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the 20th annual international conference on Mobile computing and networking (MobiCom). ACM","author":"Mike Liang Chieh-Jan","year":"2014","unstructured":"Chieh-Jan Mike Liang, Nicholas D Lane, Niels Brouwers, Li Zhang, B\u00f6rje F Karlsson, Hao Liu, Yan Liu, Jun Tang, Xiang Shan, Ranveer Chandra, et al. 2014. Caiipa: Automated large-scale mobile app testing through contextual fuzzing. In Proceedings of the 20th annual international conference on Mobile computing and networking (MobiCom). ACM, New York, NY, USA, 519\u2013530."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3307334.3326089"},{"key":"e_1_3_2_1_29_1","volume-title":"2022 52nd Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE","author":"Park Haram","year":"2022","unstructured":"Haram Park, Carlos Kayembe Nkuba, Seunghoon Woo, and Heejo Lee. 2022. L2Fuzz: Discovering Bluetooth L2CAP vulnerabilities using stateful fuzz testing. In 2022 52nd Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE, New York, NY, USA, 343\u2013354."},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the 12th IEEE Mediterranean Electrotechnical Conference (IEEE Cat. No. 04CH37521)","volume":"2","author":"Pek Edgar","year":"2004","unstructured":"Edgar Pek and Nikola Bogunovic. 2004. Formal verification of logical link control and adaptation protocol. In Proceedings of the 12th IEEE Mediterranean Electrotechnical Conference (IEEE Cat. No. 04CH37521), Vol. 2. IEEE, New York, NY, USA, 583\u2013586."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/648128.747848"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/648128.761244"},{"key":"e_1_3_2_1_33_1","volume-title":"The 25th Annual International Conference on Mobile Computing and Networking (MobiCom). ACM","author":"Raza Muhammad Taqi","year":"2019","unstructured":"Muhammad Taqi Raza and Songwu Lu. 2019. A Systematic Way to LTE Testing. In The 25th Annual International Conference on Mobile Computing and Networking (MobiCom). ACM, New York, NY, USA, 1\u201315."},{"key":"e_1_3_2_1_34_1","volume-title":"Proceedings of the 18th International Conference on Mobile Systems, Applications, and Services (MobiSys). ACM","author":"Wang Jiliang","year":"2020","unstructured":"Jiliang Wang, Feng Hu, Ye Zhou, Yunhao Liu, Hanyi Zhang, and Zhe Liu. 2020. BlueDoor: breaking the secure information flow via BLE vulnerability. In Proceedings of the 18th International Conference on Mobile Systems, Applications, and Services (MobiSys). ACM, New York, NY, USA, 286\u2013298."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_2_1_36_1","volume-title":"14th USENIX Workshop on Offensive Technologies (WOOT 20)","author":"Wu Jianliang","year":"2020","unstructured":"Jianliang Wu, Yuhong Nan, Vireshwar Kumar, Dave Jing Tian, Antonio Bianchi, Mathias Payer, and Dongyan Xu. 2020. BLESA: Spoofing attacks against reconnections in bluetooth low energy. In 14th USENIX Workshop on Offensive Technologies (WOOT 20). USENIX Association, Savannah, GA, 1\u201312."},{"key":"e_1_3_2_1_37_1","volume-title":"2022 IEEE Symposium on Security and Privacy (SP). IEEE","author":"Wu Jianliang","year":"2022","unstructured":"Jianliang Wu, Ruoyu Wu, Dongyan Xu, Dave Jing Tian, and Antonio Bianchi. 2022. Formal model-driven discovery of bluetooth protocol design vulnerabilities. In 2022 IEEE Symposium on Security and Privacy (SP). IEEE, New York, NY, USA, 2285\u20132303."},{"key":"e_1_3_2_1_38_1","volume-title":"Badbluetooth: Breaking android security mechanisms via malicious bluetooth peripherals.. In NDSS. NDSS, USA, 1\u201315.","author":"Xu Fenghao","year":"2019","unstructured":"Fenghao Xu, Wenrui Diao, Zhou Li, Jiongyi Chen, and Kehuan Zhang. 2019. Badbluetooth: Breaking android security mechanisms via malicious bluetooth peripherals.. In NDSS. NDSS, USA, 1\u201315."},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM","author":"Zhang Yue","year":"2022","unstructured":"Yue Zhang and Zhiqiang Lin. 2022. When good becomes evil: Tracking bluetooth low energy devices via allowlist-based side channel and its countermeasure. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM, New York, NY, USA, 3181\u20133194."},{"key":"e_1_3_2_1_40_1","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Zhang Yue","year":"2020","unstructured":"Yue Zhang, Jian Weng, Rajib Dey, Yier Jin, Zhiqiang Lin, and Xinwen Fu. 2020. Breaking secure pairing of bluetooth low energy using downgrade attacks. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association, Savannah, GA, 37\u201354."}],"event":{"name":"ACM MOBICOM '25: 31st Annual International Conference on Mobile Computing and Networking","location":"Kerry Hotel, Hong Kong Hong Kong China","acronym":"ACM MOBICOM '25","sponsor":["SIGMOBILE ACM Special Interest Group on Mobility of Systems, Users, Data and Computing"]},"container-title":["Proceedings of the 31st Annual International Conference on Mobile Computing and Networking"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3680207.3765254","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T13:27:56Z","timestamp":1763731676000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3680207.3765254"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,3]]},"references-count":40,"alternative-id":["10.1145\/3680207.3765254","10.1145\/3680207"],"URL":"https:\/\/doi.org\/10.1145\/3680207.3765254","relation":{},"subject":[],"published":{"date-parts":[[2025,11,3]]},"assertion":[{"value":"2025-11-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}