Technische Samenvatting: BODHI: Precieze Inferentie van OS-kernelspecificaties

Probleemstelling

De formele verificatie van besturingssysteemkernen (OS-kernels) is cruciaal voor veiligheidskritieke systemen, maar wordt geblokkeerd door de handmatige inspanning die nodig is om precieze formele specificaties te construeren. Hoewel Large Language Models (LLM's) bekwaamheid hebben aangetoond in algemene codegeneratie, blijft hun vermogen om formele specificaties voor OS-kernels te synthetiseren beperkt. De OSV-Bench-benchmark, die de conversie van C-systeemoproep-implementaties naar Python/Z3-toestandsmachine-specificaties evalueert, onthulde een aanzienlijke prestatiekloof: de hoogst gerapporteerde Pass@1-score onder 12 geëvalueerde modellen was slechts 55,10%.

Deze kloof vloeit voort uit vier primaire uitdagingen:

1. Complexiteit van lange context: Prompts bevatten ongeveer 26K tokens, inclusief programmeermodellen, voorbeelden en doelpcode.
2. Semantische kloof: De taak vereist het vertalen van imperatieve C-kerncode naar declaratieve Z3-Python-specificaties, waarbij fundamenteel verschillende programmeerparadigma's betrokken zijn.
3. Verweven zorgen: C-code mengt vaak pre-conditie (foutcontrole) en post-conditie (toestandsmutatie) logica, die in formele specificaties strikt gescheiden moeten worden.
4. Domeinspecifieke kennis: Kernal-API's omvatten gespecialiseerde patronen (bijvoorbeeld formules voor paginatabelvermeldingen, semantiek van referentietelling, TLB-flushe-operaties) die niet worden gedekt door training van algemene LLM's.

Methodologie: BODHI

De auteurs stellen BODHI voor, een methode voor domeinkennis-prompting die standaard few-shot prompts aanvult met een gestructureerde C-naar-Python Vertalgids. In tegenstelling tot standaard Chain-of-Thought (CoT) of Structured Chain-of-Thought (SCoT), die zich richten op het genereren van tussenliggende redeneerstappen, injecteert BODHI gestructureerd referentiemateriaal in de inputcontext.

Promptstructuur

De BODHI-prompt behoudt de vier componenten van de OSV-Bench-baseline:

1. Systeemprompt (instructies).
2. Programmeermodel (definities van klassen, constanten, functies).
3. Vijf few-shot voorbeelden (paren van C-implementatie naar Z3-specificatie).
4. Doeltaak (functionele beschrijving en C-code).

BODHI voegt een vijfde component toe: een 519-regels tellende Vertalgids die wordt ingevoegd tussen de few-shot voorbeelden en de doeltaak. Deze plaatsing maakt gebruik van het "recency-effect" in transformer-aandacht, waardoor domeinspecifieke patronen het meest toegankelijk zijn tijdens de generatie.

Ontwerp van de Vertalgids

De gids is georganiseerd in 15 categorieën die zijn afgeleid uit een iteratieve analyse van fouten in een model van gemiddeld niveau (Claude Haiku 4.5). Het volgt het principe van Separatie van Zorgen, waarbij onderscheid wordt gemaakt tussen pre-conditie-extractie en post-conditie-generatie. De categorieën zijn gegroepeerd in drie niveaus:

• Niveau 1 (Syntaxis): Behandelt specificatiesjablonen, vertaling van pre-condities (negatie van C-foutcontroles), post-conditiepatronen, syntaxis voor map-velden (onderscheid tussen lezen () en schrijven []), operatorregels en constante voorvoegsels.
• Niveau 2 (Domeinsemantiek): Behandelt formules voor Paginatabelvermeldingen (PTE) (onderscheid tussen x86 en IOMMU), schaduwmetadata, referentietelling, TLB-flushe-operaties, toestandspointer-namen en mapping van veldnamen.
• Niveau 3 (Volledigheid): Adresseert uitbreiding van C-hulpfuncties, beschikbare inventarissen van hulpfuncties en complexe IPC-toestandsmachinepatronen.

Cruciaal is dat de gids fungeert als een "domeinhandboek" dat algemene vertaalregels en illustratieve patronen bevat, geen taakspecifieke oplossingen of volledige code.

Belangrijkste Bijdragen

1. Domeinspecifieke Vertalgids: Een gestructureerde gids met 15 categorieën die C-naar-Python/Z3-vertaalpatronen behandelt, afgeleid van geverifieerde ground-truth specificaties.
2. Uitgebreide Evaluatie: Testen over negen modellen van zes aanbieders (Anthropic, Mistral, Amazon, DeepSeek, Meta, Alibaba), waarbij dichte, mixture-of-experts en redeneringsarchitecturen worden bestreken.
3. Foutanalyse: Een gedetailleerde uiteenzetting die aantoont dat BODHI zowel syntactische als semantische fouten reduceert, met het grootste effect op modellen van gemiddeld niveau die instructievolgende capaciteiten bezitten maar specifieke domeinkennis missen.
4. Nieuwe State-of-the-Art: Het bereiken van een Pass@1 van 96,73% op OSV-Bench, wat aanzienlijk boven de vorige beste score van 55,10% ligt.

Resultaten

• Prestatiewinst: BODHI verbeterde de Pass@1-scores voor elk getest model, met winsten variërend van +11,0% (Qwen3) tot +31,8% (Devstral 2).
• Topprestatie: De configuratie van Claude Opus 4.6 + BODHI behaalde 96,73%, met slechts 8 mislukkingen op 245 taken.
• Foutreductie:
  • Syntaxisfouten: BODHI verminderde syntaxisfouten aanzienlijk, met name type/sort-mismatches en misbruik van API's (bijvoorbeeld het gebruik van haakjes voor schrijfacties op maps). Voor Devstral 2 daalden syntaxisfouten van 31,0% naar 8,2%.
  • Semantische fouten: De gids adresseerde effectief domeinpatroonfouten (bijvoorbeeld onjuiste PTE-formules) en vertaallogica-fouten. Voor Claude Opus 4.6 waren baseline-fouten bijna uitsluitend domeinpatroonfouten; BODHI reduceerde deze tot 2,4%.
• Modelonafhankelijkheid: De verbeteringen waren consistent over diverse architecturen en aanbieders, wat suggereert dat de techniek niet gebonden is aan de trainingsdata van een specifiek modelfamilie.
• Optimalisatie van modellen van gemiddeld niveau: De grootste relatieve winsten werden waargenomen bij modellen van gemiddeld niveau (bijvoorbeeld Devstral 2, Claude Haiku 4.5), die voldoende instructievolgend vermogen hebben om de gids te benutten, maar de intrinsieke domeinkennis van topmodellen missen.

Betekenis en Claims

Het artikel beweert dat injectie van domeinkennis een modelonafhankelijke techniek is die effectief de kloof overbrugt tussen algemene codegeneratie en synthese van formele specificaties. De auteurs betogen dat de bottleneck in OS-kernverificatie niet het redeneervermogen van de LLM is (aangezien redenering-geoptimaliseerde modellen zoals o1 en DeepSeek-R1 geen betere prestaties leverden dan standaard instructievolgende modellen), maar eerder het gebrek aan specifieke vertaalkennis.

Door domeinkennis te structureren in een referentiegids in plaats van te vertrouwen op alleen few-shot voorbeelden, stelt BODHI LLM's in staat om complexe kernsemantiek correct te hanteren, zoals formules voor paginatabelvermeldingen en referentietelling. Het werk toont aan dat een productieve arbeidsverdeling bestaat waarbij menselijke experts de domeingids construeren, en LLM's deze op schaal toepassen om een bijna perfecte synthese van specificaties te bereiken. De auteurs merken op dat de aanpak wordt beperkt door de kosten van gidsconstructie en het vermogen van het model om outputformaten te adhereren, maar dat het een reproduceerbare weg biedt om formele verificatie te verbeteren zonder modelhertraining.