Компания Anthropic представи резултатите от експерименти с използването на AI модели за формална верификация на надеждността и безопасността на съществуващи проекти. По време на експеримента бяха генерирани матемтически доказателства за отсъствие на грешки при работа с паметта за 123 отворени библиотеки, тествани в инфраструктурата OSS Fuzz.
Проверката беше извършена на ниво компилиран асемблерен код за архитектурата RISC-V. Общият обем на генерираните доказателства беше около 180 милиона реда код за системата за верификация Rocq Prover (около 600 хиляди реда на бинарен файл с 18 хиляди инструкции RISC-V). Доказателствата бяха формулирани чрез автоматично преобразуване на съществуващи fuzzing тестове в формални спецификации, след което AI моделът Claude доказваше, че при всякакви входни данни с обем до 64 МБ в програмата не възникват сривове.
В процеса на построяване на доказателствата AI моделът успя да открие и подготви корекции за стотици грешки, които преди това не бяха забелязани при fuzzing тестването. Между другото, бяха открити уязвимости, водещи до препълване на буфера при обработка на определени входни данни (например, CVE-2026-56132 в libexpat), както и логически грешки. Освен това, AI моделът бе използван за доказване на съответствието на реализирането на алгоритъма zlib в ядрото на Linux със спецификацията RFC 1950.
Също така на езика Rust беше генериран интерпретатор за подмножество на езика Python, за който чрез инструмента Verus бе подготвено формално доказателство за съответствие на семантиката на CPython. За сравнение на поведението с CPython бяха изпълнени над 1.7 милиона случайно генерирани Python програми. В 99.95% от случаите резултатите от изпълнението на тези програми в новата реализация и в CPython съвпаднаха, а откритите несъответствия се оказаха известни гранични случаи.
Извършената формална верификация гарантира съответствие със спецификациите, но напълно не изключва възникването на проблеми със сигурността, тъй като остава неформализиран риск, породен от проблеми с многопоточността, динамично свързване и аномално поведение на реалното оборудване. Ключовото предимство на предложеното решение е работата директно с бинарни файлове, което позволява да се избегне необходимостта от пренаписване на съществуващия код на формално верифицируеми езици.
Източник: opennet.ru
