Claude bewijst crashvrij gedrag van 239 fuzz-testdoelen

Claude levert machinaal controleerbare bewijzen dat 239 fuzz-testdoelen uit 123 open sourcebibliotheken geen crash veroorzaken bij invoer kleiner dan 64 megabyte op een gespecificeerde RISC-V/Linux-uitvoering, meldt Anthropic in een onderzoeksverslag van 22 oktober.

Onderhouders van open source C/C++-software kunnen bestaande fuzztests omzetten in controleerbare uitspraken over concrete codepaden. Wie een bibliotheek alleen in een product gebruikt, krijgt hierdoor geen algemene veiligheidsverklaring: het bewijs geldt per testdoel, voor een beperkte systeemopzet en voor de codeversie die na eventuele reparaties is getest.

Een fuzztest wordt een formele stelling

Een fuzzer stuurt automatisch gemaakte invoer naar een testfunctie en kijkt of de software crasht. Dat vindt fouten die een testteam niet vooraf heeft bedacht, maar de invoerruimte is vrijwel onbeperkt. Zelfs een campagne met miljarden pogingen kan niet aantonen dat elke mogelijke invoer is geprobeerd.

Anthropic zette bestaande Google OSS-Fuzz-tests om in een formele stelling: een testfunctie mag voor geen enkele invoer kleiner dan 64 megabyte crashen of een bestaande testassertie laten falen. Claude schreef het bewijs over de gecompileerde RISC-V-instructies, met de formele modellen van Theorem voor de processor en Linux-processen.

Claude schreef de bewijzen in Rocq, waarna de kernel controleerde of ze de formele stelling volgen. Anthropic rapporteert circa 180 miljoen bewijsregels voor 239 doelen, ongeveer 600.000 per bewijs. De bijbehorende binaries telden mediaan 18.000 RISC-V-instructies. Een mens hoeft niet elke regel na te lezen, maar moet de stelling en het systeemmodel wel begrijpen.

Zeldzame invoer bracht fouten boven

Claude mocht fouten die het tijdens het bewijzen vond ook aanpassen. Na een wijziging werd de test opnieuw gespecificeerd en moest Claude het bijgewerkte programma opnieuw bewijzen. De uitkomst geldt daardoor voor de gepatchte code. Ze zegt niet dat de versie die een gebruiker vandaag downloadt dezelfde garantie al heeft.

Anthropic meldt honderden gevonden fouten. Een ervan zat in een decompressiefunctie: een teller liep onder nul en veroorzaakte een schrijfactie buiten het bedoelde geheugengebied, maar alleen bij invoer van ongeveer 20 megabyte met een zeldzame opbouw. Een andere fout vroeg om 64 megabyte invoer en meer dan 2 gigabyte geheugen. Claude vond ook een bestaande fout opnieuw in libexpat die alleen bij diep geneste XML-invoer optrad.

Anthropic zegt dat sommige fouten jaren aan testcampagnes en biljoenen runs overleefden, maar noemt geen aantal per bibliotheek. Google meldde in mei 2017 dat OSS-Fuzz 10 biljoen testinvoeren per dag verwerkte. Dat was een programma-brede meting over 47 projecten, geen teller voor de versies uit deze proef. Formele verificatie stelt een andere vraag: crasht één testfunctie bij enige invoer kleiner dan 64 megabyte?

Het bewijs geldt per testdoel

De garantie heeft een smalle basis. Elk doel draait als statische RISC-V-binary, met één thread, musl en een vaste geheugenlimiet onder Linux. Veel bedrijven draaien dezelfde bibliotheken op x86- of ARM-servers met dynamisch gekoppelde glibc. Die uitvoeringen vallen buiten deze bewijzen.

Ook de eigenschap is begrensd. De proef bestrijkt geselecteerde fuzz-testdoelen, invoer kleiner dan 64 megabyte, AddressSanitizer-crashes en bestaande testbeweringen. AddressSanitizer mist sommige geheugenfouten; het bewijs dekt niet alle bibliotheekfuncties, aanroepers of logische fouten zonder crash. De Rocq-kernel controleert het bewijs, niet of het processor- en Linux-model volledig overeenkomt met productie.

De index van Theorem telt 60 bewezen ingangen in 25 bibliotheken in de versie van 22 oktober, tegenover 239 doelen in het onderzoeksverslag. Anthropic publiceert een deel en houdt bewijzen achter wanneer die een onopgeloste fout kunnen tonen. Andere lezers kunnen dus een deel narekenen, niet het hele experiment.

Theorem biedt gratis controle aan open sourceprojecten

Theorem biedt de formele controle kosteloos aan voor toegelaten open-sourceprojecten. Een kernonderhouder moet het project aanmelden en een statische RISC-V-build aanleveren. Dat maakt de route concreet voor onderhouders van veelgebruikte C- en C++-bibliotheken. Een softwarebedrijf dat een dependency afneemt, kan het bewijs alleen benutten als de bronversie en de build overeenkomen met wat het zelf inzet.

Anthropic heeft ook een andere beveiligingsroute geopend: de gratis OSS Scanner stuurt periodieke meldingen zonder menselijke controle naar projectonderhouders. Die scanner zoekt mogelijke kwetsbaarheden en stelt soms een reparatie voor. De open-sourcecode-scanner VulnHunter van Capital One gebruikt aanvalgerichte analyse en een falsificatie-engine. Formele verificatie voegt een controleerbare uitspraak toe over één testdoel en de omgeving waarin het draait.

De efficiëntiecijfers komen uit een aparte reeks van 36 kleine taken. Opus 5.5 bewees de helft met ongeveer 40 procent minder tokens dan Opus 5. Gedeelde bewijzen scheelden 17 procent tokens. Deze proef meet niet de kosten van de 239 bibliotheekdoelen. De grafiek toont de modelvergelijking.

Voor softwareteams verschuift de relevante vraag daarmee naar de exacte versie, compiler, architectuur en testingang waarop het bewijs rust. De volgende stap is of maintainers en leveranciers die gegevens samen met hun builds kunnen blijven publiceren. De 60 openbaar gemaakte doelen laten zien hoeveel van de proef nu al door anderen kan worden nagekeken; de overige claims vragen nog om de bijbehorende bewijzen en context.