Компанія Аnthropic представила результати експериментів щодо використання AI-моделей для формальної верифікації надійності та безпеки вже існуючих проектів. В ході експерименту за допомогою 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
