A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

Dit paper introduceert Preguss, een modulair raamwerk dat statische analyse en deductieve verificatie combineert met LLM-ondersteunde synthesese om formele specificaties te genereren en zo de verificatie van grote, real-world programma's met meer dan 1000 regels code aanzienlijk te automatiseren en de menselijke inspanning met 80,6% tot 88,9% te verminderen.

De kern

Stel je voor dat je een gigantisch, ingewikkeld machinekamer hebt, vol met duizenden schroeven, buizen en draden. Dit is een groot computerprogramma (zoals de software voor een ruimteschip of een besturingssysteem). Je wilt er 100% zeker van zijn dat deze machine nooit zal crashen, niet zal exploderen en geen fouten zal maken terwijl hij draait.

In de wereld van software noemen we dit verificatie. Het probleem is: deze machines zijn zo groot dat zelfs de slimste computers (en menselijke experts) het moeilijk vinden om alles in één keer te controleren. Ze raken de draad kwijt of zien kleine foutjes over het hoofd.

Deze paper introduceert Preguss, een slimme nieuwe manier om dit probleem op te lossen. Het is als het hebben van een super-intelligente assistent (een AI) die samenwerkt met een strenge inspecteur.

Hier is hoe het werkt, vertaald naar alledaagse taal:

1. Het Probleem: De "Grote Boek" Uitdaging

Stel je voor dat je een boek van 1000 pagina's moet controleren op fouten.

• De oude manier: Je probeert het hele boek in één keer te lezen. Je hersenen (of de computer) raken overbelast. Je mist details.
• De AI-problematiek: Moderne AI's (zoals ChatGPT) zijn slim, maar ze kunnen niet goed een heel boek in één keer "in hun hoofd" houden. Ze raken de draad kwijt als het te groot is. Ze kunnen ook niet goed begrijpen hoe hoofdstuk A precies invloed heeft op hoofdstuk Z, als die ver weg staan.

2. De Oplossing: Preguss (De Slimme Splits-En-Heers Strategie)

Preguss gebruikt een slimme truc: "Splits en Heers". In plaats van het hele boek in één keer te lezen, breekt het het probleem op in kleine, beheersbare stukjes.

Het proces heeft twee hoofdfases:

Fase 1: De Inspecteur vindt de "Gevaarlijke Plekken" (De Delen)

Eerst laat Preguss een strenge, traditionele inspecteur (een "statische analyzer") het programma scannen. Deze inspecteur is niet slim, maar wel heel grondig. Hij zegt: "Hier, bij schroef 42, zou er een probleem kunnen zijn. Misschien breekt er iets."

In plaats van dat de AI nu het hele programma moet uitleggen, zegt Preguss: "Oké, we focussen alleen op schroef 42 en de buizen die direct daarheen lopen."

• Analogie: Het is alsof je een grote stad hebt. In plaats van te proberen het hele verkeer in de stad te regelen, zegt de AI: "We focussen ons vandaag alleen op het kruispunt bij de school. Wat gebeurt er daar?"

Fase 2: De AI bouwt de "Regels" (Het Veroveren)

Nu komt de slimme AI (het LLM) in actie, maar dan op een heel specifieke manier.

• De AI krijgt alleen de informatie over dat ene kruispunt (schroef 42) en de directe omgeving.
• De AI moet een regelschrift (een specificatie) schrijven dat zegt: "Als je hier komt, moet je zeker weten dat de snelheid onder de 50 km/u is."
• De slimme truc: De AI kijkt niet alleen naar de plek zelf, maar ook naar de buizen die daar naartoe lopen (andere functies). Als die buizen een verkeerde druk hebben, moet de AI dat ook in de regels zetten.

Als de AI een goede regel schrijft, controleert de strenge inspecteur of het klopt.

• Klopt het? Geweldig! We zijn een stap verder.
• Klopt het niet? De inspecteur geeft feedback: "Nee, die regel is te streng, of te vaag." De AI leert van deze feedback en probeert het opnieuw. Dit gaat door tot het perfect is.

3. Waarom is dit zo speciaal?

In het verleden probeerden AI's vaak het hele programma in één keer te "begrijpen" en regels te schrijven. Dat werkte niet goed voor grote projecten.

Preguss werkt als een bouwmeester die een gigantisch kasteel bouwt:

• Hij bouwt niet het hele kasteel in één dag.
• Hij bouwt eerst de fundering van de toren.
• Dan de muren van die toren.
• Dan het dak.
• En hij gebruikt de regels van de vorige stap om de volgende stap te bouwen.

Dit betekent dat Preguss programma's van 1000 regels (of zelfs meer) kan verifiëren, terwijl andere methoden al vastliepen bij 100 regels.

4. Het Resultaat in het Dagelijks Leven

De auteurs hebben dit getest op echte, grote software, zoals:

• De software voor een ruimteschip (SAMCODE).
• Besturingssystemen voor internet van dingen (Contiki).

Wat deden ze?

1. Minder menselijk werk: Mensen moesten 80% tot 89% minder tijd besteden aan het handmatig controleren van regels. De AI deed het zware werk.
2. Echte fouten gevonden: In de ruimteschipssoftware vond Preguss 6 echte fouten die eerder waren gemist. Dit zijn fouten die hadden kunnen leiden tot een crash of een mislukte missie.
3. Schaalbaarheid: Het werkt ook voor programma's die duizenden regels lang zijn.

Samenvatting in één zin

Preguss is als een slimme teamleider die een gigantisch, complex project opdeelt in kleine, makkelijke taken, waarbij een AI en een strenge inspecteur samenwerken om elke kleine taak perfect te maken, zodat het hele grote project veilig en foutloos is.

Het maakt het mogelijk om software te bouwen die we kunnen vertrouwen, zelfs als die software enorm groot en complex is.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het artikel "A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs" in het Nederlands.

Titel

Een verhaal van 1001 LoC: Potentiële Runtime Error-geleide Specificatiesynthese voor het Verifiëren van Groot-Schalige Programma's

1. Het Probleem

Het volledig geautomatiseerde verifiëren van groot-schalige software- en hardware-systemen is een van de grootste uitdagingen binnen formele methoden.

• Runtime Errors (RTE's): Fouten zoals deling door nul, bufferoverlopen en dereferentie van null pointers leiden tot ongedefinieerd gedrag (UB) en kunnen catastrofaal zijn, vooral in veiligheidskritieke systemen.
• Beperkingen van bestaande tools:
  • Statische analyse: Tools gebaseerd op abstracte interpretatie (zoals Frama-C/Eva) kunnen RTE's detecteren, maar genereren vaak veel "false positives" (valse alarmen) vanwege hun benaderende aard. Het handmatig oplossen hiervan is moeilijk.
  • Deductieve verificatie: Tools zoals Frama-C/Wp vereisen formele specificaties (precondities, postcondities, loop-invarianten) om correctheid te bewijzen. Het genereren van deze specificaties is echter nog steeds sterk afhankelijk van menselijke expertise.
• Beperkingen van LLM's (Large Language Models): Hoewel LLM's veelbelovend zijn voor het genereren van specificaties, falen ze bij groot-schalige programma's (>1000 regels code) vanwege:
  1. Context-limieten: Ze kunnen het volledige programma niet in één keer verwerken.
  2. Interprocedurale complexiteit: Ze hebben moeite om complexe specificaties te genereren die over meerdere functies heen gaan (bijv. contracten tussen caller en callee).
  3. Over-constraining: Ze genereren soms te strenge precondities die valse alarmen veroorzaken.

2. Methodologie: Preguss

Het artikel introduceert Preguss, een modulair, fijnmazig raamwerk dat statische analyse en deductieve verificatie combineert via een "divide-and-conquer" strategie. Het doel is het automatisch synthetiseren van formele specificaties om RTE-vrijheid te bewijzen.

Het proces bestaat uit twee fasen:

Fase 1: Potentiële RTE-geleide Constructie en Prioritering (Divide)

• Statische Analyse: Een statische analyzer (bijv. Frama-C/Rte) scant het programma en genereert RTE-asserties (guard assertions) die potentiële fouten markeren.
• V-Unit Constructie: Het monolithische verificatieprobleem wordt opgesplitst in beheersbare eenheden, genaamd V-Units. Elke V-Unit bevat:
  • Een guard assertion (de te verifiëren RTE).
  • Een gefilterde programmaslice: de host-functie en alle "callee"-functies die direct of indirect worden aangeroepen.
• Prioritering: De V-Units worden in een wachtrij geplaatst volgens een strikte volgorde:
  • Bottom-up: Eerst worden de "callee"-functies verifieerd, zodat hun contracten beschikbaar zijn voor de "caller".
  • Locatie-gebaseerd: Binnen dezelfde functie worden asserties verwerkt op basis van hun locatie in de code.
  • Dit voorkomt dat de context voor de LLM te groot wordt en zorgt voor een logische volgorde van specificatiegeneratie.

Fase 2: Fijnmazige Interprocedurale Specificatiesynthese (Conquer)

Voor elke V-Unit in de wachtrij gebruikt Preguss een iteratief proces met een LLM en een deductieve verifier:

1. Verificatie: De verifier probeert de guard assertion te bewijzen met de huidige specificaties.
2. Feedback-geleid Refinement: Als de verifier faalt (status "unknown"), gebruikt hij de bewijsverplichtingen (proof obligations) als feedback.
3. LLM-Generatie: De LLM genereert nieuwe specificaties op basis van deze feedback en de context:
   • Host-functie: Genereert precondities en loop-invarianten voor de functie die de assertie bevat.
   • Callee-functies: Genereert uitsluitend postcondities voor aangeroepen functies. Cruciaal: Het genereert geen precondities voor callees om te voorkomen dat er te strenge (over-constrained) precondities ontstaan die valse alarmen veroorzaken.
4. Validatie en Correctie: De gegenereerde specificaties worden gecontroleerd op syntactische en semantische geldigheid. Onjuiste specificaties worden gecorrigeerd of verworpen.
5. Iteratie: Dit proces herhaalt zich totdat de assertie bewezen is of een maximum aantal iteraties is bereikt. Als het niet lukt, wordt de assertie gemarkeerd als een "hypotheek" die menselijke review vereist.

3. Belangrijkste Bijdragen

• Concept: Formalisering van Potentiële RTE-geleide Specificatiesynthese. Het gebruik van asserties van statische analyse als leidraad voor LLM's om de juiste specificaties te genereren.
• Preguss Framework: Het eerste geautomatiseerde methode dat in staat is om RTE-vrijheid te bewijzen voor real-world programma's met meer dan 1.000 regels code (LoC) met marginaal menselijk ingrijpen.
• Dataset: Het creëren van een open-source dataset met real-world C-programma's, geannoteerd met specificaties gegenereerd door Preguss en door experts.
• Implementatie en Evaluatie: Een volledige implementatie bovenop Frama-C/Wp en Frama-C/Eva, met uitgebreide experimenten die de superioriteit tonen ten opzichte van state-of-the-art methoden.

4. Resultaten

De evaluatie omvatte benchmarks zoals Frama-C-Problems en vier real-world projecten (Contiki, X509-parser, SAMCODE, Atomthreads).

• Vergelijking met Baselines: Preguss presteert aanzienlijk beter dan bestaande LLM-methoden (zoals AutoSpec).
  • Op de Frama-C-Problems benchmark (51 programma's) slaagde Preguss in 79,7% van de gevallen, tegenover 32,7% voor AutoSpec en 41,8% voor een verbeterde versie (AutoSpecRte).
• Schaalbaarheid: Preguss slaagde erin om RTE-vrijheid te verifiëren voor programma's tot 1.451 regels code (Atomthreads) en 1.280 regels code (SAMCODE).
• Efficiëntie:
  • Menselijke Inspanning: Er was een reductie van 80,6% tot 88,9% in menselijke verificatie-inspanning (gemeten aan het aantal handmatig aangepaste specificaties).
  • Tijd: De tool verwerkte grote projecten binnen enkele uren, terwijl baselines vaak faalden of uren nodig hadden zonder resultaat.
• Gevonden Fouten: In het spacecraft-besturingssysteem (SAMCODE) identificeerde Preguss 6 bevestigde echte RTE's (ongeïnitieerde variabele-toegang) die door de ontwikkelaars werden bevestigd als logische bugs.

5. Betekenis en Impact

• Doorbraak in Automatisering: Preguss toont aan dat het mogelijk is om formele verificatie van groot-schalige, complexe C-programma's te automatiseren, een gebied dat traditioneel als te moeilijk werd beschouwd voor volledige automatisering.
• Synergie: Het raamwerk lost het probleem van LLM-contextlimieten op door het probleem op te splitsen in kleine, gerichte eenheden (V-Units) en gebruikt statische analyse om de LLM te "sturen" naar de juiste context.
• Praktische Toepasbaarheid: De significante reductie in menselijke inspanning maakt formele verificatie haalbaar voor industriële toepassingen, zoals in de ruimtevaart (SAMCODE) en embedded systemen.
• Veiligheid: Door het automatisch opsporen van zowel valse alarmen als echte runtime errors, draagt het direct bij aan de betrouwbaarheid van veiligheidskritieke software.

Kortom, Preguss biedt een robuuste oplossing voor de schaalbaarheidsproblemen in formele verificatie door slimme integratie van statische analyse, deductieve verificatie en Large Language Models.