Technical Summary: CNnotator: LLM-Guided Memory Safety Annotation Synthesis

Problem Statement

Memory safety errors constitute a significant proportion of security vulnerabilities in C and C++ systems. Unlike modern memory-safe languages (e.g., Rust, Java) that prevent these bugs by design, C relies on implicit memory usage patterns that are difficult for humans to extract and verify. While formal methods and AI offer complementary strengths—neural networks excel at "guessing" patterns while formal tools excel at "checking"—there is a gap in automating the translation of legacy C code into verifiable specifications. Specifically, determining how a C program manipulates memory (ownership, allocation, and deallocation) is tedious for humans but potentially inferable by Large Language Models (LLMs). The challenge lies in generating formal specifications that accurately represent these implicit patterns to enable verification or safe transpilation.

Methodology

The authors present CNnotator, a tool that synthesizes memory safety annotations for C code using a "guess-and-check" loop driven by LLMs. The system targets CN, a contract language based on separation logic (similar to Frama-C but with explicit memory representation akin to Rust's borrow checker).

The CNnotator Workflow

The tool operates as an iterative loop:

1. Preprocessing: The tool merges C project files into a single context and injects necessary CN libraries and macros to handle allocation/deallocation correctly. It parses the code into an Abstract Syntax Tree (AST) using Tree-sitter.
2. Function Selection: It iterates through functions, starting from the bottom of the file to preserve AST positions.
3. LLM "Guess" (Annotation Generation):
   • The LLM is prompted with a guide on CN syntax (scraped from the CN Tutorial), the full project code, and the specific target function.
   • Before generating an annotation, the LLM is asked to identify if the function is inherently unsafe (e.g., use-after-free). If deemed unsafe, the process halts for that function, and a comment is inserted explaining the bug.
   • If the function appears safe, the LLM generates a CN annotation specifying preconditions (ownership requirements) and postconditions.
4. Formal "Check" (Testing):
   • The generated annotation is injected into the C code.
   • The Fulminate backend compiles the specification into runtime checks.
   • The Bennet framework derives random input generators from the precondition to create concrete heap states.
   • The system runs 100 property-based tests to verify if the code executes without memory safety violations under the generated specification.
5. Refinement:
   • Success: If all 100 tests pass, the annotation is accepted.
   • Failure: If tests fail, the error messages are fed back to the LLM to refine the annotation. This loop runs up to six times.
   • Syntax Errors: If the initial generation fails due to syntax errors (which often yield unhelpful compiler messages), the system retries the original prompt up to two additional times rather than using error feedback, leveraging LLM nondeterminism.

Key Contributions

• Tool Development: The creation of CNnotator, a Python-based tool integrating LangChain/LangGraph for agent control, Tree-sitter for parsing, and the Fulminate/Bennet frameworks for automated testing.
• Hybrid Verification Approach: Demonstrating a practical pipeline where LLMs generate separation logic specifications (CN) and formal testing backends validate them, effectively sidestepping the need to trust the LLM's reasoning.
• Benchmark Suite: The construction of a test suite comprising 31 annotatable C functions (ranging from simple ownership to complex loops with global variables and macros) and 3 inherently unsafe functions designed to test the tool's ability to detect bugs.

Experimental Results

The authors evaluated CNnotator across five OpenAI LLM backends (o3, o4-mini, o3-mini, GPT-4.1, and GPT-4o) on the 31 annotatable functions.

• Performance: The o3 reasoning model achieved the highest performance, successfully annotating 96.8% of functions (30/31). It achieved a 90.3% success rate on the first attempt, requiring an average of only 1.10 attempts per successful annotation.
• Chat Models: Even the chat model GPT-4o achieved a 64.5% first-attempt success rate and a 71.0% overall success rate, outperforming the newer o3-mini in first-attempt metrics.
• Failure Modes:
  • The tool successfully identified all three manually inserted inherently unsafe functions (use-after-free, double-free) and declined to annotate them.
  • False positives (annotations passing tests but being incorrect) were not observed in manual inspections of the o3 results.
  • Over-permissive annotations (requiring more ownership than necessary) were noted as a potential issue but considered acceptable as they still yield valid specifications.
• Efficiency: The system demonstrates that for small-to-medium programs, AI-assisted annotation is becoming practical, with minimal iteration required for high-success models.

Significance and Claims

The paper claims that CNnotator demonstrates the viability of AI-assisted annotation for real-world C codebases. By combining the pattern recognition capabilities of LLMs with the rigorous checking of formal testing tools, the approach addresses the "guess-and-check" nature of formal verification.

The authors position this work as a step toward:

1. Code Modernization: Facilitating the migration of legacy C code to safer languages (like Rust) by first establishing memory safety contracts.
2. Verification Automation: Automating the generation of memory safety specifications, a traditionally manual and error-prone task.
3. Practicality: Showing that current models can handle the complexity of memory ownership in C, achieving high success rates with minimal human intervention.

The paper remains modest regarding its scope, noting that the benchmarks consist of functions under 50 lines with simple control flow and do not yet cover complex production code patterns like type casting or advanced pointer arithmetic. However, the results suggest that as LLM capabilities improve, the technique could scale to larger and more complex systems.