Claude formális bizonyításokat írt 123 nyílt forrású könyvtárhoz

Az Anthropic szerint a szoftverek többsége hibás, amelyeket az AI-modellek ma már könnyen megtalálnak és kihasználnak. A formális szoftververifikáció elvileg garantálhatja a hibamentességet, eddig azonban évekig tartó szakértői munkát igényelt. A Theoremmel közös kísérletben a Claude RISC-V assembly szintű biztonsági tulajdonságokat bizonyított több mint 100 valós, nyílt forráskódú szoftverkönyvtárban. A cég szerint ez az első nagy léptékű próbálkozás, amelyben AI-val alkalmaztak formális verifikációt éles szoftvereken assembly szinten.

A bizonyítás szerint a vizsgált programok 64 MB-nál kisebb bemenetek esetén, egyszálú, statikus binárisként, rögzített memóriakeret mellett, Linux operációs rendszeren futva mindig normálisan leállnak, memóriabiztonsági hiba vagy sikertelen állítás nélkül. A munka közben a Claude olyan hibákat is talált, amelyeket évekig nem észleltek, pedig a szoftverek több billió tesztfutáson estek át. A Linux kernelben nemrég több mint 1000 sebezhetőséget hoztak nyilvánosságra.

Az Anthropic példaként említi, hogy a seL4 operációs rendszermag megvalósítása két személyévet, a formális verifikálása viszont húsz személyévet vett igénybe. A cég a bizonyítások egy részét közzéteszi, a RISC-V- és operációsrendszer-szemantikával együtt. A Theorem vállalja, hogy más nyílt forráskódú projektekre is lefuttatja az eljárást, és Claude-skillt tesz közzé a fejlesztők számára. A kísérletek között szerepel a zlib tömörítő algoritmus biztonságának vizsgálata és egy Rustban írt Python-interpreter viselkedési egyenértékűségének bizonyítása.