Anthropic tvrdí, že Claude prokázal bezpečnostní vlastnosti 123 knihoven

Anthropic zveřejnil výzkum 22. října 2026. Uvedl v něm, že Claude ve spolupráci se společností Theorem vytvořil strojově ověřené formální důkazy bezpečnostních vlastností na úrovni assemblerového kódu RISC-V pro 239 vstupních bodů fuzzovacích testů ve 123 knihovnách s otevřeným zdrojovým kódem.

Podle Anthropic Claude opravil nalezené chyby a následně dokázal, že programy pro každý vstup menší než 64 MB a každou modelovanou reakci operačního systému Linux i každé rozložení paměti vždy řádně skončí, aniž dojde k chybám bezpečnosti paměti nebo selhání asercí. Důkazy předpokládají, že program běží jako jednovláknový statický binární soubor s pevně stanoveným limitem paměti na procesoru RISC-V se systémem Linux. Anthropic uvedl, že důkazy mají přibližně 180 milionů řádků jazyka Rocq a typický důkaz čítá asi 600 000 řádků a pokrývá binární soubory s mediánovou délkou 18 000 instrukcí RISC-V. Společnost uvedla, že pokud je jí známo, jde o první rozsáhlý pokus využít AI k uplatnění formální verifikace na produkční software na úrovni assemblerového kódu.

Část důkazů spolu se sémantikou instrukční sady RISC-V a operačního systému, o niž se opírají, se zveřejňuje na GitHubu. Anthropic uvedl, že zveřejňuje také důvěryhodné komponenty vytvořené pro tento projekt, které dosud nebyly veřejně dostupné, úplné důkazy pro fuzzovací testy, jež nevyžadovaly opravu, a specifikace fuzzovacích testů, které se nepodařilo prokázat. Důkazy, které by mohly odhalit neopravenou chybu, však nezveřejňuje.

Převod fuzzovacích testů na formální důkazy

Tento přístup převádí existující kompilovatelný fuzzovací test každé knihovny na formální specifikaci vyjadřující jedno pravidlo: test při žádném vstupu menším než 64 MB nesmí havarovat. Specifikace je definována nad zkompilovanými instrukcemi RISC-V pomocí formální sémantiky instrukční sady RISC-V a procesů Linuxu od společnosti Theorem a ověřovač důkazů Rocq kontroluje každý dokončený důkaz podle specifikace. Anthropic uvádí, že vývojáři tak musí důvěřovat pouze třem komponentám: formálním modelům RISC-V a procesů Linuxu, přesnému znění teorémů a samotnému ověřovači Rocq.

Anthropic uvedl, že tento postup použil na stovky projektů v rámci iniciativy OSS-Fuzz společnosti Google, která zajišťuje průběžné fuzzovací testování způsobilých projektů s otevřeným zdrojovým kódem a automaticky instrumentuje programy v jazycích C a C++ pomocí nástroje AddressSanitizer. Ten program ukončí, kdykoli dojde k nesprávnému přístupu do paměti. Dodatek datovaný 22. října 2026 uvádí úplné znění prokázaného teorému: pro všechny vstupy menší než 64 MiB a všechna rozložení paměti nedojde u binárního souboru instrumentovaného nástrojem ASan ani u běžného binárního souboru k chybě, přerušení běhu ani k nemodelovanému chování; oba soubory navíc vytvářejí totožné stopy čtení a zápisu, chovají se při ukončení stejně a zanechávají stejný konečný stav souborového systému.

Dodatek uvádí, že Claude během projektu napsal přibližně jednu miliardu řádků jazyka Rocq, z nichž asi 180 milionů prošlo ověřovačem důkazů. Vstupní bod 391řádkového parseru cJSON získal důkaz o 630 000 řádcích, zatímco knihovna fftw3 s 51 000 přilinkovanými řádky získala důkaz o 480 000 řádcích. Protože Claude mohl před dokončením důkazu upravovat kód, Anthropic tyto úpravy penalizoval, nabízel bonus za prokázání toho, které vstupy úprava změnila, a úpravy zaznamenával a kontroloval, aby omezil účelové obcházení hodnoticího mechanismu.

Chyby odhalené při pokusech o dokazování

Anthropic uvádí, že pokusy o důkazy odhalily stovky chyb, z nichž mnohé by fuzzovací nástroj pravděpodobně nenašel. Při dokazování vstupního bodu jedné knihovny Claude objevil podtečení čítače v dekompresoru, které způsobovalo zápis mimo vyhrazenou oblast paměti, ale pouze u vstupů o velikosti přibližně 20 MB s jedním vzácným, specifickým rozložením. Mezi další nálezy patřilo čtení mimo vyhrazenou oblast paměti v dekodéru obrázků, které vyžadovalo vstup o velikosti 64 MB a více než 2 GB paměti; další takové čtení vyžadovalo konkrétní posloupnost volání přes dvě obslužné položky odkazující na tentýž soubor. Claude také znovu objevil chybu CVE-2026-56132 v knihovně libexpat, která vyžadovala hluboce vnořený vstup.

Claude našel také logické chyby, které nikdy nezpůsobí havárii, včetně omezení toho, které soubory může aplikace načítat a které se neuplatňuje vždy. Anthropic uvedl, že pokusy o verifikaci několika široce používaných kritických aplikací odhalily dosud neznámou logickou chybu, která zůstávala skrytá déle než deset let. Při snaze ověřit široce používanou čtečku PDF pak během jediného týdne našel tolik bezpečnostních chyb, kolik se jich obvykle nahlásí za rok.

Další experimenty a zjištění o efektivitě

Kromě OSS-Fuzz požádal Anthropic Clauda, aby vytvořil formální specifikaci RFC 1950, technického dokumentu definujícího kompresní formát zlib, a následně dokázal, že implementace zlib v jádře Linuxu tuto specifikaci správně realizuje. Claude přímo prokázal správnost binárního souboru zkompilovaného pro x86 pomocí formální sémantiky instrukční sady x86, kterou sám vytvořil. Anthropic uvedl, že stejný postup zopakoval u šesti dalších široce používaných knihoven a našel drobné, nezneužitelné chyby v okrajových případech, které se nyní hlásí upstreamu. Společnost také uvedla, že při vytváření sémantiky x86 byly odhaleny stovky chyb v oficiální referenční dokumentaci a menší počet chyb v samotném hardwaru a že jednokrokové provádění podle této sémantiky dokáže spustit uživatelské prostředí Ubuntu na jádře Linuxu.

V dalším experimentu Claude vytvořil v Rustu interpret rozsáhlé podmnožiny jazyka Python a pomocí ověřovacího nástroje Verus dokázal, že odpovídá sémantice CPythonu popsané v odborné práci. Technická příloha uvádí, že bylo dokázáno všech 17 vrstev interpretu a že platí věta: „Kdykoli interpret vrátí výsledek, jde o výsledek předepsaný formální sémantikou.“ Anthropic uvedla, že empirické testování 1,7 milionu náhodně vygenerovaných programů v Pythonu prokázalo v 99,95 % případů totožné chování s CPythonem; z deseti záměrně vložených chyb jich pět náhodné testování neodhalilo, zatímco všech sedm zneplatnilo důkaz.

Aby Anthropic změřila efektivitu, vytvořila 36 malých ověřovacích úloh zmenšením skutečných vstupních bodů OSS-Fuzz. Vznikly tak programy o 283–2 491 instrukcích, se vstupy omezenými na 64 bajtů a s běhovým prostředím „mini-ASan“ o přibližně 100 instrukcích, které nahradilo AddressSanitizer. Anthropic uvádí, že Opus 5.5 prokáže polovinu úloh s přibližně o 40 % menším počtem tokenů než Opus 5. Anthropic také uvádí, že agenti, kteří mohli ve sdíleném pracovním prostoru kopírovat důkazy ostatních, potřebovali o 17 % méně tokenů než agenti pracující samostatně; některým se podařilo uspět poté, co při samostatné práci předtím neuspěli, a agenti pracující samostatně nedokázali dokončit dva z důkazů. Společnost uvedla, že stejný efekt opakovaného využití se ve větším měřítku projevil i při práci na OSS-Fuzz: týmy agentů kopírovaly hotové důkazy a upravovaly je, protože značná část každého důkazu se týká společného inicializačního kódu běhového prostředí C a AddressSanitizeru.

Uvedená omezení a program OSS Verify

Anthropic uvádí, že důkazy neznamenají, že knihovny neobsahují chyby: zbývající chyby se mohou nacházet v důvěryhodných komponentách nebo mimo rozsah důkazů. Důkazy se týkají jednovláknových statických binárních souborů RISC-V propojených s musl libc, zatímco většina uživatelů tyto knihovny používá na platformách x86 nebo ARM a dynamicky je propojuje s glibc; AddressSanitizer navíc neodhalí všechny chyby zabezpečení paměti. Společnost uvedla, že očekává, že s vývojem modelů bude možné tato omezení překonat.

Theorem nabízí prostřednictvím programu OSS Verify stejný postup zdarma projektům s otevřeným zdrojovým kódem, které splňují podmínky. Zapojení probíhá prostřednictvím žádosti o začlenění změn, která do repozitáře programu přidá soubory project.yaml, Dockerfile a build.sh. Theorem uvádí, že projekty posuzuje obdobně jako OSS-Fuzz a upřednostňuje široce používanou kritickou infrastrukturu. Podle Theorem správci obdrží důkaz v systému Rocq, ověřený jádrem Rocq, že žádný cíl fuzz testování nespadne při žádném vstupu o velikosti až 64 MiB; chyby nalezené při vytváření důkazu jsou správcům sdělovány soukromě e-mailem, bez stanovené lhůty pro jejich zveřejnění, a vytvoření důkazu může trvat několik dní. Plán Theorem počítá s ověřením celého ekosystému Nix včetně kritické infrastruktury, jako jsou glibc, OpenSSL a cURL.