Claude виявив сотні помилок у ПЗ, які роками не бачили тести
Штучний інтелект продемонстрував, що може не лише знаходити помилки в програмному коді, а й допомагати формально доводити його безпечність. У спільному проєкті Anthropic і компанії Theorem модель Claude проаналізувала скомпільований машинний код та створила математичні докази для сотень точок входу в програмні бібліотеки.
Такий підхід здатен доповнити традиційне тестування й зробити формальну верифікацію доступнішою для проєктів, які раніше не могли дозволити собі настільки глибокий аналіз.
Чому звичайного тестування недостатньо
Автоматизовані тести та фаззинг перевіряють програму на великій кількості вхідних даних, навмисно створюючи нестандартні або пошкоджені сценарії. Однак навіть мільйони тестів не охоплюють усі можливі комбінації значень і послідовностей операцій.
Формальна верифікація працює інакше: вона описує властивість програми мовою математичних специфікацій, а потім доводить, що код відповідає цим вимогам за визначених умов. Це не гарантує відсутності будь-яких помилок, але дає значно сильніші підтвердження для конкретних сценаріїв.
Як Claude створював докази безпеки
Для експерименту Anthropic передала Claude наявні результати фаззинг-тестів. Модель перетворила їх на формальні специфікації та згенерувала докази для 239 точок входу у 123 бібліотеках.
Аналізували асемблерний код для архітектури RISC-V — набору інструкцій, які безпосередньо виконує процесор. Загальний обсяг згенерованого коду доказів сягнув приблизно 180 мільйонів рядків, а типовий доказ займав близько 600 тисяч рядків.
- Claude формалізував властивості, які раніше перевірялися переважно тестами.
- Окремий інструмент Rocq незалежно перевірив коректність отриманих доказів.
- Після виявлення помилок модель могла виправити їх і створити новий доказ для оновленої версії коду.
Перевірка за допомогою Rocq важлива тому, що сама мовна модель не є остаточним арбітром правильності. Claude генерує рішення, а спеціалізований незалежний засіб перевіряє, чи справді воно відповідає заявленій специфікації.
Які дефекти вдалося знайти
Формальний аналіз виявив низку проблем, які тривалий час залишалися непоміченими під час звичайного тестування. Серед них були як помилки роботи з пам’яттю, так і логічні вразливості:
- Помилка лічильника. Недоповнення могло призвести до запису за межами дозволеного діапазону під час декомпресії даних.
- Дефект декодера зображень. Для його виявлення потрібно було подати майже 64 МБ вхідних даних і використати понад 2 ГБ оперативної пам’яті.
- Читання за межами буфера. Результат залежав від послідовності операцій із файловими дескрипторами.
- Проблема в XML-парсері libexpat. Вразливість стосувалася популярної бібліотеки для обробки XML.
- Логічна помилка в обмеженні завантажень. Вона могла дозволити обійти встановлену функцію контролю файлів.
Ці приклади показують перевагу формальних методів: вони здатні перевіряти не лише типові сценарії, а й рідкісні поєднання умов, які майже неможливо відтворити вручну або за допомогою випадкової генерації даних.
Які обмеження має підхід
Anthropic наголошує, що формально перевірена програма не стає автоматично повністю безпомилковою. Доказ підтверджує лише конкретну властивість за умов, які були явно описані у відповідній специфікації.
Якщо вимогу сформульовано неповно, важливий сценарій не враховано або помилка міститься в іншій частині системи, математичний доказ не зможе її виявити. Тому формальна верифікація має доповнювати, а не повністю замінювати тестування, аудит і аналіз архітектури.
Нинішній експеримент також має обмежений масштаб. Він охоплював однопотокові та статично зв’язані програми для RISC-V, що працювали у змодельованому середовищі Linux. Реальні програмні системи зазвичай складніші: вони взаємодіють із мережами, операційними системами, драйверами та паралельними процесами.
Що це означає для розробки ПЗ
Найбільший потенціал такого підходу — у повторному використанні доказів. Якщо бібліотеку оновлюють, не обов’язково починати перевірку з нуля: частину вже створених формальних описів можна адаптувати до нової версії.
У майбутньому вдосконалення моделей і спеціалізованих інструментів може зменшити витрати на перевірку критичних компонентів. Це особливо важливо для програм, від яких залежать фінансові системи, інфраструктура, промислове обладнання та засоби кібербезпеки.
Отже, Claude у цьому експерименті виступив не заміною інженерам з безпеки, а прискорювачем складної роботи. Поєднання генерації доказів штучним інтелектом і незалежної машинної перевірки може зробити формальні методи практичнішими та допомогти знаходити вразливості, які роками вислизають від традиційного тестування.
