Claude формально довів безпеку 123 бібліотек
Frontier Red Team Anthropic і Theorem Labs навчили Claude формальної верифікації — математичного доведення, що код відповідає заданій властивості. За кілька тижнів Claude перевірив 123 open-source бібліотеки на рівні асемблера; раніше така робота займала роки праці експертів. Раніше команда просканувала 25 проєктів і знайшла 493 проблеми, 94 з яких — вимкнені засоби захисту.
Формальна верифікація раніше була доступна лише критичним системам через дорогу працю експертів. AI здешевлює процес — доказова безпека може стати нормою і для звичайного коду.
Від виявлення багів до доведення їх відсутності
Традиційне тестування безпеки знаходить проблеми, але не дає гарантій — воно показує, що певних багів не знайшли, а не що їх немає. Формальна верифікація працює інакше: це математичний доказ того, що код відповідає заданій властивості. Команда Anthropic формулює це прямо: Потрібні способи довести, що код не містить багів — бо AI вже легко знаходить і використовує вразливості в типовому коді, а звичні захисні заходи цього не компенсують.
Раніше ціна такого доказу була занадто високою для масового застосування. Верифікація вимагала стільки роботи експертів, що її дозволяли собі лише невеликі кодові бази або системи, де збій коштував би дорожче за саму перевірку.
Чому рівень асемблера — найскладніша частина
Асемблер — це набір низькорівневих інструкцій, які безпосередньо виконує процесор, під тими мовами програмування, якими пишуть розробники. Довести властивість на цьому рівні означає міркувати про те, що машина реально зробить, а не про те, що автор коду мав на увазі. Claude перевірив властивості безпеки на рівні асемблера для 123 open-source бібліотек за кілька тижнів — обсяг роботи, який раніше вимагав би років праці фахівців.
Попередня робота: 493 знайдені проблеми
До проєкту з верифікацією команда вже проводила аналіз поверхні атаки на 25 open-source проєктах — понад 5 мільйонів рядків коду мовами C, C++, Java, PHP і Python. Аналіз виявив 493 проблеми, частина з них — критичні вразливості. Серед них 94 випадки, коли засоби захисту в коді були вимкнені.
Обидва проєкти входять до ширшої ініціативи Anthropic з безпеки open-source коду, яка включає інструмент під назвою OSS Scanner.
Де проходить межа методу
Доказ вартий рівно того, яку властивість він доводить. Формальна верифікація підтверджує, що код відповідає заданій специфікації — але будь-який прогал у самій специфікації залишається прогалом, навіть якщо математичний доказ коректний. Тобто метод гарантує відповідність заданим правилам, а не відсутність усіх можливих проблем узагалі.
Співпраця з компанією Theorem Labs показує, що для Anthropic це радше інструментальна задача, ніж чисто дослідницька. Чи перетвориться підхід на звичну інфраструктуру безпеки, чи залишиться демонстрацією можливостей, залежатиме від того, наскільки легко інші команди зможуть відтворити цю роботу. Умов доступу та вартості верифікації для сторонніх команд матеріал не наводить.