Pith. sign in

REVIEW 4 major objections 7 minor 43 references

BLE app security can be checked at scale by using LLMs to translate app code into formal models that a verifier can prove or refute.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

An LLM-based pipeline that converts Android BLE app code into ProVerif models finds that only about 10% of 1,050 apps implement encryption, nonces, and authentication.

T0 review reviewed 2026-08-04 challenge →

load-bearing objection Solid LLM-to-ProVerif pipeline, but the headline prevalence numbers rest on a validation loop that never measures extraction recall. the 4 major comments →

arxiv 2509.09291 v1 pith:H2KA57UI submitted 2025-09-11 cs.CR cs.NI

What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection

Biwei Yan , Yue Zhang , Minghui Xu , Runyu Pan , Jinku Li , Xiuzhen Cheng This is my paper
classification cs.CR cs.NI
keywords BLE securityapplication-layer securityformal verificationLLM code translationstatic analysisAndroid applicationsProVerifvulnerability detection
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper argues that BLE application-layer security analysis is best reframed as a translation problem: instead of asking an LLM whether code is vulnerable, ask it to convert slices of real app code into formal process models, then let a symbolic verifier decide. The authors build VerifiaBLE, which combines BLE-aware static slicing, retrieval-augmented prompt engineering, and formal verification of three protections: encryption, freshness (nonces), and authentication. On 1,050 Android BLE apps, the pipeline reports that only 10.2% implement all three protections and 53.9% implement none. Manual validation of 200 samples gives 96% precision on apps flagged secure and 100% on apps flagged insecure, supporting the claim that LLM-assisted formal modeling can make large-scale security claims auditable.

Core claim

Formal verification of real-world BLE apps is feasible at scale if the verification question is restated as code-to-model translation. The pipeline first isolates BLE-relevant execution paths from decompiled Android bytecode, then uses an LLM with retrieval-augmented, chain-of-thought prompts to render those paths as applied-pi-calculus processes with secrecy, freshness, and correspondence queries, and finally runs a symbolic verifier to prove or refute them. The paper reports that only 10.2% of 1,050 apps implement encryption, randomness, and authentication together, while 53.9% omit all three. Manual inspection of 100 flagged-secure and 100 flagged-insecure apps found 96% and 100% agreemen

What carries the argument

The load-bearing mechanism is the three-phase pipeline: (1) BLE-aware code slicing, which scans decompiled Android code for BLE API entry points and recursively walks the call graph to collect all transitive dependencies; (2) prompt-guided model generation, in which an LLM translates each slice into a formal process model using retrieval-augmented syntax rules, protocol templates, examples, and error-recovery pairs; and (3) symbolic verification, in which the verifier (ProVerif) checks three properties encoded as queries: secrecy for encryption, fresh-name generation for nonces, and correspondence assertions for authentication. The division of labor is what does the work: the LLM handles inf

Load-bearing premise

The whole result rests on the extraction step catching every code path that contributes to encryption, nonce, or authentication; if a path is missed, both the verifier and the human validator look at the same incomplete slice and can label a secure app as insecure.

What would settle it

Build a corpus of BLE apps whose full source is known and whose security features are deliberately placed in callbacks, reflection, or native code outside the slicer's obvious reach, run VerifiaBLE, and check whether apps that genuinely implement all three protections are flagged insecure. Any such false negative would show the extraction step, not the translator, is the limiting component.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Security verdicts become auditable: when a property fails, the symbolic verifier returns a concrete attack trace that names the exploit, giving developers a fixable explanation rather than a black-box score.
  • The LLM is not asked to judge security, only to translate, so hallucination and nondeterminism are bounded rather than directly deciding the outcome.
  • The same architecture can generalize to other security-critical domains where code must be lifted to a formal specification, a direction the paper explicitly suggests for testing, specification mining, and log analysis.
  • The large-scale empirical picture is stark: 10.2% of apps implement all three protections, 53.9% implement none, and even high-download or high-rated apps often lack freshness guarantees, leaving replay attacks possible.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Because the validation step inspects the same extracted slices the verifier sees, a slice that omits a real security path would make an app look insecure when it is not; the reported 10.2% secure figure is therefore best read as a lower bound, with the true secure share possibly higher.
  • The translator pattern is portable: replacing the BLE API scanner with, say, a WebAssembly or firmware call-graph extractor would let the same retrieval-augmented generation plus verifier loop produce auditable models for other heterogeneous codebases.
  • A testable extension is to measure slicer recall directly by constructing apps with known hidden security paths placed in callbacks, reflection, or native code, then checking whether VerifiaBLE still reports them insecure; this would separate extraction omissions from translation errors.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 7 minor

Summary. The paper proposes VerifiaBLE, a system that analyzes Android BLE applications by (1) statically extracting BLE-related code slices, (2) using an LLM with retrieval-augmented prompting to translate those slices into ProVerif process models, and (3) running ProVerif to check three security features: encryption, randomness/nonce usage, and authentication. The authors evaluate the system on 1,050 BLE apps from AndroZoo, report a manual validation of 100 flagged-secure and 100 flagged-insecure apps, compare against three existing BLE analysis frameworks, and present ecosystem-level statistics claiming that only 10.2% of apps implement all three protections and 53.9% omit all of them. They also include category, download, rating, developer, version-evolution, and real-device case-study analyses.

Significance. If substantiated, the paper makes a useful contribution by reframing formal-methods-based security analysis as a code-to-formal-model translation task and delegating the judgment step to ProVerif rather than to the LLM. The architecture is sensible, the evaluation corpus is large, and the use of ProVerif provides an external check on the translated models. The paper does not rely on fitted parameters or a learned classifier, which reduces the risk of overfitting in the core translation pipeline. However, the headline prevalence claim ('only 10.2% secure') is only as strong as the code-extraction phase, and the current validation does not measure extraction recall. The study is likely to be of interest to the security and software-engineering communities if that gap is closed with an independent ground-truth evaluation.

major comments (4)
  1. [Section V-B, with Section IV-A] The manual validation measures LLM translation fidelity but not extraction recall. The authors state that they 'manually inspected the BLE-relevant execution paths extracted by our tool' for 100 secure and 100 insecure apps. Since the human reviewer sees the same code slices that were fed to the LLM, a security-relevant path omitted by Phase I is invisible to both the tool and the validator. The slicing phase is based on BLE API entry points and recursive call-graph traversal, so logic reachable through reflection, dynamic proxies, native code, or service-bound callbacks may be missed. As a result, false negatives are never measured, and the reported 96% precision on flagged-secure apps is conditional on slicer completeness. The headline 'only 10.2% secure' (Table III) could therefore be substantially wrong. I would like to see a recall experiment in which, for a random sample of apps, t
  2. [Section V-B, Table II] The baseline comparison is under-specified. The metric 'Secure Apps Acc.' is not defined (precision? recall? agreement rate?), and it is unclear whether the 100 secure and 100 insecure apps are labeled by VerifiaBLE's output or by the manual inspection. If the latter, the same circularity as above applies to the baselines. The accuracy values are presented without per-tool counts or confidence intervals; for example, 86% versus 88% on 100 samples is not a meaningful difference without error bars. A precise evaluation protocol is needed: how ground-truth labels were constructed, how each tool's output was normalized to a 'secure/insecure' decision, and what exact metric is reported.
  3. [Section V-C, Table III] The prevalence estimate is not a supported point estimate. Even assuming slicer completeness, the 4 false positives among 100 flagged-secure apps (Section V-B) means the true proportion of fully secure apps is at most 10.19%, not exactly 10.19%. Conversely, the unmeasured false-negative rate among flagged-insecure apps means the 53.9% figure for 'omit them entirely' is at best a statement about the extracted slices, not about the apps. The wording throughout the paper should be revised to say 'no protection found in the extracted slice' unless an independent recall study is added.
  4. [Section V-A, and Section III-A] The dataset construction is not described in enough detail to support generalizable ecosystem claims. The paper says 8,296 apps were downloaded from AndroZoo and filtered to 1,050 BLE apps, but the sampling frame, the AndroZoo query or selection criteria, and the date of collection are not given. The paper also scopes to non-obfuscated apps (Section III-A) but does not explain how obfuscation was detected or excluded. Without this information, the category, download, and rating analyses in RQ1–RQ6 cannot be interpreted as representative of the Android BLE ecosystem. Please specify the sampling procedure, inclusion/exclusion criteria, and the number of apps excluded at each step.
minor comments (7)
  1. [Table IV] The column header 'E N A E N A ...' is ambiguous; each of the eight feature combinations should be labeled explicitly (e.g., with a legend or separate columns for Encryption, Nonce, Authentication). The current row of check/cross marks is difficult to map to the percentages.
  2. [Section V-B, Table II] BLEScope appears in Table II but Section V-B only describes BLESS and BLECryptracer. State where the BLEScope numbers come from and how its output was mapped to the secure/insecure decision.
  3. [Section V-B] The phrase 'main sources of FP' should be 'main sources of FPs', and the sentence structure in the FP explanation could be tightened.
  4. [Section IV-B] The iterative repair loop's retry threshold, success rate, and average number of repair iterations are not reported. Without these, the claim that the system is practical and scalable is hard to assess.
  5. [Figure 7] The app identifiers in the figure appear obfuscated (e.g., 'com.pet.canner .p.' and 'com.in.tagram.thread.app') while the text names the same apps with different spellings (e.g., 'com.petscanner.ps' and 'com.instagram.threadsapp'). Please align the identifiers.
  6. [Section III-A] The terminology for the second security feature oscillates among 'randomness', 'nonces', and 'freshness'. Standardize on one term and define it precisely at first use.
  7. [Section V-A] The sentence 'Therefore, we utilize BLE-related functions... as well as relevant permission settings... to filter out BLE apps' is grammatically awkward; it should read 'to filter in BLE apps' or 'to identify BLE apps'.

Circularity Check

1 steps flagged

Manual validation reuses VerifiaBLE's own code slices as ground truth, so extraction recall is unmeasured; the central LLM+ProVerif pipeline is otherwise not circular.

specific steps
  1. self definitional [Section V-B (Performance of VerifiaBLE), first paragraph]
    "Specifically, we randomly sampled 100 applications flagged as secure and 100 applications flagged as insecure. For each sample, we manually inspected the BLE-relevant execution paths extracted by our tool, focusing on whether the app correctly implements three core security features: encryption, randomness (e.g., nonces), and authentication."

    Phase I produces the BLE-relevant execution paths S; VerifiaBLE's classification C is a function of S. The manual validation V is explicitly performed on 'the BLE-relevant execution paths extracted by our tool', i.e., the same S. Therefore V is not an independent ground truth for the app—it is a ground truth for S. Any security-relevant path that Phase I fails to extract is invisible to both C and V, so the reported 96%/100% precision only validates that the LLM+ProVerif faithfully translate S, not that S is complete. The headline prevalence (10.2% secure) inherits this unvalidated completeness assumption, and false negatives are never measured. The validation loop is thus partially circular: it cannot fail on extraction errors.

full rationale

The core derivation—BLE code → static slicing → LLM-generated ProVerif model → symbolic verification—is not circular: it uses an external verifier and involves no fitted parameters, and the paper's self-citations (BLEScope, BLESS) are baselines rather than load-bearing assumptions. However, the evaluation of the central reliability claim is partially circular. The human validation inspects exactly the same extracted execution paths that the tool feeds to the LLM, so agreement between the human and VerifiaBLE measures translation fidelity only, not whether the slicer captured all security-relevant logic. Consequently, the 10.2%-secure statistic and the 96%/100% precision figures are conditional on slicing completeness, which is never independently tested. The real-device attack case studies (Section V, RQ7) provide some external confirmation, but they cover only three devices and do not measure recall. Overall, the paper has a genuine independent verification core, but its headline empirical claim is not fully de-circularized because the ground truth shares the tool's own intermediate representation.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

The paper introduces no new mathematical quantities or entities. Its contributions are an engineering pipeline and an empirical measurement. The load-bearing assumptions are methodological: the definition of the three features, the symbolic threat model, the fidelity of decompilation, and the validity of the manual ground truth.

axioms (4)
  • domain assumption The three security features (encryption, randomness/nonces, authentication) are sufficient operationalizations of BLE app-layer security for the study's conclusions.
    Section III-A defines the scope and Table I links their absence to attack categories; this is a modeling choice, not a theorem.
  • domain assumption The ProVerif symbolic attacker model is an appropriate threat model for real-world BLE conclusions.
    Section II-B and IV-C rely on ProVerif's Dolev-Yao style analysis; limitations for side channels or implementation bugs are not discussed.
  • domain assumption Decompilation of DEX to Java preserves enough semantics for static analysis and LLM translation.
    Section IV-A decompiles APKs to JAR then Java; no fidelity validation is provided.
  • domain assumption Manual inspection of extracted code slices by the authors is an accurate ground truth for the three features.
    Section V-B uses manual inspection as ground truth; no inter-rater reliability or independent review is described.

reviewed 2026-08-04 · how reviews work

0 comments
Cite this review

Pith. "Pith review of What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection." pith.science (2026). https://pith.science/paper/H2KA57UI

@misc{pith2026250909291,
  author       = {Pith},
  title        = {Pith review of: What You Code Is What We Prove: Translating BLE App Logic into Formal Models with LLMs for Vulnerability Detection},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/H2KA57UI}},
  note         = {Machine review of arXiv:2509.09291}
}
Share X Bluesky LinkedIn Reddit HN
read the original 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.

Figures

Figures reproduced from arXiv: 2509.09291 by Biwei Yan, Jinku Li, Minghui Xu, Runyu Pan, Xiuzhen Cheng, Yue Zhang.

Figure 1
Figure 1. Figure 1: BLE Protocol Stack and Security Architecture [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Code snippet of AppLights To evaluate the security of such custom BLE protocols more rigorously, formal verification techniques are often em￾ployed. Analysts typically begin by reviewing the application’s source code and abstracting the protocol logic into a formal specification language, such as applied pi-calculus. They then define security goals like confidentiality or authentication, and use tools such… view at source ↗
Figure 3
Figure 3. Figure 3: Design of VerifiaBLE: Phase I extracts BLE code snippets from APKs. Phase II uses an LLM and RAG context to generate ProVerif models. Phase III verifies these models and reports potential vulnerabilities. contents, focusing on retrieving the Dalvik Executable (DEX) files that contain the compiled bytecode. These DEX files are then converted into Java Archive (JAR) format to enable compatibility with standa… view at source ↗
Figure 4
Figure 4. Figure 4: Distribution of Download Numbers for BLE Apps [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Percentage of Secure/Insecure BLE Apps Across [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: The distribution of apps across developers, categories (by color), and security (by edge color). Bubble size reflects [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Security Evolution of BLE Applications Across Mul [PITH_FULL_IMAGE:figures/full_fig_p009_7.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

43 extracted references · 2 linked inside Pith

  1. [1]

    Automatic fingerprinting of vulnerable BLE IoT devices with static UUIDs from mobile apps,

    C. Zuo, H. Wen, Z. Lin, and Y . Zhang, “Automatic fingerprinting of vulnerable BLE IoT devices with static UUIDs from mobile apps,” in Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019, pp. 1469–1483

    2019

  2. [2]

    BLESS: A BLE application security scanning framework,

    Y . Zhang, J. Weng, Z. Ling, B. Pearson, and X. Fu, “BLESS: A BLE application security scanning framework,” inIEEE INFOCOM 2020- IEEE Conference on Computer Communications. IEEE, 2020, pp. 636– 645

    2020

  3. [3]

    BLESA: Spoofing attacks against reconnections in bluetooth low energy,

    J. Wu, Y . Nan, V . Kumar, D. J. Tian, A. Bianchi, M. Payer, and D. Xu, “BLESA: Spoofing attacks against reconnections in bluetooth low energy,” in14th USENIX Workshop on Offensive Technologies (WOOT 20), 2020

    2020

  4. [4]

    Breaking secure pairing of bluetooth low energy using downgrade attacks,

    Y . Zhang, J. Weng, R. Dey, Y . Jin, Z. Lin, and X. Fu, “Breaking secure pairing of bluetooth low energy using downgrade attacks,” in29th USENIX Security Symposium (USENIX Security 20), 2020, pp. 37–54

    2020

  5. [5]

    FirmXRay: Detecting bluetooth link layer vulnerabilities from bare-metal firmware,

    H. Wen, Z. Lin, and Y . Zhang, “FirmXRay: Detecting bluetooth link layer vulnerabilities from bare-metal firmware,” inProceedings of the 2020 ACM SIGSAC conference on computer and communications secu- rity, 2020, pp. 167–180. JOURNAL OF LATEX CLASS FILES, VOL. 14, NO. 8, AUGUST 2021 11

    2020

  6. [6]

    Bluetooth core specification v5. 1,

    M. Woolley, “Bluetooth core specification v5. 1,”Bluetooth Special Interest Group, 2019

    2019

  7. [7]

    Attention is all you need,

    A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. Kaiser, and I. Polosukhin, “Attention is all you need,”Advances in neural information processing systems, vol. 30, 2017

    2017

  8. [8]

    Attention is all you need for LLM-based code vulnerability localization,

    Y . Li, X. Li, H. Wu, Y . Zhang, X. Cheng, S. Zhong, and F. Xu, “Attention is all you need for LLM-based code vulnerability localization,”arXiv preprint arXiv:2410.15288, 2024

    Pith/arXiv arXiv 2024

  9. [9]

    A survey on large language model (LLM) security and privacy: The good, the bad, and the ugly,

    Y . Yao, J. Duan, K. Xu, and et al., “A survey on large language model (LLM) security and privacy: The good, the bad, and the ugly,”High- Confidence Computing, p. 100211, 2024

    2024

  10. [10]

    Llm- based test-driven interactive code generation: User study and empirical evaluation,

    S. Fakhoury, A. Naik, G. Sakkas, S. Chakraborty, and S. K. Lahiri, “Llm- based test-driven interactive code generation: User study and empirical evaluation,”IEEE Transactions on Software Engineering, vol. 50, no. 9, pp. 2254–2268, 2024

    2024

  11. [11]

    An efficient cryptographic protocol verifier based on prolog rules,

    B. Blanchet, “An efficient cryptographic protocol verifier based on prolog rules,” inProceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001, pp. 82–96

    2001

  12. [12]

    Multitask-based evaluation of open- source LLM on software vulnerability,

    X. Yin, C. Ni, and S. Wang, “Multitask-based evaluation of open- source LLM on software vulnerability,”IEEE Transactions on Software Engineering, vol. 50, no. 11, pp. 3071–3087, 2024

    2024

  13. [13]

    To Err is machine: Vulnerability detection challenges LLM reasoning,

    B. Steenhoek, M. M. Rahman, M. K. Roy, M. S. Alam, H. Tong, S. Das, E. T. Barr, and W. Le, “To Err is machine: Vulnerability detection challenges LLM reasoning,”arXiv preprint arXiv:2403.17218, 2024

    Pith/arXiv arXiv 2024

  14. [14]

    Vulnerability detection with code language models: How far are we?

    Y . Ding, Y . Fu, O. Ibrahim, C. Sitawarin, X. Chen, B. Alomair, D. Wag- ner, B. Ray, and Y . Chen, “Vulnerability detection with code language models: How far are we?” in2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE Computer Society, 2024, pp. 469–481

    2024

  15. [15]

    Androzoo: Collecting millions of android apps for the research community,

    K. Allix, T. F. Bissyand ´e, J. Klein, and Y . Le Traon, “Androzoo: Collecting millions of android apps for the research community,” in Proceedings of the 13th international conference on mining software repositories, 2016, pp. 468–471

    2016

  16. [16]

    A study of the feasibility of co- located app attacks against BLE and a Large-Scale analysis of the current Application-Layer security landscape,

    P. Sivakumaran and J. Blasco, “A study of the feasibility of co- located app attacks against BLE and a Large-Scale analysis of the current Application-Layer security landscape,” in28th USENIX Security Symposium (USENIX Security 19), 2019, pp. 1–18

    2019

  17. [17]

    SweynTooth: unleashing mayhem over bluetooth low energy,

    M. E. Garbelini, C. Wang, S. Chattopadhyay, S. Sumei, and E. Kurni- awan, “SweynTooth: unleashing mayhem over bluetooth low energy,” in 2020 USENIX Annual Technical Conference (USENIX ATC 20), 2020, pp. 911–925

    2020

  18. [18]

    Finding traceability attacks in the bluetooth low energy specification and its im- plementations,

    J. Wu, P. Traynor, D. Xu, D. J. Tian, and A. Bianchi, “Finding traceability attacks in the bluetooth low energy specification and its im- plementations,” in33rd USENIX Security Symposium (USENIX Security 24), 2024, pp. 4499–4516

    2024

  19. [19]

    Extrapolating formal analysis to uncover attacks in bluetooth passkey entry pairing

    M. K. Jangid, Y . Zhang, and Z. Lin, “Extrapolating formal analysis to uncover attacks in bluetooth passkey entry pairing.” inNDSS, 2023

    2023

  20. [20]

    BlueSW AT: A lightweight state-aware security framework for bluetooth low energy,

    X. Che, Y . He, X. Feng, K. Sun, K. Xu, and Q. Li, “BlueSW AT: A lightweight state-aware security framework for bluetooth low energy,” inProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 2024, pp. 2087–2101

    2024

  21. [21]

    Eddystone- eid: Secure and private infrastructural protocol for ble beacons,

    L. David, A. Hassidim, Y . Matias, M. Yung, and A. Ziv, “Eddystone- eid: Secure and private infrastructural protocol for ble beacons,”IEEE Transactions on Information Forensics and Security, vol. 17, pp. 3877– 3889, 2022

    2022

  22. [22]

    MiniBLE: Exploring insecure BLE API usages in mini-programs,

    Z. Zhang, J. Du, W. Diao, and J. Wu, “MiniBLE: Exploring insecure BLE API usages in mini-programs,” inProceedings of the ACM Work- shop on Secure and Trustworthy Superapps, 2023, pp. 18–22

    2023

  23. [23]

    Vul-RAG: Enhancing LLM-based vulnerability detection via knowledge-level RAG,

    X. Du, G. Zheng, K. Wang, J. Feng, W. Deng, M. Liu, B. Chen, X. Peng, T. Ma, and Y . Lou, “Vul-RAG: Enhancing LLM-based vulnerability detection via knowledge-level RAG,”CoRR, 2024

    2024

  24. [24]

    On hardware security bug code fixes by prompting large language models,

    B. Ahmad, S. Thakur, B. Tan, R. Karri, and H. Pearce, “On hardware security bug code fixes by prompting large language models,”IEEE Transactions on Information Forensics and Security, vol. 19, pp. 4043– 4057, 2024

    2024

  25. [25]

    Transformer-based language models for software vulnera- bility detection,

    C. Thapa, S. I. Jang, M. E. Ahmed, S. Camtepe, J. Pieprzyk, and S. Nepal, “Transformer-based language models for software vulnera- bility detection,” inProceedings of the 38th Annual Computer Security Applications Conference, 2022, pp. 481–496

    2022

  26. [26]

    Software vul- nerability detection using large language models,

    M. D. Purba, A. Ghosh, B. J. Radford, and B. Chu, “Software vul- nerability detection using large language models,” in2023 IEEE 34th International Symposium on Software Reliability Engineering Workshops (ISSREW), 2023, pp. 112–119

    2023

  27. [27]

    DrAttack: Prompt decomposition and reconstruction makes powerful LLMs jailbreakers,

    X. Li, R. Wang, M. Cheng, T. Zhou, and C.-J. Hsieh, “DrAttack: Prompt decomposition and reconstruction makes powerful LLMs jailbreakers,” inFindings of the Association for Computational Linguistics: EMNLP 2024, 2024, pp. 13 891–13 913

    2024

  28. [28]

    COLD-attack: Jailbreaking LLMs with stealthiness and controllability,

    X. Guo, F. Yu, H. Zhang, L. Qin, and B. Hu, “COLD-attack: Jailbreaking LLMs with stealthiness and controllability,” inProceedings of the 41st International Conference on Machine Learning, 2024, pp. 16 974– 17 002

    2024

  29. [29]

    DeepInception: Hypnotize large language model to be jailbreaker,

    X. Li, Z. Zhou, J. Zhu, J. Yao, T. Liu, and B. Han, “DeepInception: Hypnotize large language model to be jailbreaker,” inNeurips Safe Generative AI Workshop 2024, 2024

    2024

  30. [30]

    Can large language models provide security & privacy advice? measuring the ability of llms to refute misconceptions,

    Y . Chen, A. Arunasalam, and Z. B. Celik, “Can large language models provide security & privacy advice? measuring the ability of llms to refute misconceptions,” inProceedings of the 39th Annual Computer Security Applications Conference, 2023, pp. 366–378

    2023

  31. [31]

    Examining zero-shot vulnerability repair with large language models,

    H. Pearce, B. Tan, B. Ahmad, R. Karri, and B. Dolan-Gavitt, “Examining zero-shot vulnerability repair with large language models,” in2023 IEEE Symposium on Security and Privacy (SP). IEEE, 2023, pp. 2339–2356

    2023

  32. [32]

    On protecting the data privacy of large language models (LLMs) and LLM agents: A literature review,

    B. Yan, K. Li, M. Xu, and et al., “On protecting the data privacy of large language models (LLMs) and LLM agents: A literature review,” High-Confidence Computing, p. 100300, 2025

    2025

  33. [33]

    LLM-guided formal verification coupled with mutation testing,

    M. Hassan, S. Ahmadi-Pour, K. Qayyum, C. K. Jha, and R. Drechsler, “LLM-guided formal verification coupled with mutation testing,” in 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 2024, pp. 1–2

    2024

  34. [34]

    SecureFalcon: Are we there yet in automated software vulnerability detection with LLMs?

    M. A. Ferrag, A. Battah, N. Tihanyi, R. Jain, D. Maimut ¸, F. Alwahedi, T. Lestable, N. S. Thandi, A. Mechri, M. Debbahet al., “SecureFalcon: Are we there yet in automated software vulnerability detection with LLMs?”IEEE Transactions on Software Engineering, 2025

    2025

  35. [35]

    Effectiveness of large language models to generate formally verified C code,

    M. Sevenhuijsen, “Effectiveness of large language models to generate formally verified C code,” 2024

    2024

  36. [36]

    Domain- adapted LLMs for VLSI design and verification: A case study on formal verification,

    M. Liu, M. Kang, G. B. Hamad, S. Suhaib, and H. Ren, “Domain- adapted LLMs for VLSI design and verification: A case study on formal verification,” in2024 IEEE 42nd VLSI Test Symposium (VTS). IEEE, 2024, pp. 1–4

    2024

  37. [37]

    Generative AI augmented induction-based formal verification,

    A. Kumar and D. N. Gadde, “Generative AI augmented induction-based formal verification,” in2024 IEEE 37th International System-on-Chip Conference (SOCC). IEEE, 2024, pp. 1–2

    2024

  38. [38]

    (Security) assertions by large language models,

    R. Kande, H. Pearce, B. Tan, B. Dolan-Gavitt, S. Thakur, R. Karri, and J. Rajendran, “(Security) assertions by large language models,”IEEE Transactions on Information Forensics and Security, vol. 19, pp. 4374– 4389, 2024

    2024

  39. [39]

    Don’t trust: Verify-grounding LLM quantitative reasoning with autoformalization,

    J. P. Zhou, C. Staats, W. Li, C. Szegedy, K. Q. Weinberger, and Y . Wu, “Don’t trust: Verify-grounding LLM quantitative reasoning with autoformalization,” inICLR, 2024

    2024

  40. [40]

    VeriPlan: Integrating formal verification and LLMs into end-user planning,

    C. P. Lee, D. Porfirio, X. J. Wang, K. C. Zhao, and B. Mutlu, “VeriPlan: Integrating formal verification and LLMs into end-user planning,” in Proceedings of the 2025 CHI Conference on Human Factors in Com- puting Systems, 2025, pp. 1–19

    2025

  41. [41]

    Formal-LLM: Integrating formal language and natural language for controllable LLM- based agents,

    Z. Li, W. Hua, H. Wang, H. Zhu, and Y . Zhang, “Formal-LLM: Integrating formal language and natural language for controllable LLM- based agents,”CoRR, 2024

    2024

  42. [42]

    FVEL: Interactive formal verification environment with large language models via theorem proving,

    X. Lin, Q. Cao, Y . Huang, H. Wang, J. Lu, Z. Liu, L. Song, and X. Liang, “FVEL: Interactive formal verification environment with large language models via theorem proving,”Advances in Neural Information Processing Systems, vol. 37, pp. 54 932–54 946, 2024

    2024

  43. [43]

    CryptoFormalEval: Integrating large language models and formal verification for automated crypto- graphic protocol vulnerability detection,

    C. Curaba, D. Denis, and A. Minisini, “CryptoFormalEval: Integrating large language models and formal verification for automated crypto- graphic protocol vulnerability detection,” inThe First Workshop on System-2 Reasoning at Scale, NeurIPS’24, 2024

    2024

This paper was first reviewed by deepseek-v4-flash on August 4, 2026.