Az Anthropic cég bemutatta az AI-modellek használatának kísérleteinek eredményeit, amelyek célja a meglévő projektek megbízhatóságának és biztonságának formális verifikációja. A kísérlet során AI-modellek segítségével 123 nyílt forráskódú könyvtárra generáltak matematikai bizonyítékokat a memóriahasználat hibáinak hiányáról az OSS Fuzz infrastruktúrájában.
A tesztelés a RISC-V architektúra bináris assembler kód szintjén történt. A generált bizonyítékok összterjedelme körülbelül 180 millió kódsor volt a Rocq Prover verifikációs rendszer számára (körülbelül 600 ezer sor egy 18 ezer RISC-V utasítást tartalmazó bináris fájlhoz). A bizonyítékokat a meglévő fuzzing tesztek automatikus átalakításával formális specifikációkká hozták létre, majd a Claude AI-modell bizonyította, hogy bármilyen 64 MB-ig terjedő bemenet esetén a program nem omlik össze.
A bizonyítékok felépítése során az AI-modell képes volt azonosítani és javításokat előkészíteni számos hiba számára, amelyeket korábban nem észleltek a fuzzing tesztelés során. Többek között, felfedeztek sebezhetőségeket, amelyek a puffer túlcsordulásához vezethetnek bizonyos bemeneti adatok feldolgozása során (például CVE-2026-56132 a libexpat-ben), valamint logikai hibákat. Emellett az AI-modellt a Linux kernel zlib algoritmusának RFC 1950 specifikációhoz való megfelelőségének bizonyítására is használták.
Rust nyelven egy interpretátort generáltak a Python nyelv egy részhalmazához, amelyhez a Verus eszközkészletével formális bizonyítékot készítettek a CPython szemináriumának való megfelelésről. A CPython-nal való viselkedés összehasonlítása érdekében több mint 1,7 millió véletlenszerűen generált Python program futott. Az esetek 99,95%-ában ezeknek a programoknak az új végrehajtási eredményei és a CPython egyeztek, a felfedezett eltérések pedig ismert határhesseket mutattak.
A formális verifikáció garantálja a specifikációknak való megfelelést, de nem zárja ki teljesen a biztonsági problémák megjelenését, mivel a párhuzamos programozás, a dinamikus linking és a valós hardver anomáliáinak eredményeként felmerülő kockázatok nincsenek formailag érvényesítve. Az ajánlott megközelítés kulcsfontosságú előnye, hogy közvetlenül a bináris fájlokkal dolgozik, így elkerülhető a meglévő kód átírása formálisan verifikálható nyelveken.
Forrás: opennet.ru
