Claude нашёл скрытые ошибки в открытом ПО
Компания Anthropic обнаружила сотни ошибок в библиотеках открытого программного обеспечения с помощью модели Claude
Модель Claude совместно с компанией Theorem применила математические доказательства непосредственно к скомпилированному машинному коду. В ходе работы проверили свойства безопасности в 123 библиотеках открытого ПО и выявили сотни ошибок, которые оставались незамеченными годами, несмотря на триллионы автоматических тестов.
Claude превратил существующие фаззинг-тесты — проверки, при которых на вход программе подают необычные данные, — в математические спецификации, то есть строгие описания того, как должна вести себя программа. Модель написала около 180 миллионов строк проверочного кода: в среднем одно доказательство занимало около 600 тысяч строк. Затем отдельная программа Rocq проверила, что доказательства действительно соответствуют спецификациям, — поэтому разработчикам не нужно вручную проверять каждую строку кода.
Среди обнаруженных ошибок — переполнение счётчика при распаковке сжатых данных: из-за него программа могла записать информацию за пределы отведённой ей памяти, но только если получала на вход около 20 МБ данных, расположенных редким образом. Ещё одна ошибка нашлась в декодере изображений — программе, которая открывает картинки: чтобы она проявилась, нужны были входные данные объёмом 64 МБ и более 2 ГБ памяти. Нашлись и другие уязвимости, в том числе уже известная проблема в библиотеке libexpat, которая разбирает файлы формата XML.
Формальная верификация — проверка программы строгими математическими методами — позволяет доказать, что код соблюдает определённые правила при заданных условиях, и помогает находить дефекты, которые пропускают обычные тесты. При этом программа, проверенная таким образом, не обязательно свободна от ошибок: гарантии действуют только для тех свойств, входных данных и предположений, которые описаны в каждом доказательстве.
Anthropic рассчитывает, что в будущем улучшенные модели и повторно используемые доказательства снизят затраты на проверку критически важных компонентов ПО. Если разработчики смогут один раз проверить широко используемые библиотеки и повторно применять полученные гарантии, это повысит безопасность множества приложений, которые от них зависят.
Ранее по теме: ИИ нашёл уязвимости в криптографических алгоритмах
Источник: Interesting Engineering
