Виталик Бутерин: формальная верификация с помощью искусственного интеллекта — это будущее безопасной разработки программного обеспечения

Оглавление Виталик Бутерин выдвинул оптимистическую точку зрения на будущее кибербезопасности, утверждая, что формальная проверка с помощью ИИ может фундаментально изменить способ написания безопасного программного обеспечения. Вместо того, чтобы рассматривать ИИ как угрозу безопасности кода, Бутерин рассматривает его как инструмент, который в сочетании с формальной проверкой может создавать математически проверенное и высокоэффективное программное обеспечение. Его точка зрения бросает вызов растущему пессимизму в отрасли по поводу кибератак с использованием искусственного интеллекта. Новый подход к разработке программного обеспечения набирает обороты в исследовательских кругах Ethereum. Разработчики пишут код на языках низкого уровня или непосредственно на Lean — языке, используемом для проверяемых математических доказательств. Целью является код, корректность которого можно проверить автоматически и математически. Бутерин описывает этот метод как потенциально преобразующий, цитируя исследователя Йоичи Хираи, который называет его «окончательной формой разработки программного обеспечения». Такой подход полностью отделяет эффективность от читабельности. Одна версия кода работает быстро; другой написан ясно для человеческого понимания, и их связывает доказательство. Это особенно важно для систем с высокими ставками, таких как ZK-EVM, квантово-устойчивые подписи и алгоритмы консенсуса. Эти системы сложны в построении, но обладают свойствами безопасности, которые легко формально сформулировать. Именно в этом разрыве между сложностью и ясностью формальная проверка работает лучше всего. Такие проекты, как Arklib и evm-asm, уже применяют этот метод к инфраструктуре Ethereum. Проект evm-asm создает реализацию EVM непосредственно на сборке RISC-V, а затем формально доказывает, что она соответствует читаемой высокоуровневой версии. Некоторые представители отрасли утверждают, что обнаружение ошибок с помощью искусственного интеллекта делает невозможным безопасное и не требующее доверия программное обеспечение. Многие люди утверждают, что при обнаружении ошибок с помощью ИИ безопасный код (и, следовательно, не заслуживающий доверия что-либо) будет невозможен. У меня гораздо более оптимистичный взгляд, и формальная проверка с помощью искусственного интеллекта является основной причиной того, почему: https://t.co/0ceMBZ6uqj — vitalik.eth (@VitalikButerin) 18 мая 2026 г. Бутерин прямо опровергает эту точку зрения. Он рассматривает текущий период как переходный вызов, а не как постоянный сдвиг в пользу нападающих. Он полагает, что, как только ситуация стабилизируется, защита станет сильнее, чем раньше. В качестве подтверждающего доказательства он указывает на работу Mozilla. Mozilla отметила, что дефекты безопасности ограничены и что теперь у защитников есть реальный способ найти их все. Традицию шифропанка, основанную на идее о том, что цифровые защитники имеют преимущество, не следует отказываться. Модель Бутерина разделяет программное обеспечение на доверенное безопасное ядро ​​и менее доверенные периферийные компоненты. Edge работает в песочницах с минимальными разрешениями. Ядро, намеренно оставленное небольшим, получает все преимущества формальной проверки с помощью ИИ. Бутерин старается не преувеличивать важность формальной проверки. Несколько задокументированных сбоев показывают его реальные пределы. Ошибки появлялись в формально проверенных компиляторах C, где определенные ограничения просто не были указаны. Уязвимость 2025 года в libcrux показала, что непроверенные встроенные оболочки могут повредить выходные данные на определенных аппаратных платформах. Другая ошибка привела к сбою процесса из-за необработанной ошибки расшифровки в коде за пределами проверенной части. Характер сбоев одинаков: либо была проверена только часть кода, либо критическое свойство не было включено в доказательство. Формальная проверка не может доказать правильность программного обеспечения в полном человеческом смысле этого слова, а лишь то, что указанные свойства сохраняются при определенных предположениях. Атаки по побочным каналам представляют собой еще одну границу. Даже хорошо зарекомендовавшая себя схема шифрования может привести к утечке секретного ключа из-за электрических колебаний. Математические модели злоумышленников не всегда отражают все реальные типы утечек. Вывод Бутерина взвешен. Формальная проверка не является полным решением, но она является мощным катализатором уже существующей тенденции в области безопасности, которую ИИ делает значительно более доступной.