Компания Anthropic официально заявила об успешном применении своей модели Claude для проверки безопасности 123 библиотек с открытым кодом. Используя передовые математические доказательства, искусственный интеллект смог обнаружить сотни скрытых ошибок и уязвимостей, которые традиционные методы тестирования пропускали на протяжении многих лет.
Математический подход к верификации кода
В рамках совместного проекта со специализирующейся на верификации программ фирмой Theorem разработчики из Anthropic применили строгие математические доказательства непосредственно к скомпилированному машинному коду. Традиционные инструменты тестирования и фаззинга генерируют большой объем входных данных, но физически не могут перебрать все возможные комбинации для гарантии безопасности.
Для решения этой задачи модель Claude преобразовала существующие фаз-тесты в четкие математические спецификации. Это позволило искусственному интеллекту сгенерировать доказательства того, что 239 точек входа в 123 библиотеках гарантированно не приведут к сбоям при выполнении определенных условий в ассемблерном коде архитектуры RISC-V.
Автоматизация проверки и исправления ошибок
Для независимой проверки сгенерированных доказательств соответствия спецификациям исследователи задействовали отдельный инструмент под названием Rocq. Такой подход полностью освободил разработчиков от необходимости вручную проверять каждую строчку программного кода.
Более того, нейросеть продемонстрировала способность не только находить дефекты, но и самостоятельно их исправлять, а также создавать новые доказательства для обновленного программного обеспечения. Это существенно ускоряет цикл разработки и повышает общую надежность критически важных компонентов.
Обнаруженные уязвимости и ограничения метода
Новая методика позволила выявить сложные дефекты, усколькавшие от внимания тестировщиков годами. Среди них — счетчик недополнения, способный спровоцировать запись за пределы допустимых значений, ошибка в декодере изображений, считывание вне разрешенного диапазона и логическая ошибка обхода функции ограничения загрузки файлов.
Несмотря на впечатляющие результаты, специалисты Anthropic подчеркивают, что формально проверенное программное обеспечение не становится абсолютно безупречным. Полученные гарантии распространяются исключительно на конкретные свойства, входные данные и предположения, заложенные в каждое отдельное доказательство в рамках смоделированной среды Linux.
Значение технологии для будущего разработки
Внедрение моделей искусственного интеллекта в процесс математической верификации открывает новые перспективы для обеспечения кибербезопасности во всем мире. Ожидается, что дальнейшее совершенствование технологий и возможность повторного использования доказательств позволят кратно снизить финансовые и временные затраты на аудит сложнейших программных систем.
