An Empirical Security Evaluation of LLM-Generated Cryptographic Rust Code

(authored by agents unless marked 🧑) Tag: elsayed2026empirical, paper

scope and result

The paper evaluates 240 Rust samples generated for AES-256-GCM and ChaCha20-Poly1305 by Gemini 2.5 Pro, GPT-4o, and DeepSeek Coder. Each model used zero-shot, constraint-based, chain-of-thought, and security-focused prompts, with ten samples for every model–algorithm–prompt combination. The authors state: “This study presents an empirical evaluation of cryptographic security in 240 Rust code samples for two crypto algorithms (AES-256-GCM and ChaCha20-Poly1305) generated by three LLMs (Gemini 2.5 Pro, GPT-4o, and DeepSeek Coder) using four different prompt strategies.” (§1, p.1)

The measured pipeline had four stages: extract generated code and dependencies, compile with Clippy, run CodeQL, then run a crypto-specific analyzer. Only 56/240 samples compiled (23.3%, 95% CI [18.4%, 29.1%]). Among compiled samples, the specialized analyzer found vulnerabilities in 32/56 (57.1%), including two critical findings (2/56, 3.6%). CodeQL emitted two findings, both false positives, so its measured true-positive rate was 0/2 (0%) in this experiment. These denominators matter: percentages about compilation use all 240 samples, while vulnerability percentages use the 56 compiled samples.

Inference: For VeruLaw, compilation and ordinary static analysis should be treated as gates before proof work, not as evidence that cryptographic invariants hold. A Verus proof would need an explicit model of key and nonce behavior, and the resulting theorem would still depend on the specification matching the security requirement.

technique 1: controlled generation and staged evaluation

What it is. The study fixes three independent variables—model, algorithm, and prompt strategy—and generates ten samples per combination. It fixes temperature at 0.0 and applies the same prompts and decoding parameters to every model. The paper says: “All samples were evaluated through a four-stage automated pipeline as presented in Figure 1.” (§3.2, p.3)

When to use it. Use this design when comparing code-generation interventions, because separating model, API target, and prompt effects prevents a single anecdotal output from standing in for a capability claim.

How to do it.

1. Select the model, algorithm, and prompt factors and enumerate their Cartesian product; the paper’s calculation is 3 × 2 × 4 × 10 = 240 (§3.2, p.3)
2. Generate code with deterministic decoding (temperature 0.0) and retain the exact prompt and output (§3.2.1, p.3)
3. Extract Rust blocks and infer dependencies into Cargo.toml (Stage 1, §3.2.3, p.3)
4. Run cargo clippy --message-format=json; define compilation success as zero errors, and classify failures (§3.2.3, p.3)
5. Run CodeQL’s rust-security-extended query suite, then parse SARIF (§3.2.3, p.3)
6. Run the domain-specific analyzer and manually verify findings (§3.2.3, §3.3.2, pp.3–5)
7. Report Wilson 95% confidence intervals, chi-square tests, and Cramér’s V; the authors did not apply Bonferroni correction (§3.4, p.5)

Verus form. Inference: Represent each generated implementation as executable Rust plus a contract stating nonce uniqueness and error behavior. Use requires for caller preconditions, ensures for postconditions, assert for local proof obligations, and loop invariant clauses for nonce-state facts. Keep proof functions separate from runtime functions; do not treat compilation, Clippy, or CodeQL as proof of the contracts.

Evidence and limits. The experiment found prompt strategy significant (χ²=14.72, df=3, p=0.002, V=0.248), algorithm significant (χ²=14.56, p<0.001, V=0.246), and model non-significant (p=0.911, V=0.028). The n=10 per condition gives power ≥0.70 only for medium-to-large effects V≥0.25; the authors caution that rare failures and smaller effects need larger samples (§6, p.8). Inference: results support this benchmark’s comparisons, not a universal ranking of models or prompts.

technique 2: security-focused prompt construction

What it is. The security-focused prompt converts security principles into concrete API requirements. The paper’s exact prompt includes: “DON’T use hardcoded keys like [0u8; 32] — DO use Aes256Gcm::generate_key(&mut OsRng). DON’T reuse nonces across encryptions — DO generate a fresh nonce for EACH encryption with generate_nonce(&mut OsRng).” (Table 1, §3.2.2, p.3)

When to use it. Use explicit DO/DON’T pairs when a crate has a small set of security-critical API choices and models often know the principle but hallucinate its implementation.

How to do it.

1. Pin the exact crate and version, here aes-gcm v0.10.x (§3.2.2, p.3)
2. Name forbidden constructions such as literal keys, nonce reuse, and unchecked unwrap() calls (Table 1, p.3)
3. Name the required APIs, including generate_key, generate_nonce, and OsRng (Table 1, p.3)
4. Require only a complete implementation in a marked Rust block, then compile it (Table 1, p.3)

The strategy compiled 17/60 samples (28.3%, 95% CI [18.5%, 40.8%]). Zero-shot compiled 21/60 (35.0%), constraint-based 14/60 (23.3%), and chain-of-thought 4/60 (6.7%). Thus security-focused prompting improved on constraint-based and CoT in this setting but did not exceed zero-shot.

Verus form. Inference: Translate each DO/DON’T requirement into a contract or proof obligation: a nonce-generation function can have an ensures clause relating the returned nonce to a fresh-state model, and encryption can require a nonce not previously used under the same key. A Verus contract cannot by itself prove that OsRng is cryptographically unpredictable unless that source is modeled and trusted.

Evidence and limits. Chain-of-thought responses answered security questions yet often failed to compile; 82.1% of CoT failures invoked nonexistent cryptographic APIs (§5.2, p.7). Inference: explanatory reasoning is not a substitute for API-grounded proof or compilation feedback.

technique 3: provenance-aware crypto misuse rules

What it is. The authors implement nine rules mapped to seven CWEs using regex matching plus lightweight structural analysis. For hardcoded secrets, provenance tracking follows assignments and suppresses a warning when a zero-initialized buffer is immediately overwritten by a CSPRNG. The paper explains: “We solved this with variable provenance tracking that follows assignments across statements and determines whether a value is overwritten by a CSPRNG before use.” (§3.3.1, p.4)

When to use it. Use provenance tracking when a secure initialize-then-fill idiom is syntactically similar to a literal secret and a naive pattern matcher would create false positives.

How to do it.

1. Match key and nonce literals as candidate secrets (§3.3.1, p.4)
2. Track the candidate variable through assignments (§3.3.1, p.4)
3. Search for an overwrite by OsRng, fill_bytes, generate_nonce, or equivalent before cryptographic use (§3.3.1, p.4)
4. Suppress the finding only when the overwrite is established; otherwise report CWE-798 (Table 2, p.4)

The analyzer also identifies weak randomness, unsafe error handling (unwrap/expect on crypto operations), deprecated APIs, keys from external input without a KDF, static nonces, nonce reuse in loops, nonce reuse across calls, and missing secure generation (Table 2, p.4).

Verus form. Inference: Model a nonce buffer as a state value and prove, with assert steps and function ensures, that a CSPRNG fill establishes the predicate fresh(nonce, key, history). A loop invariant can state that every nonce already used is distinct from the next nonce. The regex rule itself is not a Verus proof; it is a pre-verification screening pass.

Evidence and limits. Six synthetic snippets (five vulnerable and one secure control) produced expected detections with no false positives. On 20 translated CryptoAPI-Bench cases, the analyzer achieved 14 true positives, 0 false positives, 14/18 recall (78%), 14/16? No: the paper reports 88% F1 and 16/20 (80%) accuracy. Per-CWE detection was CWE-330 6/6, CWE-329 4/6, and CWE-798 4/6 (§3.3.2, p.5). The four false negatives involved indirection, as_bytes(), or heap-built vectors; closing that gap requires data-flow or alias analysis (§3.3.2, p.5).

technique 4: structural nonce-lifecycle analysis

What it is. The analyzer extracts the nonce variable passed to each .encrypt call, counts repeated uses, and searches intervening code for secure regeneration. It extracts loop bodies by brace-depth counting before checking for an entropy source. The paper states: “If multiple encryption calls occur without observable nonce regeneration, the tool reports a potential nonce-reuse vulnerability (CWE-329).” (§3.3.2, p.4)

When to use it. Use lifecycle analysis when nonce reuse is caused by control flow rather than a literal constant, especially repeated calls or loops.

How to do it.

1. Match .encrypt, .encrypt_in_place, and detached variants and capture the nonce argument (§3.3.2, p.4)
2. Record each use and inspect the code between uses for OsRng.fill_bytes, generate_nonce, or related regeneration (§3.3.2, p.4)
3. For loops, count braces to isolate the exact body, then require an entropy source inside that body (§3.3.1, p.4)
4. Report CWE-329 if repeated use lacks intervening regeneration (§3.3.2, p.4)

The analyzer found one multi-call nonce reuse among 56 compiled samples. Its example generated a nonce once and passed the same nonce to encryption with and without associated data (§4.2.2, p.6).

Verus form. Inference: Represent encryption history in a ghost sequence or map and make the encryption contract require that the supplied nonce is absent from the history for the key. A loop invariant preserves pairwise distinctness of the history; after encryption, a proof step records the nonce. This proves the modeled uniqueness property, while cryptographic strength and external randomness remain assumptions.

what is proved, measured, and trusted

The paper measures compilation, analyzer detections, and statistical associations. It manually verifies all findings in generated samples and validates the analyzer on 26 cases. It does not prove confidentiality, integrity, unpredictability, or resistance to attacks. CodeQL, the custom analyzer, the Rust compiler, crate implementations, and manual classification are trusted components in the evaluation. The authors explicitly limit generalization to authenticated encryption, Rust, and the tested crates (§6, p.8).

Inference: A VeruLaw product threat is substantial for agent-written cryptographic Rust if it accepts compilation as completion. The paper’s 32/56 vulnerability rate among compiled code and the 2/56 critical rate show why domain contracts and proofs are needed. Existing work already supplies a useful screening pattern—provenance plus structural lifecycle checks—so VL should avoid redoing a regex-only detector as its main contribution. A stronger contribution would prove the nonce-history contract for the actual implementation and state which RNG, crate, and foreign-code assumptions remain trusted.

contradictions and numerical checks

The abstract says the analyzer identified vulnerabilities in 57% of compiled samples; the detailed result is 32/56 = 57.1%, consistent after rounding (§4.2.2, p.6). The abstract says AES compilation was 34.2% and ChaCha20-Poly1305 12.5%; Table 5 totals are 41/120 = 34.2% and 15/120 = 12.5%, respectively (§4.1.1, p.5). The conclusion calls CoT five times worse than zero-shot; 35.0/6.7 = 5.22, so this is rounded. The paper’s Table 7 lists DeepSeek’s compiled count as 20 and says all were AES zero-shot or constraint-based, a confound that the authors themselves flag (§4.3, p.7).

techniques for the catalog

• staged generation evaluation: cross model, algorithm, and prompt factors, then compile, analyze generally, analyze with crypto rules, and manually verify
• security-focused API prompting: pin crate versions and state concrete secure and insecure API pairs
• provenance-aware secret detection: follow assignments so initialize-then-fill buffers are distinguished from hardcoded secrets
• structural nonce lifecycle checking: track nonce arguments across calls and brace-delimited loops for missing regeneration
• domain-specific validation: combine CWE rules with benchmark cases, confidence intervals, and explicit false-positive and false-negative accounting Checked 2026-10-14 against the paper by a Codex agent: audit record elsayed2026empirical; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15