Приховані помилки у ПЗ: Claude знайшов сотні багів, які тести пропускали роками

Штучний інтелект успішно впорався із завданням перевірки безпеки ПЗ.

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

Цей підхід дозволяє зробити ретельну перевірку доступною для набагато ширшого кола технологічних проєктів.

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

Не пропустіть: Запобігти ядерній катастрофі: GPT і Claude дозволили пожертвувати чоловіками

Як Claude створює математичні докази?

Для аналізу Anthropic використала модель Claude, яка перетворила наявні фаз-тести на чіткі математичні специфікації. Після цього ШІ згенерував докази того, що 239 точок входу у 123 бібліотеках не спричинять збоїв за визначених умов.

Під час роботи досліджувався асемблерний код архітектури RISC-V, який відображає інструкції процесора:

• Claude згенерував приблизно 180 мільйонів рядків коду доказу
• Типовий сформований доказ охоплює близько 600000 рядків

Окремий незалежний інструмент під назвою Rocq перевірив згенеровані докази на відповідність специфікаціям.

Це звільнило розробників від необхідності вручну перевіряти кожен рядок коду. Більше того, модель самостійно виправляла знайдені помилки та генерувала нові докази для оновленого програмного забезпечення.

Читайте більше: ШІ самостійно зламав понад 100 сайтів: одна атака коштувала хакеру лише 50 доларів

Вразливості, які витримали роки випробувань

Завдяки новому методу вдалося виявити дефекти, які роками залишалися поза увагою звичайних тестувальників:

Лічильник недоповнення, що міг спровокувати запис за межі допустимих значень під час декомпресії.

Помилка у декодері зображень, для виявлення якої знадобилося ввести майже 64 МБ даних та понад 2 ГБ оперативної пам'яті.

Зчитування за межами дозволеного діапазону залежно від послідовності операцій з дескрипторами файлів.

Вразливість у популярному XML-парсері libexpat.

Логічна помилка, яка дозволяла обійти функцію обмеження завантаження файлів.

Цікаво дізнатися: Контроль замість безпеки: OpenAI та Anthropic приховують звіти про ризики ШІ

Обмеження методу та плани на майбутнє

Незважаючи на виняткові результати, в Anthropic наголошують, що формально перевірене ПЗ не стає повністю безпомилковим. Отримані гарантії поширюються лише на конкретні властивості, вхідні дані та припущення, описані в кожному окремому доказі.

Поточні тести охоплюють лише однопотокові та статично зв'язані програми RISC-V у змодельованому середовищі Linux.

З усім тим, компанія очікує, що вдосконалення моделей та можливість повторного використання доказів дозволять суттєво знизити вартість перевірки критичних компонентів у майбутньому.