Technische Samenvatting: CNnotator: LLM-gestuurde synthese van geheugensafety-annotaties

Probleemstelling

Geheugensafety-fouten vormen een aanzienlijk deel van de beveiligingskwetsbaarheden in C- en C++-systemen. In tegenstelling tot moderne geheugensafe talen (bijv. Rust, Java), die deze bugs bij ontwerp voorkomen, vertrouwt C op impliciete geheugengebruikspatronen die moeilijk door mensen te extraheren en te verifiëren zijn. Hoewel formele methoden en AI complementaire sterktes bieden — neurale netwerken blinken uit in het "raden" van patronen, terwijl formele tools uitblinken in het "controleren" — bestaat er een kloof in het automatiseren van de vertaling van legacy C-code naar verifieerbare specificaties. Specifiek is het bepalen hoe een C-programma met geheugen omgaat (eigendom, allocatie en deallocatie) een tijdrovende taak voor mensen, maar potentieel afleidbaar door Large Language Models (LLM's). De uitdaging ligt in het genereren van formele specificaties die deze impliciete patronen accuraat representeren om verificatie of veilige transpilatie mogelijk te maken.

Methodologie

De auteurs presenteren CNnotator, een tool die geheugensafety-annotaties voor C-code synthetiseert via een "guess-and-check"-lus aangedreven door LLM's. Het systeem richt zich op CN, een contracttaal gebaseerd op separation logic (vergelijkbaar met Frama-C, maar met een expliciete geheugenrepresentatie die lijkt op die van Rust's borrow checker).

De CNnotator Workflow

De tool werkt als een iteratieve lus:

1. Preprocessing: De tool voegt C-projectbestanden samen tot één context en injecteert noodzakelijke CN-bibliotheken en macro's om allocatie/deallocatie correct af te handelen. Het parseert de code naar een Abstract Syntax Tree (AST) met behulp van Tree-sitter.
2. Functieselectie: De tool iterereert door functies, beginnend onderaan het bestand om de AST-posities te behouden.
3. LLM "Guess" (Annotatiegeneratie):
   • De LLM wordt geprompt met een gids over de CN-syntax (gescraped uit de CN Tutorial), de volledige projectcode en de specifieke doelfunctie.
   • Voordat de annotatie wordt gegenereerd, wordt de LLM gevraagd te identificeren of de functie inherent onveilig is (bijv. use-after-free). Als de functie als onveilig wordt beschouwd, stopt het proces voor die functie en wordt er een commentaar ingevoegd die de bug uitlegt.
   • Als de functie veilig lijkt, genereert de LLM een CN-annotatie die precondities (eigendomseisen) en postcondities specificeert.
4. Formele "Check" (Testen):
   • De gegenereerde annotatie wordt in de C-code geïnjecteerd.
   • De Fulminate backend compileert de specificatie naar runtime-checks.
   • Het Bennet framework afleidt willekeurige inputgeneratoren uit de precondition om concrete heap-toestanden te creëren.
   • Het systeem voert 100 property-based tests uit om te verifiëren of de code zonder schendingen van de geheugensafety wordt uitgevoerd onder de gegenereerde specificatie.
5. Verfijning:
   • Succes: Als alle 100 tests slagen, wordt de annotatie geaccepteerd.
   • Falen: Als tests falen, worden de foutmeldingen teruggekoppeld aan de LLM om de annotatie te verfijnen. Deze lus kan tot zes keer worden uitgevoerd.
   • Syntaxfouten: Als de initiële generatie faalt door syntaxfouten (die vaak onbruikbare compilerberichten opleveren), probeert het systeem de oorspronkelijke prompt tot twee extra keren opnieuw in plaats van foutfeedback te gebruiken, waarbij gebruik wordt gemaakt van de nondeterminisme van de LLM.

Belangrijkste Bijdragen

• Toolontwikkeling: De creatie van CNnotator, een Python-gebaseerde tool die LangChain/LangGraph integreert voor agentcontrole, Tree-sitter voor parsing, en de Fulminate/Bennet frameworks voor geautomatiseerd testen.
• Hybride Verificatieaanpak: Het demonstreren van een praktische pipeline waarbij LLM's separation logic-specificaties (CN) genereren en formele testing backends deze valideren, waardoor de noodzaak om de redenering van de LLM te vertrouwen effectief wordt omzeild.
• Benchmark Suite: De constructie van een testsuite bestaande uit 31 annoteerbare C-functies (variërend van eenvoudig eigendom tot complexe loops met globale variabelen en macro's) en 3 inherent onveilige functies ontworpen om het vermogen van de tool om bugs te detecteren te testen.

Experimentele Resultaten

De auteurs evalueerden CNnotator over vijf OpenAI LLM backends (o3, o4-mini, o3-mini, GPT-4.1, en GPT-4o) op de 31 annoteerbare functies.

• Prestaties: Het reasoning model o3 bereikte de hoogste prestaties en annoteerde succesvol 96,8% van de functies (30/31). Het behaalde een succespercentage van 90,3% bij de eerste poging, met een gemiddeld aantal pogingen van slechts 1,10 per succesvolle annotatie.
• Chatmodellen: Zelfs het chatmodel GPT-4o behaalde een succespercentage van 64,5% bij de eerste poging en een totaal succespercentage van 71,0%, waarmee het o3-mini overtrof op het gebied van first-attempt metrics.
• Foutmodi:
  • De tool identificeerde succesvol alle drie de handmatig ingevoegde inherent onveilige functies (use-after-free, double-free) en weigerde deze te annoteren.
  • False positives (annotaties die de tests passeren maar incorrect zijn) werden niet waargenomen tijdens handmatige inspectie van de o3-resultaten.
  • Overmatige permissiviteit van annotaties (waarbij meer eigendom wordt vereist dan nodig) werd opgemerkt als een potentieel probleem, maar werd als acceptabel beschouwd omdat ze nog steeds geldige specificaties opleveren.
• Efficiëntie: Het systeem laat zien dat voor kleine- tot middelgrote programma's, AI-ondersteunde annotatie praktisch wordt, met minimale iteratie vereist voor hoogpresterende modellen.

Betekenis en Claims

Het artikel claimt dat CNnotator de levensvatbaarheid van AI-ondersteunde annotatie voor real-world C-codebases aantoont. Door de patroonherkenningscapaciteiten van LLM's te combineren met de rigoureuze controle van formele testing tools, adresseert de aanpak de "guess-and-check"-aard van formele verificatie.

De auteurs positioneren dit werk als een stap naar:

1. Code Modernisering: Het faciliteren van de migratie van legacy C-code naar veiligere talen (zoals Rust) door eerst geheugensafety-contracten vast te stellen.
2. Automatisering van Verificatie: Het automatiseren van de generatie van geheugensafety-specificaties, een taak die traditioneel handmatig en foutgevoelig is.
3. Praktische Toepasbaarheid: Het aantonen dat huidige modellen de complexiteit van geheugeneigendom in C kunnen aan, met hoge succespercentages en minimale menselijke interventie.

Het artikel blijft bescheiden over de reikwijdte, waarbij wordt opgemerkt dat de benchmarks bestaan uit functies met minder dan 50 regels en eenvoudige control flows, en nog niet de complexe patronen van productiecode zoals type casting of geavanceerde pointer arithmetic dekken. Echter, de resultaten suggereren dat naarmate de capaciteiten van LLM's verbeteren, de techniek kan schalen naar grotere en complexere systemen.