Скрытые ошибки в ПО: 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.

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