{"ID":2872135,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.09291","arxiv_id":"2509.09291","title":"What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection","abstract":"The application layer of Bluetooth Low Energy (BLE) is a growing source of security vulnerabilities, as developers often neglect to implement critical protections such as encryption, authentication, and freshness. While formal verification offers a principled way to check these properties, the manual effort of constructing formal models makes it impractical for large-scale analysis. This paper introduces a key insight: BLE application security analysis can be reframed as a semantic translation problem, i.e., from real-world code to formal models. We leverage large language models (LLMs) not to directly detect vulnerabilities, but to serve as translators that convert BLE-specific code into process models verifiable by tools like ProVerif. We implement this idea in VerifiaBLE, a system that combines static analysis, prompt-guided LLM translation, and symbolic verification to check three core security features: encryption, randomness, and authentication. Applied to 1,050 Android BLE apps, VerifiaBLE uncovers systemic weaknesses: only 10.2\\% of apps implement all three protections, while 53.9\\% omit them entirely. Our work demonstrates that using LLMs as structured translators can lower the barrier to formal methods, unlocking scalable verification across security-critical domains.","short_abstract":"The application layer of Bluetooth Low Energy (BLE) is a growing source of security vulnerabilities, as developers often neglect to implement critical protections such as encryption, authentication, and freshness. While formal verification offers a principled way to check these properties, the manual effort of construc...","url_abs":"https://arxiv.org/abs/2509.09291","url_pdf":"https://arxiv.org/pdf/2509.09291v1","authors":"[\"Biwei Yan\",\"Yue Zhang\",\"Minghui Xu\",\"Runyu Pan\",\"Jinku Li\",\"Xiuzhen Cheng\"]","published":"2025-09-11T09:27:37Z","proceeding":"cs.CR","tasks":"[\"cs.CR\",\"cs.NI\"]","methods":"[\"Large Language Model\",\"Language Model\"]","has_code":false}