What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914032501391360 |
|---|---|
| author | Yan, Biwei Zhang, Yue Xu, Minghui Pan, Runyu Li, Jinku Cheng, Xiuzhen |
| author_facet | Yan, Biwei Zhang, Yue Xu, Minghui Pan, Runyu Li, Jinku Cheng, Xiuzhen |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_09291 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection Yan, Biwei Zhang, Yue Xu, Minghui Pan, Runyu Li, Jinku Cheng, Xiuzhen Cryptography and Security Networking and Internet Architecture 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. |
| title | What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection |
| topic | Cryptography and Security Networking and Internet Architecture |
| url | https://arxiv.org/abs/2509.09291 |