Claude создал машинопроверяемые доказательства безопасности для 123 библиотек

Исследователи представили результаты крупномасштабного проекта, в рамках которого языковая модель Claude сгенерировала машинопроверяемые формальные доказательства безопасности на уровне ассемблерного кода RISC-V для сотен точек входа фазз-тестирования. Эта работа охватила 123 открытые библиотеки в сотрудничестве со специалистами Theorem.

Согласно обнародованным данным, модель самостоятельно исправляла обнаруженные уязвимости, после чего доказывала корректность программ для всех входных данных объемом менее 64 МБ с учетом смоделированных реакций ОС Linux. Проект демонстрирует новые возможности применения искусственного интеллекта для верификации промышленного софта.

Превращение фазз-тестов в формальные доказательства

Методика заключается в преобразовании компилируемых фазз-тестов каждой библиотеки в строгую спецификацию. Главное правило такой спецификации кодирует простое требование: тест никогда не завершается аварийно при любых входных данных заданного объема. Описание формируется на основе скомпилированных инструкций RISC-V с использованием семантики Theorem для набора инструкций и процессов Linux, а специальный инструмент проверки Rocq верифицирует готовый результат.

Данный подход был применен к многочисленным проектам из инициативы OSS-Fuzz компании Google, автоматически инструментирующей код на языках C и C++ с помощью AddressSanitizer. В техническом приложении уточняется, что за время работы Claude написала около одного миллиарда строк кода на языке Rocq, из которых примерно 180 миллионов строк успешно прошли проверку. Например, для парсера cJSON потребовалось сгенерировать доказательство объемом 630 тысяч строк, а для библиотеки fftw3 этот показатель составил 480 тысяч строк.

Обнаруженные уязвимости в процессе верификации

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

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

Дополнительные эксперименты и оценка эффективности

Помимо проектов из OSS-Fuzz, разработчики поручили ИИ сформулировать спецификацию технического документа RFC 1950 для формата сжатия zlib и доказать корректность ее реализации в ядре Linux. Модель успешно верифицировала скомпилированный под архитектуру x86 бинарный файл, используя самостоятельно созданную формальную семантику набора инструкций x86. Побочным эффектом этого этапа стало обнаружение сотен неточностей в официальной справочной документации и нескольких аппаратных дефектов.

В рамках другого эксперимента Claude спроектировала интерпретатор подмножества языка Python на Rust и доказала его соответствие семантике CPython. Эмпирическое тестирование миллионов сгенерированных программ подтвердило идентичность поведения в подавляющем большинстве случаев. При оценке производительности выяснилось, что применение совместного рабочего пространства, где агенты могут заимствовать чужие успешные доказательства, снижает расход токенов на семнадцать процентов по сравнению с изолированной работой.

Ограничения метода и программа OSS Verify

Авторы исследования подчеркивают, что наличие формальных доказательств не гарантирует абсолютное отсутствие багов: оставшиеся проблемы могут находиться внутри доверенных компонентов или за пределами текущей области видимости. Рассмотренные бинарные файлы работают как однопоточные статические приложения под RISC-V с лимитом памяти, тогда как на практике пользователи чаще запускают софт на других архитектурах с динамической связкой библиотек.

Для развития технологии инициатива OSS Verify предлагает бесплатный конвейер проверки квалифицированным проектам с открытым исходным кодом. Разработчики могут подать заявку через стандартный pull request, добавив конфигурационные файлы в репозиторий программы. Сопровождающие ПО получают готовое машинное доказательство для каждого целевого объекта, а обнаруженные уязвимости передаются авторам в частном порядке без жестких дедлайнов на публичное раскрытие.