Anthropic het die resultate van eksperimente aangebied met behulp van KI-modelle om die betroubaarheid en sekuriteit van bestaande projekte formeel te verifieer. Tydens die eksperiment is KI-modelle gebruik om wiskundige bewyse te genereer van die afwesigheid van geheuefoute vir 123 oopbronbiblioteke wat in die OSS Fuzz-infrastruktuur getoets is.
Die verifikasie is uitgevoer op die vlak van saamgestelde samestellingskode vir die RISC-V-argitektuur. Die totale volume gegenereerde bewyse het ongeveer 180 miljoen reëls kode vir die Rocq Prover-verifikasiestelsel beloop (ongeveer 600 000 reëls per binêre lêer met 18 000 RISC-V-instruksies). Die bewyse is gegenereer deur bestaande fuzzing-toetse outomaties om te skakel na formele spesifikasies, waarna die Claude KI-model bewys het dat die program foutloos is vir enige invoerdata tot 64 MB.
Tydens die bewysbouproses kon die KI-model honderde foute identifiseer en regstellings voorberei wat voorheen onopgespoor is deur fuzz-toetsing. Dit het onder andere bufferoorloop-kwesbaarhede ingesluit tydens die verwerking van sekere invoerdata (bv. CVE-2026-56132 in libexpat), sowel as logiese foute. Verder is die KI-model gebruik om ooreenstemming van die kern se implementering van die zlib-algoritme te bewys. Linux RFC 1950 spesifikasies.
'n Interpreteerder vir 'n subversameling van Python is ook in Rust gegenereer, waarvoor 'n formele bewys van ooreenstemming met CPython-semantiek voorberei is met behulp van die Verus-gereedskapskis. Om gedrag met CPython te vergelyk, is meer as 1.7 miljoen ewekansig gegenereerde Python-programme uitgevoer. In 99.95% van gevalle het die resultate van die uitvoering van hierdie programme in die nuwe implementering en in CPython ooreengestem, en enige teenstrydighede wat gevind is, was bekende randgevalle.
Formele verifikasie waarborg spesifikasie-nakoming, maar dit skakel nie sekuriteitskwessies heeltemal uit nie, aangesien risiko's wat veroorsaak word deur multithreading-probleme, dinamiese skakeling en anomale gedrag op werklike hardeware ongeformaliseerd bly. 'n Belangrike voordeel van die voorgestelde benadering is dat dit direk met binêre lêers werk, wat die behoefte om bestaande kode in formeel verifieerbare tale te herskryf, uitskakel.
Bron: opennet.ru
