17:33 23.10.2026 Пт 3 мин
ИИ проверил безопасность 123 библиотек (коллаж: РБК-Украина) Додати як бажане джерело в Google
Anthropic заявила, что модель Claude официально проверила свойства безопасности 123 библиотек с открытым кодом и обнаружила сотни скрытых ошибок благодаря использованию математических доказательств.
Об этом пишет РБК-Украина со ссылкой на Interesting Engineering.
Искусственный интеллект успешно справился с задачей проверки безопасности ПО.
В рамках совместного проекта с фирмой Theorem, специализирующейся на верификации программ, разработчики Anthropic применили математические доказательства непосредственно к скомпилированному машинному коду.
Этот подход позволяет сделать тщательную проверку доступной для гораздо более широкого круга технологических проектов.
Разработчики отметили, что традиционные инструменты тестирования и фаззинга генерируют большое количество входных данных, однако физически не способны исчерпать все возможные комбинации.
Не пропустите: Предотвратить ядерную катастрофу: GPT и Claude позволили пожертвовать мужчинами
Как Claude создает математические доказательства?
Для анализа Anthropic использовала модель Claude, которая превратила существующие фаз-тесты в четкие математические спецификации. После этого ИИ сгенерировал доказательства того, что 239 точек входа в 123 библиотеках не повлекут за собой сбоев при определенных условиях.
В ходе работы исследовался ассемблерный код архитектуры RISC-V, отображающий инструкции процессора:
Отдельный независимый инструмент под названием Rocq проверил сгенерированные доказательства соответствия спецификациям.
Это освободило разработчиков от необходимости вручную проверять каждую строчку кода. Более того, модель самостоятельно исправляла найденные ошибки и создавала новые доказательства для обновленного программного обеспечения.
Читайте больше: ИИ самостоятельно сломал более 100 сайтов: одна атака стоила хакеру всего 50 долларов
Уязвимости, выдержавшие годы испытаний
Благодаря новому методу удалось обнаружить дефекты, которые годами оставались без внимания обычных тестировщиков:
Счетчик недополнения, который мог спровоцировать запись за пределы допустимых значений во время декомпрессии.
Ошибка в декодере изображений, для обнаружения которой потребовалось ввести около 64 МБ данных и более 2 ГБ оперативной памяти.
Считывание вне разрешенного диапазона в зависимости от последовательности операций с дескрипторами файлов.
Уязвимость в популярном XML-парсере libexpat.
Логическая ошибка, позволяющая обойти функцию ограничения загрузки файлов.
Интересно узнать: Контроль вместо безопасности: OpenAI и Anthropic скрывают отчеты о рисках ИИ
Ограничение метода и планы на будущее
Несмотря на исключительные результаты, в Anthropic подчеркивают, что формально проверенное ПО не становится полностью безошибочным. Полученные гарантии распространяются только на конкретные свойства, входные данные и предположения, описанные в каждом отдельном доказательстве.
Текущие тесты охватывают только однопоточные и статически связанные программы RISC-V в смоделированной среде Linux.
Со всем тем компания ожидает, что совершенствование моделей и возможность повторного использования доказательств позволят существенно снизить стоимость проверки критических компонентов в будущем.
