# Claude нашёл скрытые ошибки в открытом ПО

ИИ · 23 октября 2026, 03:02 · Новости будущего
Адрес: https://xn----btbbgegr2bjbg3anrb0h.xn--p1ai/2026/10/23/claude-nashel-skrytye-oshibki-v-otkrytom-po/

Компания Anthropic обнаружила сотни ошибок в библиотеках открытого программного обеспечения с помощью модели Claude

Модель Claude совместно с компанией Theorem применила математические доказательства непосредственно к скомпилированному машинному коду. В ходе работы проверили свойства безопасности в 123 библиотеках открытого ПО и выявили сотни ошибок, которые оставались незамеченными годами, несмотря на триллионы автоматических тестов.

Claude превратил существующие фаззинг-тесты — проверки, при которых на вход программе подают необычные данные, — в математические спецификации, то есть строгие описания того, как должна вести себя программа. Модель написала около 180 миллионов строк проверочного кода: в среднем одно доказательство занимало около 600 тысяч строк. Затем отдельная программа Rocq проверила, что доказательства действительно соответствуют спецификациям, — поэтому разработчикам не нужно вручную проверять каждую строку кода.

Среди обнаруженных ошибок — переполнение счётчика при распаковке сжатых данных: из-за него программа могла записать информацию за пределы отведённой ей памяти, но только если получала на вход около 20 МБ данных, расположенных редким образом. Ещё одна ошибка нашлась в декодере изображений — программе, которая открывает картинки: чтобы она проявилась, нужны были входные данные объёмом 64 МБ и более 2 ГБ памяти. Нашлись и другие уязвимости, в том числе уже известная проблема в библиотеке libexpat, которая разбирает файлы формата XML.

Формальная верификация — проверка программы строгими математическими методами — позволяет доказать, что код соблюдает определённые правила при заданных условиях, и помогает находить дефекты, которые пропускают обычные тесты. При этом программа, проверенная таким образом, не обязательно свободна от ошибок: гарантии действуют только для тех свойств, входных данных и предположений, которые описаны в каждом доказательстве.

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

Источник: [Interesting Engineering](https://interestingengineering.com/ai-robotics/claude-formal-verification-software-security)
Теги: искусственный интеллект, программное обеспечение, формальная верификация, ошибки в по, безопасность по