Компанія Anthropic офіційно заявила про успішне застосування своєї моделі Claude для перевірки безпеки 123 бібліотек з відкритим кодом. Використовуючи передові математичні доведення, штучний інтелект зміг виявити сотні прихованих помилок та вразливостей, які традиційні методи тестування пропускали протягом багатьох років.

Математичний підхід до верифікації коду

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

Для розв'язання цього завдання модель Claude перетворила наявні фаз-тести на чіткі математичні специфікації. Це дозволило штучному інтелекту згенерувати доведення того, що 239 точок входу в 123 бібліотеках гарантовано не призведуть до збоїв за виконання певних умов в асемблерному коді архітектури RISC-V.

Автоматизація перевірки та виправлення помилок

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

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

Виявлені вразливості та обмеження методу

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

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

Значення технології для майбутнього розробки

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