Anthropic: Claude har bevisat säkerheten i 123 bibliotek

Anthropic uppger att deras modell Claude har skrivit maskinkontrollerade matematiska bevis som visar att kompilerad kod från 123 bibliotek med öppen källkod inte kan krascha under definierade förhållanden. Modellen hittade även buggar längs vägen som förblivit oupptäckta i åratal trots biljoner testkörningar, enligt forskning som publicerades den 22 oktober av företagets Frontier Red Team, som arbetat med projektet tillsammans med firman Theorem.anthropic.com

Företaget kallar detta vad de tror är "den första storskaliga insatsen att använda AI för att tillämpa formell verifiering på programvara i produktion på assemblernivå." De argumenterar för att AI nu enkelt kan hitta och utnyttja buggar, så testning ensamt räcker inte längre för att skydda programvara, skriver Anthropic.anthropic.com

Från fuzz-tester till bevis

Teamet började med fuzz-tester från Googles OSS-Fuzz-program och gjorde om varje test till en formell specifikation. Regeln var att testet aldrig får krascha på någon input mindre än 64 MB när den kompileras till RISC-V-maskinkod. Under några veckor bevisade Claude detta för 239 ingångspunkter i 123 bibliotek. Bevisen uppgår till cirka 180 miljoner rader kod i Rocq-bevis-språket, och ett typiskt bevis omfattar ungefär 600 000 rader, enligt Anthropic. Rocq-beviskontrollern bekräftar att varje bevis matchar sin specifikation, så utvecklare behöver inte granska den genererade koden rad för rad, rapporterade Interesting Engineering.interestingengineering.com+1

Anthropic uppgav att en delmängd av bevisen publiceras, tillsammans med den RISC-V- och Linux-semantik som ligger bakom dem. Theorem erbjuder sig att köra samma pipeline gratis för kvalificerade projekt med öppen källkod genom sitt OSS Verify-program, rapporterade Unite.AI. Theorem har även släppt en Claude-färdighet för att hjälpa utvecklare att registrera sig.unite.ai+1

Buggar som fuzzers missade

Att skriva bevisen ledde till att hundratals buggar hittades, vilka Claude patchade innan den bevisade den lagade koden. I en dekompressor hittade den en underflödesbugg som ledde till en skrivning utanför minnesgränsen, men endast vid input på cirka 20 MB med en sällsynt layout. En annan läsning utanför minnesgränsen, i en bildavkodare, krävde en 64 MB input och mer än 2 GB minne. Claude återupptäckte även en känd sårbarhet i libexpat och hittade en logisk brist där en funktion som var tänkt att begränsa vilka filer en applikation kan ladda inte alltid efterlevdes, enligt forskningen.anthropic.com

Begränsningar i garantin

Anthropic varnade för att bevisen inte innebär att biblioteken är buggfria. De förutsätter en enkeltrådad statisk binärfil med en fast minnesbudget som körs på en RISC-V-processor under Linux. Eventuella kvarvarande buggar ligger antingen utanför bevisens omfattning eller i de betrodda komponenterna, det vill säga hårdvaru- och operativsystemmodellerna, teorem-satserna och själva Rocq-kontrollern, skriver företaget. De flesta distribuerade system använder andra processorarkitekturer eller konfigurationer, noterade Interesting Engineering.interestingengineering.com+1

Anthropic anser ändå att ekonomin håller på att förändras. "Vi uppmuntrar alla utvecklare att utforska formell verifiering med LLMer, särskilt de som tidigare försökt med mindre kapabla modeller och upptäckt att det inte fungerade," skriver teamet.anthropic.com