Anthropic: Claude prokázal bezpečnost 123 knihoven

Společnost Anthropic uvádí, že její model Claude vytvořil strojově ověřené matematické důkazy, které ukazují, že zkompilovaný kód ze 123 knihoven s otevřeným zdrojovým kódem nemůže za definovaných podmínek selhat. Model během procesu také našel chyby, které zůstávaly roky neodhaleny i přes biliony testovacích spuštění, uvádí výzkum zveřejněný 22. října týmem Frontier Red Team, který na projektu spolupracoval s firmou Theorem, jež se specializuje na formální metody.anthropic.com

Společnost to označuje za „první rozsáhlé úsilí o využití AI k aplikaci formální verifikace na produkční software na úrovni assembleru“. Anthropic uvádí, že AI nyní dokáže snadno najít a zneužít chyby, takže samotné testování již k zabezpečení softwaru nestačí.anthropic.com

Od fuzz testů k důkazům

Tým začal s fuzz testy z programu OSS-Fuzz od Google a každý z nich převedl na formální specifikaci. Pravidlem bylo, že test nikdy nesmí selhat při žádném vstupu menším než 64 MB při kompilaci do strojového kódu RISC-V. Během několika týdnů Claude toto prokázal pro 239 vstupních bodů napříč 123 knihovnami. Důkazy čítají přibližně 180 milionů řádků kódu v dokazovacím jazyce Rocq a typický důkaz má zhruba 600 000 řádků, uvádí Anthropic. Kontrolor důkazů Rocq potvrzuje, že každý důkaz odpovídá své specifikaci, takže vývojáři nemusí generovaný kód kontrolovat řádek po řádku, informoval server Interesting Engineering.interestingengineering.com+1

Anthropic uvedl, že část důkazů je zveřejňována spolu se sémantikou RISC-V a Linuxu, na které jsou založeny. Theorem nabízí, že stejný proces provede zdarma pro kvalifikované projekty s otevřeným zdrojovým kódem prostřednictvím svého programu OSS Verify, informoval server Unite.AI. Theorem také vydal dovednost pro Claude, která správcům pomáhá se registrovat.unite.ai+1

Chyby, které fuzzery přehlédly

Psaní důkazů odhalilo stovky chyb, které Claude opravil ještě předtím, než opravený kód dokázal. V dekompresoru našel podtečení čítače, které vedlo k zápisu mimo meze, ale pouze u vstupů o velikosti kolem 20 MB s jedním vzácným rozložením. Další čtení mimo meze v dekodéru obrázků vyžadovalo 64 MB vstup a více než 2 GB paměti. Claude také znovu objevil známou zranitelnost v libexpat a našel logickou chybu, kdy funkce určená k omezení toho, které soubory může aplikace načíst, nebyla vždy vynucována, uvádí výzkum.anthropic.com

Limity záruky

Anthropic varoval, že důkazy neznamenají, že knihovny jsou bezchybné. Předpokládají jednovláknový statický binární soubor s pevným paměťovým limitem běžící na procesoru RISC-V pod Linuxem. Veškeré zbývající chyby jsou buď mimo rozsah důkazů, nebo se nacházejí v důvěryhodných komponentách, což znamená modely hardwaru a operačního systému, samotné věty a samotný kontrolor Rocq, napsala společnost. Většina nasazených systémů používá jiné architektury procesorů nebo konfigurace, poznamenal Interesting Engineering.interestingengineering.com+1

Anthropic se přesto domnívá, že se ekonomika mění. „Vyzýváme všechny vývojáře, aby prozkoumali formální verifikaci pomocí LLM, zejména ty, kteří to dříve zkoušeli s méně schopnými modely a zjistili, že to nefunguje,“ napsal tým.anthropic.com