{"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\/da\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic udvikler teknikker til formel verifikation af eksisterende software ved hj\u00e6lp af AI","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Selskabet Anthropic har pr\u00e6senteret resultaterne af eksperimenter vedr\u00f8rende brugen af AI-modeller til formel verifikation af p\u00e5lidelighed og sikkerhed i allerede eksisterende projekter. I l\u00f8bet af eksperimentet blev der med hj\u00e6lp fra AI-modeller genereret matematiske beviser for frav\u00e6r af fejl i hukommelsesh\u00e5ndteringen for 123 \u00e5bne biblioteker, der blev testet i OSS Fuzz-infrastrukturen. <\/p>\n
Verifikationen blev gennemf\u00f8rt p\u00e5 niveauet for den komplierede assemblerkode for RISC-V-arkitekturen. Den samlede m\u00e6ngde af genererede beviser udgjorde cirka 180 millioner linjer kode for verifikationssystemet Rocq Prover (cirka 600.000 linjer for en bin\u00e6r fil med 18.000 RISC-V-instruktioner). Beviserne blev dannet ved automatisk at konvertere eksisterende fuzzing-tests til formelle specifikationer, hvorefter AI-modellen Claude beviste, at der under alle inddata op til 64 MB ikke opst\u00e5r fejl i programmet. <\/p>\n
I l\u00f8bet af opbygningen af beviserne kunne AI-modellen identificere og forberede rettelser til hundredevis af fejl, som tidligere ikke blev bem\u00e6rket under fuzzing-testning. Blandt andet blev der identificeret s\u00e5rbarheder, der f\u00f8rer til buffer-overl\u00f8b ved behandling af visse inddata (f.eks. CVE-2026-56132 i libexpat), samt logiske fejl. Desuden blev AI-modellen brugt til at bevise, at implementeringen af zlib-algoritmen i Linux-kernen overholder specifikationen i RFC 1950.<\/p>\n
Derudover blev der genereret en fortolker p\u00e5 Rust til en undergruppe af Python-sproget, for hvilken der ved hj\u00e6lp af v\u00e6rkt\u00f8jet Verus blev forberedt et formelt bevis for overensstemmelse med semantikken af CPython. For at sammenligne adf\u00e6rden med CPython blev der udf\u00f8rt mere end 1,7 millioner tilf\u00e6ldigt genererede Python-programmer. I 99,95% af tilf\u00e6ldene stemte resultaterne af eksekveringen af disse programmer i den nye implementering overens med CPython, og de identificerede forskelle viste sig at v\u00e6re kendte gr\u00e6nsetilf\u00e6lde.<\/p>\n
Den udf\u00f8rte formelle verifikation garanterer overensstemmelse med specifikationen, men udelukker ikke fuldst\u00e6ndigt opst\u00e5ende sikkerhedsproblemer, da der stadig er uformelle risici for\u00e5rsaget af problemer med multitr\u00e5dning, dynamisk binding og unormel adf\u00e6rd fra det faktiske udstyr. En n\u00f8glefordel ved den foresl\u00e5ede tilgang er arbejdet direkte med bin\u00e6re filer, hvilket g\u00f8r det muligt at undg\u00e5 behovet for at omskrive den eksisterende kode til formelt verificerbare sprog. \n Kilde: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"