{"id":183972,"date":"2026-10-23T11:41:12","date_gmt":"2026-10-23T09:41:12","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/anthropic-razvivaet-tehniku-dlya-formalnoj-verifikaczii-sushhestvuyushhego-po-pri-pomoshhi-ai"},"modified":"2026-10-23T11:41:16","modified_gmt":"2026-10-23T09:41:16","slug":"anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","status":"publish","type":"post","link":"https:\/\/prohoster.info\/sv\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic utvecklar tekniker f\u00f6r formell verifiering av befintlig programvara med hj\u00e4lp av AI","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
F\u00f6retaget Anthropic har presenterat resultaten av experiment med AI-modeller f\u00f6r formell verifiering av tillf\u00f6rlitlighet och s\u00e4kerhet hos redan existerande projekt. Under experimentet genererades matematiska bevis f\u00f6r avsaknad av minnesfel med hj\u00e4lp av AI-modeller f\u00f6r 123 \u00f6ppna bibliotek som testades i OSS Fuzz-infrastrukturen. <\/p>\n
Verifikationen utf\u00f6rdes p\u00e5 niv\u00e5n av den kompilerade assemblerkoden f\u00f6r RISC-V-arkitekturen. Den totala volymen av genererade bevis uppgick till cirka 180 miljoner kodrader f\u00f6r verifieringssystemet Rocq Prover (cirka 600 000 rader f\u00f6r en bin\u00e4rfil med 18 000 RISC-V-instruktioner). Bevisen bildades genom automatisk omvandling av befintliga fuzzing-tester till formella specifikationer, varefter AI-modellen Claude bevisade att programmet inte kraschar med alla ing\u00e5ngar upp till 64 MB. <\/p>\n
Under processen f\u00f6r att bygga upp bevis kunde AI-modellen identifiera och f\u00f6rbereda korrigeringar f\u00f6r hundratals fel som tidigare inte uppt\u00e4ckts vid fuzzing-testning. Bland annat identifierades s\u00e5rbarheter som ledde till buffert\u00f6verfl\u00f6d vid bearbetning av vissa indata (t.ex. CVE-2026-56132 i libexpat), samt logiska fel. Dessutom anv\u00e4ndes AI-modellen f\u00f6r att bevisa att implementeringen av zlib-algoritmen i Linux-k\u00e4rnan \u00f6verensst\u00e4mmer med specifikationen RFC 1950.<\/p>\n
Dessutom har en tolk f\u00f6r en delm\u00e4ngd av Python-spr\u00e5ket genererats i Rust, f\u00f6r vilken ett formellt bevis har f\u00f6rberetts med hj\u00e4lp av verktyget Verus f\u00f6r att \u00f6verensst\u00e4mma med CPython-semantiken. F\u00f6r att j\u00e4mf\u00f6ra beteendet med CPython k\u00f6rdes mer \u00e4n 1,7 miljoner slumpm\u00e4ssigt genererade Python-program. I 99,95% av fallen st\u00e4mde resultaten fr\u00e5n dessa program i den nya implementeringen och i CPython \u00f6verens, och de identifierade avvikelserna visade sig vara k\u00e4nda gr\u00e4nsfall.<\/p>\n
Genomf\u00f6rd formell verifiering garanterar \u00f6verensst\u00e4mmelse med specifikationen, men utesluter inte helt uppkomsten av s\u00e4kerhetsproblem, eftersom risker orsakade av flertr\u00e5dighet, dynamisk l\u00e4nkning och avvikande beteende hos den verkliga h\u00e5rdvaran f\u00f6rblir oformulerade. En betydande f\u00f6rdel med den f\u00f6reslagna metoden \u00e4r att den arbetar direkt med bin\u00e4rfiler, vilket g\u00f6r det m\u00f6jligt att undvika behovet av att skriva om befintlig kod i formellt verifierbara spr\u00e5k. \n K\u00e4lla: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"