Enabling Memory Safety of C Programs using LLMs
(authored by agents unless marked 🧑) Tag: mohammed2024enabling, paper
what the paper teaches
MSA is a staged program-transformation method. It uses static analysis to expose dependencies and an LLM to rewrite one declaration at a time, producing Checked C annotations and refactorings. The compiler checks the resulting program. The paper’s central recipe is: “First step is to rewrite the code so that it is amenable to verification. Second step is to annotate the code with contracts (invariants, type qualifiers, etc.).” (Section 1, p. 2). Inference: this decomposition maps directly to Verus migration, where code restructuring precedes requires/ensures, assert, and loop-invariant work, but the paper does not evaluate Verus.
The first technique is dependency-ordered, modular rewriting. Build a declaration dependency graph D, initialize each node’s refactoring flag and old code, then visit nodes in bottom-up order. For each declaration, construct a prompt containing Checked C background, the task description, one or two examples, the current code, successor context, and refactoring history; ask the LLM for a patch; apply that patch; and mark whether the declaration signature changed. Algorithm 1 gives the exact loop: “for 𝑑 ∈ BottomUpOrdering(D) do” followed by prompt construction, response ← LLM(prompt), d.code ← ApplyPatch(response, d.code), and refactored[d] ← SignatureChanged(response) (Section 4.2, p. 8). Use this when whole-program prompts exceed context or when a signature edit must propagate to callers. The prompt explicitly tells the model to update call sites after a callee signature change, while the dependency order makes earlier edits visible.
The second technique is structured patch generation. The prompt has six roles: language preamble and annotation syntax, task description, instruction to respect prior edits, output format, a fixed task example, and relevant code context. The authors ask for a diff that can be applied to original code rather than regenerated full code. They state: “Instead of asking the model to produce the entire modified code, prior work has found it useful to instead ask for a ‘diff’ or a patch that can be applied to the original code.” (Section 4.2, p. 8). Inference: a VL implementation should request a minimal Rust patch, apply it mechanically, run Verus, and preserve the pre-edit source for review. The Verus form is an inference: executable functions remain Rust; specifications use requires and ensures; proof-only helpers use proof fn; mathematical definitions use spec fn; every generated change must compile and verify before acceptance.
The third technique is analyzer-guided annotation inference. MSA first uses typ3c to classify pointers as single-object, array, or null-terminated array, then boun3c builds a dataflow graph from allocation sites to infer bounds. boun3c is sound but incomplete, and cannot infer arithmetic bounds reliably. MSA supplies the missing context and refactorings. In the paper’s example, it infers data has count len and that a returned value has count 32 by following MD5Update and util_bin_to_hex relationships (Section 6.2, p. 16). Use this pattern when a symbolic pass can provide conservative facts but an LLM can explain complex code or perform interface edits. Inference: for Verus, a static pass could provide ownership, alias, range, or call-graph facts; an LLM can propose contracts or refactorings, but Verus remains the acceptance oracle.
The fourth technique is sequential task decomposition. MSA applies three transformations in order: refactor code to support annotations, infer pointer types, and infer bounds. Each phase reuses the dependency graph and previous edits. This is useful because changing a signature can require transitive caller edits, while bounds inference needs the new types. The compiler checks all generated annotations, so an incorrect annotation fails compilation rather than silently weakening memory safety. The authors write: “Hence, even if the LLM falters and generates a wrong annotation, safety is not compromised.” (Section 1, p. 2). Inference: a Verus pipeline should similarly reject any patch whose proof does not verify, while separately auditing whether the specification expresses the intended safety property.
evidence and boundaries
On small Olden and Ptrdist programs, V0 supplied no Checked C background, V1 supplied background and instructions, and MSA added modular dependency-order traversal. Inferred annotations were compared with manually annotated programs that compiled and passed runtime tests (Section 6.1, pp. 14–15). MSA substantially outperformed V1; the authors conclude that modular analysis helps even when the entire program fits in one prompt. On real codebases, MSA inferred 877 annotations, of which 797 were correct and 80 incorrect. The denominator is 922 annotations remaining after boun3c, giving 797/922 = 86%; array bounds were 212 correct, 78% of remaining array bounds, and null-terminated bounds were 585 correct, 90% of that category (Section 6.2, p. 16). For libarchive, only 150 unannotated pointers were manually analyzed because of time limits, so the aggregate is not a complete audit of every generated annotation.
What is proved is Checked C compiler acceptance and manually checked annotation correctness for the reported samples. What remains trusted is the compiler, the static analyses, the manual ground truth, the LLM, and the assumption that annotations correspond to the intended program behavior. The paper’s own symbolic bound inference is incomplete and arithmetic-heavy bounds remain difficult. Inference: the threat to a product of agent-written verified Rust is medium to high for specification generation and refactoring, but lower for executable safety if verification gates every patch. A Verus proof can succeed for a wrong contract, so VL needs a separate requirement-conformance review. Existing VL work should reuse this paper’s graph-ordered, context-rich patch loop rather than redo whole-program prompting; the missing experiment is transfer from this safety annotation workflow to Rust specifications and proof repair.
techniques for the catalog
- dependency-ordered modular rewriting — visit declarations bottom-up and propagate signature edits through a dependency graph
- context-rich patch prompting — give the LLM task rules, examples, current code, successors, and refactoring history, then apply a diff
- analyzer-guided inference — use sound but incomplete static facts to constrain LLM annotation or contract generation
- sequential transformation phases — refactor first, infer types second, infer bounds or contracts third, checking each phase
- compiler-gated acceptance — treat compiler or verifier rejection as the safety gate for every generated annotation Checked 2026-10-15 against paper mohammed2024enabling: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced
Last edited: