AI-gedreven Beveiligingsaudits
In dit artikel legt auteur Fredrik Dahlgren uit hoe AI-agents de aanpak van beveiligingsaudits transformeren. De kernboodschap is dat AI niet alleen nuttig is voor directe codereviews, maar vooral voor het bouwen van aangepaste tooling en formele modellen die de diepgang van een audit aanzienlijk verhogen.
Casus: De Miden VM Bij de audit van de Miden VM, een zero-knowledge VM met een eigen assemblytaal (MASM), was er nauwelijks developer tooling beschikbaar. Met behulp van AI-agents ontwikkelde het team in zes maanden tijd:
- Een LSP-server en VS Code-extensie voor syntax highlighting en codenavigatie.
- Een decompiler die MASM-procedures vertaalt naar een begrijpelijke tussenrepresentatie.
- Een static analysis engine op basis van abstracte interpretatie om type-validatiefouten op te sporen.
- Een Lean-model voor de formele verificatie van de VM-executor.
Resultaten en Bevindingen De inzet van deze tools leidde tot significante resultaten:
- High-severity bug: Er werd een lek gevonden in de
mod_12289 procedure, waardoor kwaadaardige actoren Falcon-handtekeningen hadden kunnen vervalsen om fondsen te stelen.
- Formele bewijzen: Er werden 95 machine-gecontroleerde correctheidsbewijzen geleverd voor de core library.
- Overige bugs: Er werden subtiele edge cases ontdekt in de 64-bit right-rotation (
rotr) en 256-bit vermenigvuldiging (wrapping_mul).
Conclusie De auteur stelt dat de economie van security-audits is veranderd. Waar het bouwen van specifieke tools vroeger te tijdrovend en riskant was, maken AI-agents dit nu rendabel omdat de kosten beperkt zijn tot tokens. Dit stelt auditors in staat om exploratieve projecten uit te voeren die de veiligheid van software drastisch verbeteren.
Auditing in het tijdperk van (goed genoeg) AI
Veel beveiligingsbedrijven hebben blogposts gepubliceerd waarin ze beschrijven hoe ze hun agent-harness op een codebase hebben gericht en tientallen bugs hebben gevonden (wij zijn daar één van). Deze berichten richten zich echter meestal op agent-gestuurde codereviews, wat slechts één aspect is van hoe wij AI gebruiken in onze beveiligingsaudits. We willen een ander perspectief bieden: nog voordat de codereview begint, stellen agents ons nu in staat om aangepaste tooling en formele modellen te bouwen die de kwaliteit en diepgang van onze reviews verbeteren.
Onlangs hebben we de Miden VM beoordeeld, een nieuwe zero-knowledge VM met een eigen custom assemblytaal en vrijwel geen developer tooling. Ter voorbereiding hebben we zes maanden lang onze agents ingezet om vanaf nul een LSP-server, een decompiler, een static analysis engine en een Lean-model van de VM-executor te bouwen. Deze tools vonden echte beveiligingsproblemen, zoals een niet-gevalideerde input van de prover, waardoor een kwaadaardige prover Falcon-handtekeningen zou kunnen vervalsen en fondsen van Miden-accounthouders zou kunnen stelen. Daarnaast leverde het werk met Lean 95 door de machine gecontroleerde correctheidsbewijzen op, die een groot onderdeel van de Miden core library dekken.
De Miden zkVM auditen
Eind 2025 kwam het Miden-team naar ons toe om delen van hun zero-knowledge VM te laten reviewen vóór de lancering. Een deel van de review was gericht op de Miden core library, die een kleine set cryptografische primitieven bevat geschreven in een custom assemblytaal genaamd Miden assembly (MASM). Dit maakte ons enthousiast, omdat het precies in ons straatje paste: een high-assurance project dat complexe cryptografische code schrijft in een low-level custom assemblytaal die we nog nooit eerder hadden gezien. Tegelijkertijd bracht dit unieke uitdagingen met zich mee.
Afbeelding 1: De linker afbeelding toont een MASM-procedure die de XOR berekent van twee 128-bit waarden (gerepresenteerd als 32-bit limbs). De rechter afbeelding toont dezelfde procedure geïmplementeerd met 32-bit x86 assembly-code.
De Miden VM implementeert een stack-machine architectuur. Dit betekent dat elke instructie opereert op waarden die van de stack worden gelezen, en het resultaat van de instructie vervolgens terug wordt geschreven naar de bovenkant van de stack. Hoewel dit conceptueel eenvoudig is, maakt het code geschreven in MASM uitdagend om te reviewen, aangezien de inputs en outputs van instructies via de stack verlopen en altijd impliciet zijn. Daarnaast bestond er, omdat de Miden VM een volledig nieuwe architectuur is, zeer weinig developer tooling zoals IDE-ondersteuning, Language Server Protocol (LSP) servers en linters.
We wisten dat we zes maanden hadden om ons voor te bereiden op de review, aangezien de implementatie nog niet volledig was. Daarom stelden we onszelf de vraag: "Waar kunnen we onze tijd en tokens aan besteden om ervoor te zorgen dat de review zoveel mogelijk bugs in de codebase opspoort?"
Alle tools bouwen
Omdat MASM geen developer tooling had, begonnen we met de vraag welke tools we beschikbaar zouden willen hebben zodra het project startte. We gebruiken gewoonlijk VS Code voor codereviews, waarbij syntax highlighting en codenavigatie essentieel zijn voor de leesbaarheid en om de datastroom door een codebase te kunnen volgen. Hiervoor hadden we een LSP-server en een bijbehorende VS Code-extensie nodig. Binnen enkele dagen lietten we Claude een werkend prototype bouwen dat de meeste gewenste functionaliteit bood: functies zoals syntax highlighting, goto definition, het vinden van codereferenties en het tonen van procedure-docstrings bij het hoveren. Met deze basis op orde besloten we meer taalspecifieke functies toe te voegen, zoals het tonen van inline instructiedocumentatie en stack-effecten voor individuele instructies.
Afbeelding 2: Het annoteren van de code met inline stack-effecten en instructiedocumentatie helpt om de context-switch te voorkomen die nodig is om instructiesemantiek elders op te zoeken.
Na het bouwen van de LSP-server gingen we nadenken over andere manieren om high-level semantische informatie te verschaffen ter ondersteuning van handmatige en agent-gestuurde reviews. We dachten dat het interessant zou zijn om te kijken of we getrouwe decompilatie voor MASM-procedures in de VS Code-UI konden bieden, om de reviewer te helpen de high-level control flow en data flow van de procedures snel te begrijpen. Voor MASM is dit een moeilijker probleem dan het op het eerste gezicht lijkt. Stack-machine lifting en decompilatie zijn goed bestudeerde problemen, maar het decompileren van handgeschreven MASM blijft moeilijk om een aantal redenen:
- De meeste procedures in de core library hebben geen gedeclareerde signatures, wat betekent dat het aantal inputs en outputs uit de context moet worden afgeleid.
- MASM-procedures conformeren niet aan een goed gedefinieerde calling convention, en het netto stack-effect van dergelijke calls is over het algemeen statisch onmogelijk te bepalen. Dit betekent dat alle analysefouten propageren via de call-chain.
- While-loops hoeven niet stack-neutraal te zijn, wat betekent dat de while-loop conditie in elke iteratie een ander stack-slot kan bezetten. Dit maakt het ook onmogelijk om instructie-inputs te mappen naar stack-slots voor opvolgende instructies.
- Verschillende branches in conditionele statements kunnen verschillende stack-effecten hebben, wat op soortgelijke wijze stack-tracking en signature-inferentie bemoeilijkt.
Dit betekende dat we niet konden verwachten alle MASM-procedures te kunnen decompileren als we ook wilden dat de gedecompileerde output correct was. We richtten ons daarom op het correct decompileren van een goed gedefinieerde subset van MASM. Tijdens de ontwikkeling van de decompiler wisselden we af tussen het gebruik van Claude voor planning en ontwikkeling, en Codex voor codereviews. Telkens wanneer we een nieuwe functie hadden geïmplementeerd, lieten we agents een gerandomiseerde set procedures uit de core library decompileren en het resultaat vergelijken met de originele MASM om regressies op te sporen. Eventuele problemen werden toegevoegd als regressietests om door het model te worden opgelost.
Afbeelding 3: De eqz procedure, die test of een 256-bit integer (gerepresenteerd als acht 32-bit limbs) gelijk is aan nul, samen met de bijbehorende gedecompileerde pseudocode.
De decompiler vormde de grootste inspanning van de tooling-ontwikkeling voor dit project, met meer dan 100 AI-gegenereerde commits over meerdere maanden. Het grootste voordeel van dit werk bleken de interne analyseframeworks en de intermediate representation (tussenrepresentatie) van de decompiler te zijn, die we konden hergebruiken voor statische analyse, in plaats van de volledige decompilatie-pipeline.
Met de decompiler op orde hadden we toegang tot een tussenrepresentatie van elke procedure, waarbij instructie-inputs en -outputs waren ingevuld als expressies. Hierdoor konden we alle standaard static analysis machinery (zoals data flow analyse) toepassen op het probleem van het vinden van bugs in de MASM-code. We gebruikten dit om een aantal analyse-passes over de tussenrepresentatie uit te voeren, om vragen te beantwoorden zoals:
- Worden prover-supplied advice-waarden[^1] zoals resten (remainders) en modulaire inversen correct gevalideerd?
- Worden type-constraints (bijv. of een input een 32-bit integer of een boolean is) afgedwongen?
- Worden lokale variabelen geïnitialiseerd over alle executiepaden?
Een manier om deze kwesties te onderzoeken is abstracte interpretatie. Het idee achter deze techniek is eenvoudig: in plaats van het programma uit te voeren met echte getallen, volgt de analyse de typen waarden die op elk moment op de stack kunnen staan, zoals "een 32-bit integer" of "onbekend". Het doorloopt de code herhaaldelijk totdat er geen nieuwe informatie meer wordt gevonden. Omdat het altijd elke mogelijke waarde bijhoudt (met een beetje extra ruimte), kan het nooit een echt scenario missen. Als een check dus slaagt in de analyse, is gegarandeerd dat deze standhoudt in elke werkelijke run van het programma.
We gebruikten Claude en Codex om een algemene abstracte interpretatie-engine te bouwen, en implementeerden vervolgens een aantal concrete analyse-passes hierbovenop. We lieten de agents schakelen tussen ontwikkeling en codereview, zoals eerder beschreven. Ook lieten we de agents command-line interfaces ontwerpen en bouwen voor zowel de decompiler als een nieuwe MASM-linter, zodat de nieuwe tools ook beschikbaar werden voor agent-gestuurde codereview-workflows.
Alle bugs vinden
Tijdens de eigenlijke review identificeerden deze analyses meer dan 400 unieke locaties[^2] waar type-validatie verbeterd kon worden (allemaal bereikbaar vanuit de publieke API van de library), evenals één high-severity bevinding.
Afbeelding 4: De remainder wordt gelezen van de advice stack, maar wordt niet gevalideerd om te garanderen dat het een geldige 64-bit integer is.
Het high-severity probleem werd veroorzaakt door een onvoldoende beperkte advice-waarde in de mod12289 procedure, die een 64-bit waarde reduceert modulo 12289, waarbij een quotiënt en een restwaarde (remainder) als advice-waarden door de prover worden geleverd. Het quotiënt wordt gecontroleerd om te garanderen dat het een geldige 64-bit waarde is (gerepresenteerd als twee 32-bit limbs), maar de restwaarde wordt nooit gevalideerd voordat deze wordt doorgegeven aan de 32-bit instructie u32overflowingsub. Door het quotiënt en de restwaarde zorgvuldig te variëren zodat ze nog steeds voldeden aan de beperkingen die door de aftrekking werden opgelegd, ontdekten we dat het mogelijk was dat mod_12289 een waarde teruggaf die niet de correcte restwaarde was. Een kwaadaardige prover zou dit kunnen exploiteren om Falcon-handtekeningen te vervalsen en elk Miden-account dat wordt beheerd door een Falcon-keypair leeg te trekken.
Maar wat als er geen bugs zijn?
Al dit werk betekende dat we een uitgebreide set tools hadden om zowel handmatige als agent-gestuurde codereviews te ondersteunen bij aanvang van de audit. We hadden echter ook tijd gehad om na te denken over andere manieren om het handmatige reviewproces te ondersteunen. Bijvoorbeeld: als de procedures in de core library correct waren geïmplementeerd en geen bugs bevatten, zou het dan mogelijk zijn om dit te bewijzen met een proof assistant zoals Lean?
Het blijkt dat de Miden VM zeer geschikt is voor formele modellering, aangezien de instructieset klein is en de meeste instructies vrij zijn van side-effects. Om MASM formeel te modelleren, begonnen we met het implementeren van een minimale Miden VM-executor in Lean, en lieten we Claude een automatische vertaler bouwen van MASM-procedures naar Lean. Tijdens de review lieten we meerdere agents parallel werken om de correctheid van zoveel mogelijk procedures in de library te bewijzen. Omdat de Lean-kernel kon valideren dat de gegenereerde bewijzen correct waren, hoefden we alleen de theorem statements handmatig te auditen om er zeker van te zijn dat elk theorema de juiste correctheidseigenschap voor de bijbehorende procedure bewees. Om ervoor te zorgen dat de theorema's gemakkelijk te reviewen waren, introduceerden we Lean-types voor veldelementen en de integer-types die in de core library zijn geïmplementeerd. Dit betekende dat op hoog niveau de meeste correctheidseigenschappen in de volgende vorm konden worden uitgedrukt:
Als de stack wordt gegeven door $[x1, x2, x3, \dots, xn, \dots]$ en we voeren de procedure $P$ uit, dan termineert $P$ en wordt de stack gegeven door $[P(x1, x2, x3, \dots, xn), \dots]$.
Afbeelding 5: High-level statement van correctheid voor de procedure $P$ met $n$ argumenten.
Onze agent-gestuurde formele modelleringsinspanningen resulteerden in 95 correctheidsbewijzen die alle binaire rekencomponenten van de core library dekten. Dit werk identificeerde ook twee subtiele bugs die de bestaande unit test suite niet had opgemerkt. De eerste was een edge case in de 64-bit right-rotation rotr, die incorrect reageerde op grote inputs groter dan de Goldilocks-prime als de rotational shift een veelvoud van 32 was. De tweede was een probleem in de 256-bit vermenigvuldiging wrapping_mul, die waarden van de caller van de stack verwijderde voordat deze terugkeerde.
Afbeelding 6: Handmatige review identificeerde dat het correctheidsbewijs voor de 64-bit rotr procedure een aanvullende aanname vereiste (dat shift mod 32 $\neq 0$) om het bewijs te laten slagen.
Waarom we dit twee jaar geleden niet hadden kunnen doen
De tools die we ontwikkelden voorafgaand aan deze opdracht, en de Lean-libraries en bewijzen die tijdens de review zijn gegenereerd, zijn allemaal zijprojecten waar we één of twee jaar geleden geen tijd of middelen aan hadden kunnen besteden. Projecten als deze zijn vaak sterk exploratief van aard, en de eindresultaten en potentiële opbrengsten zijn moeilijk te voorspellen. In de praktijk betekent dit dat het lastig is om klanten vooraf te overtuigen hiervan. Echter, in het afgelopen jaar zijn agents goed genoeg geworden om dergelijke niet-essentiële projecten uit te voeren met slechts licht toezicht, wat de economie van welke projecten de moeite waard zijn volledig heeft veranderd. Tegenwoordig kosten mislukte zijprojecten alleen tokens.
Bij Miden waren de voordelen van al dit voorbereidende werk duidelijk. De LSP-server en de static analysis engine verbeterden onze handmatige review-dekking, versterkten agent-gestuurde reviews en identificeerden echte beveiligingsproblemen in de codebase die tot miljoenen dollars aan verloren fondsen hadden kunnen leiden. De AI-gegenereerde Lean-correctheidsbewijzen verbeterden daarnaast de zekerheid over een groot en fundamenteel onderdeel van de library, waardoor het team met vertrouwen verder kon bouwen. Het team heeft de static analysis engine die voor de review is ontwikkeld overgenomen, wat betekent dat ons zijproject nu ook zal helpen bij het beveiligen van toekomstige updates van de Miden core library.
***
[^1]: Dit zijn vooraf berekende inputs die via een aparte advice-stack door de prover worden geleverd en zorgvuldig moeten worden gevalideerd. [^2]: De meeste van deze bevindingen waren te wijten aan het feit dat bijna alle procedures in de core library deel uitmaakten van de publieke API, wat betekende dat externe ontwikkelaars ze zonder proper validatie konden aanroepen.
Auditing in het tijdperk van (goed genoeg) AI
Veel beveiligingsbedrijven hebben blogposts gepubliceerd waarin ze beschrijven hoe ze hun agent-harness op een codebase hebben gericht en tientallen bugs hebben gevonden (wij zijn daar één van). Deze berichten richten zich echter meestal op agent-gestuurde codereviews, wat slechts één aspect is van hoe wij AI gebruiken in onze beveiligingsaudits. We willen een ander perspectief bieden: nog voordat de codereview begint, stellen agents ons nu in staat om aangepaste tooling en formele modellen te bouwen die de kwaliteit en diepgang van onze reviews verbeteren.
Onlangs hebben we de Miden VM beoordeeld, een nieuwe zero-knowledge VM met een eigen custom assemblytaal en vrijwel geen developer tooling. Ter voorbereiding hebben we zes maanden lang onze agents ingezet om vanaf nul een LSP-server, een decompiler, een static analysis engine en een Lean-model van de VM-executor te bouwen. Deze tools vonden echte beveiligingsproblemen, zoals een niet-gevalideerde input van de prover, waardoor een kwaadaardige prover Falcon-handtekeningen zou kunnen vervalsen en fondsen van Miden-accounthouders zou kunnen stelen. Daarnaast leverde het werk met Lean 95 door de machine gecontroleerde correctheidsbewijzen op, die een groot onderdeel van de Miden core library dekken.
De Miden zkVM auditen
Eind 2025 kwam het Miden-team naar ons toe om delen van hun zero-knowledge VM te laten reviewen vóór de lancering. Een deel van de review was gericht op de Miden core library, die een kleine set cryptografische primitieven bevat geschreven in een custom assemblytaal genaamd Miden assembly (MASM). Dit maakte ons enthousiast, omdat het precies in ons straatje paste: een high-assurance project dat complexe cryptografische code schrijft in een low-level custom assemblytaal die we nog nooit eerder hadden gezien. Tegelijkertijd bracht dit unieke uitdagingen met zich mee.
Afbeelding 1: De linker afbeelding toont een MASM-procedure die de XOR berekent van twee 128-bit waarden (gerepresenteerd als 32-bit limbs). De rechter afbeelding toont dezelfde procedure geïmplementeerd met 32-bit x86 assembly-code.
De Miden VM implementeert een stack-machine architectuur. Dit betekent dat elke instructie opereert op waarden die van de stack worden gelezen, en het resultaat van de instructie vervolgens terug wordt geschreven naar de bovenkant van de stack. Hoewel dit conceptueel eenvoudig is, maakt het code geschreven in MASM uitdagend om te reviewen, aangezien de inputs en outputs van instructies via de stack verlopen en altijd impliciet zijn. Daarnaast bestond er, omdat de Miden VM een volledig nieuwe architectuur is, zeer weinig developer tooling zoals IDE-ondersteuning, Language Server Protocol (LSP) servers en linters.
We wisten dat we zes maanden hadden om ons voor te bereiden op de review, aangezien de implementatie nog niet volledig was. Daarom stelden we onszelf de vraag: "Waar kunnen we onze tijd en tokens aan besteden om ervoor te zorgen dat de review zoveel mogelijk bugs in de codebase opspoort?"
Alle tools bouwen
Omdat MASM geen developer tooling had, begonnen we met de vraag welke tools we beschikbaar zouden willen hebben zodra het project startte. We gebruiken gewoonlijk VS Code voor codereviews, waarbij syntax highlighting en codenavigatie essentieel zijn voor de leesbaarheid en om de datastroom door een codebase te kunnen volgen. Hiervoor hadden we een LSP-server en een bijbehorende VS Code-extensie nodig. Binnen enkele dagen lietten we Claude een werkend prototype bouwen dat de meeste gewenste functionaliteit bood: functies zoals syntax highlighting, goto definition, het vinden van codereferenties en het tonen van procedure-docstrings bij het hoveren. Met deze basis op orde besloten we meer taalspecifieke functies toe te voegen, zoals het tonen van inline instructiedocumentatie en stack-effecten voor individuele instructies.
Afbeelding 2: Het annoteren van de code met inline stack-effecten en instructiedocumentatie helpt om de context-switch te voorkomen die nodig is om instructiesemantiek elders op te zoeken.
Na het bouwen van de LSP-server gingen we nadenken over andere manieren om high-level semantische informatie te verschaffen ter ondersteuning van handmatige en agent-gestuurde reviews. We dachten dat het interessant zou zijn om te kijken of we getrouwe decompilatie voor MASM-procedures in de VS Code-UI konden bieden, om de reviewer te helpen de high-level control flow en data flow van de procedures snel te begrijpen. Voor MASM is dit een moeilijker probleem dan het op het eerste gezicht lijkt. Stack-machine lifting en decompilatie zijn goed bestudeerde problemen, maar het decompileren van handgeschreven MASM blijft moeilijk om een aantal redenen:
- De meeste procedures in de core library hebben geen gedeclareerde signatures, wat betekent dat het aantal inputs en outputs uit de context moet worden afgeleid.
- MASM-procedures conformeren niet aan een goed gedefinieerde calling convention, en het netto stack-effect van dergelijke calls is over het algemeen statisch onmogelijk te bepalen. Dit betekent dat alle analysefouten propageren via de call-chain.
- While-loops hoeven niet stack-neutraal te zijn, wat betekent dat de while-loop conditie in elke iteratie een ander stack-slot kan bezetten. Dit maakt het ook onmogelijk om instructie-inputs te mappen naar stack-slots voor opvolgende instructies.
- Verschillende branches in conditionele statements kunnen verschillende stack-effecten hebben, wat op soortgelijke wijze stack-tracking en signature-inferentie bemoeilijkt.
Dit betekende dat we niet konden verwachten alle MASM-procedures te kunnen decompileren als we ook wilden dat de gedecompileerde output correct was. We richtten ons daarom op het correct decompileren van een goed gedefinieerde subset van MASM. Tijdens de ontwikkeling van de decompiler wisselden we af tussen het gebruik van Claude voor planning en ontwikkeling, en Codex voor codereviews. Telkens wanneer we een nieuwe functie hadden geïmplementeerd, lieten we agents een gerandomiseerde set procedures uit de core library decompileren en het resultaat vergelijken met de originele MASM om regressies op te sporen. Eventuele problemen werden toegevoegd als regressietests om door het model te worden opgelost.
Afbeelding 3: De eqz procedure, die test of een 256-bit integer (gerepresenteerd als acht 32-bit limbs) gelijk is aan nul, samen met de bijbehorende gedecompileerde pseudocode.
De decompiler vormde de grootste inspanning van de tooling-ontwikkeling voor dit project, met meer dan 100 AI-gegenereerde commits over meerdere maanden. Het grootste voordeel van dit werk bleken de interne analyseframeworks en de intermediate representation (tussenrepresentatie) van de decompiler te zijn, die we konden hergebruiken voor statische analyse, in plaats van de volledige decompilatie-pipeline.
Met de decompiler op orde hadden we toegang tot een tussenrepresentatie van elke procedure, waarbij instructie-inputs en -outputs waren ingevuld als expressies. Hierdoor konden we alle standaard static analysis machinery (zoals data flow analyse) toepassen op het probleem van het vinden van bugs in de MASM-code. We gebruikten dit om een aantal analyse-passes over de tussenrepresentatie uit te voeren, om vragen te beantwoorden zoals:
- Worden prover-supplied advice-waarden[^1] zoals resten (remainders) en modulaire inversen correct gevalideerd?
- Worden type-constraints (bijv. of een input een 32-bit integer of een boolean is) afgedwongen?
- Worden lokale variabelen geïnitialiseerd over alle executiepaden?
Een manier om deze kwesties te onderzoeken is abstracte interpretatie. Het idee achter deze techniek is eenvoudig: in plaats van het programma uit te voeren met echte getallen, volgt de analyse de typen waarden die op elk moment op de stack kunnen staan, zoals "een 32-bit integer" of "onbekend". Het doorloopt de code herhaaldelijk totdat er geen nieuwe informatie meer wordt gevonden. Omdat het altijd elke mogelijke waarde bijhoudt (met een beetje extra ruimte), kan het nooit een echt scenario missen. Als een check dus slaagt in de analyse, is gegarandeerd dat deze standhoudt in elke werkelijke run van het programma.
We gebruikten Claude en Codex om een algemene abstracte interpretatie-engine te bouwen, en implementeerden vervolgens een aantal concrete analyse-passes hierbovenop. We lieten de agents schakelen tussen ontwikkeling en codereview, zoals eerder beschreven. Ook lieten we de agents command-line interfaces ontwerpen en bouwen voor zowel de decompiler als een nieuwe MASM-linter, zodat de nieuwe tools ook beschikbaar werden voor agent-gestuurde codereview-workflows.
Alle bugs vinden
Tijdens de eigenlijke review identificeerden deze analyses meer dan 400 unieke locaties[^2] waar type-validatie verbeterd kon worden (allemaal bereikbaar vanuit de publieke API van de library), evenals één high-severity bevinding.
Afbeelding 4: De remainder wordt gelezen van de advice stack, maar wordt niet gevalideerd om te garanderen dat het een geldige 64-bit integer is.
Het high-severity probleem werd veroorzaakt door een onvoldoende beperkte advice-waarde in de mod12289 procedure, die een 64-bit waarde reduceert modulo 12289, waarbij een quotiënt en een restwaarde (remainder) als advice-waarden door de prover worden geleverd. Het quotiënt wordt gecontroleerd om te garanderen dat het een geldige 64-bit waarde is (gerepresenteerd als twee 32-bit limbs), maar de restwaarde wordt nooit gevalideerd voordat deze wordt doorgegeven aan de 32-bit instructie u32overflowingsub. Door het quotiënt en de restwaarde zorgvuldig te variëren zodat ze nog steeds voldeden aan de beperkingen die door de aftrekking werden opgelegd, ontdekten we dat het mogelijk was dat mod_12289 een waarde teruggaf die niet de correcte restwaarde was. Een kwaadaardige prover zou dit kunnen exploiteren om Falcon-handtekeningen te vervalsen en elk Miden-account dat wordt beheerd door een Falcon-keypair leeg te trekken.
Maar wat als er geen bugs zijn?
Al dit werk betekende dat we een uitgebreide set tools hadden om zowel handmatige als agent-gestuurde codereviews te ondersteunen bij aanvang van de audit. We hadden echter ook tijd gehad om na te denken over andere manieren om het handmatige reviewproces te ondersteunen. Bijvoorbeeld: als de procedures in de core library correct waren geïmplementeerd en geen bugs bevatten, zou het dan mogelijk zijn om dit te bewijzen met een proof assistant zoals Lean?
Het blijkt dat de Miden VM zeer geschikt is voor formele modellering, aangezien de instructieset klein is en de meeste instructies vrij zijn van side-effects. Om MASM formeel te modelleren, begonnen we met het implementeren van een minimale Miden VM-executor in Lean, en lieten we Claude een automatische vertaler bouwen van MASM-procedures naar Lean. Tijdens de review lieten we meerdere agents parallel werken om de correctheid van zoveel mogelijk procedures in de library te bewijzen. Omdat de Lean-kernel kon valideren dat de gegenereerde bewijzen correct waren, hoefden we alleen de theorem statements handmatig te auditen om er zeker van te zijn dat elk theorema de juiste correctheidseigenschap voor de bijbehorende procedure bewees. Om ervoor te zorgen dat de theorema's gemakkelijk te reviewen waren, introduceerden we Lean-types voor veldelementen en de integer-types die in de core library zijn geïmplementeerd. Dit betekende dat op hoog niveau de meeste correctheidseigenschappen in de volgende vorm konden worden uitgedrukt:
Als de stack wordt gegeven door $[x1, x2, x3, \dots, xn, \dots]$ en we voeren de procedure $P$ uit, dan termineert $P$ en wordt de stack gegeven door $[P(x1, x2, x3, \dots, xn), \dots]$.
Afbeelding 5: High-level statement van correctheid voor de procedure $P$ met $n$ argumenten.
Onze agent-gestuurde formele modelleringsinspanningen resulteerden in 95 correctheidsbewijzen die alle binaire rekencomponenten van de core library dekten. Dit werk identificeerde ook twee subtiele bugs die de bestaande unit test suite niet had opgemerkt. De eerste was een edge case in de 64-bit right-rotation rotr, die incorrect reageerde op grote inputs groter dan de Goldilocks-prime als de rotational shift een veelvoud van 32 was. De tweede was een probleem in de 256-bit vermenigvuldiging wrapping_mul, die waarden van de caller van de stack verwijderde voordat deze terugkeerde.
Afbeelding 6: Handmatige review identificeerde dat het correctheidsbewijs voor de 64-bit rotr procedure een aanvullende aanname vereiste (dat shift mod 32 $\neq 0$) om het bewijs te laten slagen.
Waarom we dit twee jaar geleden niet hadden kunnen doen
De tools die we ontwikkelden voorafgaand aan deze opdracht, en de Lean-libraries en bewijzen die tijdens de review zijn gegenereerd, zijn allemaal zijprojecten waar we één of twee jaar geleden geen tijd of middelen aan hadden kunnen besteden. Projecten als deze zijn vaak sterk exploratief van aard, en de eindresultaten en potentiële opbrengsten zijn moeilijk te voorspellen. In de praktijk betekent dit dat het lastig is om klanten vooraf te overtuigen hiervan. Echter, in het afgelopen jaar zijn agents goed genoeg geworden om dergelijke niet-essentiële projecten uit te voeren met slechts licht toezicht, wat de economie van welke projecten de moeite waard zijn volledig heeft veranderd. Tegenwoordig kosten mislukte zijprojecten alleen tokens.
Bij Miden waren de voordelen van al dit voorbereidende werk duidelijk. De LSP-server en de static analysis engine verbeterden onze handmatige review-dekking, versterkten agent-gestuurde reviews en identificeerden echte beveiligingsproblemen in de codebase die tot miljoenen dollars aan verloren fondsen hadden kunnen leiden. De AI-gegenereerde Lean-correctheidsbewijzen verbeterden daarnaast de zekerheid over een groot en fundamenteel onderdeel van de library, waardoor het team met vertrouwen verder kon bouwen. Het team heeft de static analysis engine die voor de review is ontwikkeld overgenomen, wat betekent dat ons zijproject nu ook zal helpen bij het beveiligen van toekomstige updates van de Miden core library.
***
[^1]: Dit zijn vooraf berekende inputs die via een aparte advice-stack door de prover worden geleverd en zorgvuldig moeten worden gevalideerd. [^2]: De meeste van deze bevindingen waren te wijten aan het feit dat bijna alle procedures in de core library deel uitmaakten van de publieke API, wat betekende dat externe ontwikkelaars ze zonder proper validatie konden aanroepen.
Groetjes,