ИИ Claude обнаружил сотни ошибок в программах, прошедших триллионы проверок
Компания Anthropic сообщила о масштабном эксперименте по поиску ошибок в программном обеспечении с помощью искусственного интеллекта Claude. Совместно со специалистами компании Theorem исследователи проверили 123 библиотеки с открытым исходным кодом и обнаружили сотни программных дефектов. Некоторые ошибки сохранялись годами, несмотря на триллионы запусков автоматизированных тестов. Разработчикам удалось не только выявить проблемы, но и математически подтвердить отсутствие определённых типов сбоев в исправленных версиях программ.
Главной особенностью проекта стало использование формальной верификации — метода, позволяющего математически доказать выполнение заданных требований к программе. В отличие от обычного тестирования, при котором проверяется множество отдельных сценариев, такой подход позволяет охватить все возможные входные данные в установленных пределах.
В основу исследования легли программные библиотеки из проекта Google OSS-Fuzz, предназначенного для автоматического поиска уязвимостей. Его инструменты постоянно подают программам случайные и специально изменённые данные, пытаясь вызвать сбои, переполнение памяти или другие ошибки.
Однако даже миллиарды проверок не гарантируют обнаружения редких дефектов. Некоторые проблемы проявляются только при необычном сочетании входных данных, которое автоматические тесты практически никогда не воспроизводят. В новом эксперименте Claude преобразовывал существующие тесты в математические условия, после чего составлял доказательства их выполнения. Проверка проводилась на уровне машинных инструкций архитектуры RISC-V, то есть уже скомпилированных программ.
За несколько недель система подготовила доказательства для 239 точек входа в 123 библиотеках. Общий объём составил около 180 миллионов строк кода на языке Rocq. Полученные доказательства проверялись отдельной программой, которая определяла, соответствуют ли они заданным математическим условиям. В процессе работы Claude выявил ряд необычных ошибок. Например, в одном из алгоритмов распаковки данных обнаружилась проблема, способная привести к записи информации за пределами выделенной памяти. Для её проявления требовался файл объёмом около 20 мегабайт с редким расположением данных.
Другой дефект был связан с обработкой изображений и возникал только при использовании значительно большего объёма памяти. Кроме того, исследователи обнаружили ошибки при одновременной работе с двумя дескрипторами одного файла и повторно выявили известную уязвимость в библиотеке обработки XML libexpat. После обнаружения ошибок Claude мог самостоятельно предлагать исправления, а затем повторно строить доказательства для обновлённых версий программ.
Исследователям удалось подтвердить, что проверенные программные компоненты не вызывают определённых видов сбоев при обработке входных данных объёмом менее 64 мегабайт. При этом доказательства действуют только для конкретных сборок, работающих в рамках заданной модели процессора RISC-V и операционной системы Linux. Разработчики подчёркивают, что формальная верификация не означает полного отсутствия ошибок. Метод гарантирует лишь выполнение тех условий, которые были включены в математическую модель. Уязвимости, не охваченные проверкой, могут сохраняться.
Тем не менее результаты показывают возможность значительно расширить применение формальных методов в разработке программного обеспечения. Ранее подобные проверки требовали большого объёма ручной работы и преимущественно использовались в критически важных системах.
Anthropic и Theorem рассчитывают, что дальнейшее совершенствование ИИ позволит проверять таким способом всё больше программных компонентов. Это особенно важно для библиотек, которые одновременно используются тысячами приложений и могут становиться источником массовых уязвимостей.