Claude обнаружил сотни скрытых уязвимостей в ПО

Модель искусственного интеллекта Claude, разработанная компанией Anthropic, успешно выявила сотни ранее незамеченных ошибок в программном обеспечении. Эти недостатки оставались скрытыми, несмотря на многократные автоматизированные проверки, проводившиеся в течение многих лет. В рамках проекта с фирмой Theorem, специализирующейся на верификации ПО, Claude проанализировал безопасность 123 библиотек с открытым исходным кодом, используя метод математических доказательств.

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

Применение математических доказательств для анализа ПО

В процессе анализа модель Claude трансформировала существующие фаз-тесты в формальные математические спецификации. Затем ИИ сгенерировал доказательства, подтверждающие, что 239 точек входа в 123 библиотеках не приведут к сбоям при определенных условиях. Исследовался ассемблерный код архитектуры RISC-V, отображающий инструкции процессора.

В ходе работы Claude сгенерировал около 180 миллионов строк кода доказательства, при этом типичное сформированное доказательство охватывает примерно 600 000 строк. Независимый инструмент Rocq верифицировал соответствие сгенерированных доказательств спецификациям. Модель самостоятельно исправляла обнаруженные ошибки и создавала новые доказательства для обновленного программного обеспечения, что освободило разработчиков от необходимости ручной проверки каждой строки кода.

Уязвимости, которые годами оставались незамеченными

Новый метод позволил обнаружить дефекты, которые долгое время ускользали от внимания тестировщиков. Среди них:

• Счетчик недополнения, способный вызвать запись за пределы допустимых значений при декомпрессии.
• Ошибка в декодере изображений, для обнаружения которой требовалось около 64 МБ данных и более 2 ГБ оперативной памяти.
• Считывание вне разрешенного диапазона, зависящее от последовательности операций с дескрипторами файлов.
• Уязвимость в популярном XML-парсер libexpat.
• Логическая ошибка, позволяющая обойти функцию ограничения загрузки файлов.

Ограничения и перспективы метода

Представители Anthropic подчеркивают, что формально проверенное ПО не становится полностью безошибочным. Гарантии безопасности распространяются только на конкретные свойства, входные данные и предположения, описанные в каждом доказательстве. Текущие тесты охватывают однопоточные и статически связанные программы RISC-V в смоделированной среде Linux.

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