Штучний інтелект знайшов сотні помилок у програмах, що витримали трильйони перевірок

Штучний інтелект Claude від компанії Anthrop­ic знайшов сотні програмних дефектів у коді, який роками витримував трильйони автоматизованих перевірок. Спільно зі спеціалістами компанії The­o­rem дослідники перевірили 123 бібліотеки з відкритим вихідним кодом і виявили помилки, що ховалися в коді попри масштабне тестування.

Ключовою особливістю експерименту стало застосування формальної верифікації — підходу, який дозволяє математично довести, що програма виконує задані вимоги. На відміну від звичайного тестування, де перевіряються окремі сценарії, цей метод охоплює всі можливі вхідні дані в межах заданих обмежень.

За основу взяли бібліотеки з проєкту Google OSS-Fuzz, призначеного для автоматичного пошуку вразливостей. Його інструменти безперервно подають програмам випадкові та спеціально змінені дані, намагаючись спровокувати збої, переповнення пам’яті чи інші помилки. Але навіть мільярди таких перевірок не гарантують виявлення рідкісних дефектів, що виникають лише при незвичних комбінаціях вхідних даних.

Claude перетворював існуючі тести на математичні умови й будував доказ їхнього виконання. Перевірка відбувалася на рівні машинних інструкцій архітектури RISC‑V — тобто вже скомпільованих програм. За кілька тижнів система підготувала докази для 239 точок входу в 123 бібліотеках, а загальний обсяг сягнув близько 180 мільйонів рядків коду мовою Rocq.

Серед знахідок — помилка в алгоритмі розпакування даних, здатна призвести до запису інформації за межі виділеної пам’яті: для її прояву потрібен файл обсягом близько 20 мегабайт із рідкісним розташуванням даних. Інший дефект стосувався обробки зображень і виникав лише при використанні надмірно великого обсягу пам’яті. Крім того, виявлено помилки при одночасній роботі з двома дескрипторами одного файлу та повторно підтверджено відому вразливість у бібліотеці lib­ex­pat для обробки XML.

Після виявлення проблем Claude самостійно пропонував виправлення й повторно будував математичні докази для оновлених версій. Дослідникам вдалося підтвердити: перевірені компоненти не спричиняють певних видів збоїв під час обробки вхідних даних обсягом до 64 мегабайт. Втім, розробники наголошують, що формальна верифікація не означає повної відсутності помилок — метод гарантує лише виконання тих умов, які були закладені в математичну модель.

Anthropіc і The­o­rem розраховують, що подальший розвиток ШІ дозволить перевіряти дедалі більше програмних компонентів. Це особливо важливо для бібліотек, які одночасно використовують тисячі застосунків і можуть ставати джерелом масових вразливостей.