Оригинальное название: A shallow dive into formal verification
Оригинальный автор: Vitalik
Перевод: Peggy, BlockBeats
Примечание редактора: По мере быстрого совершенствования способностей ИИ к программированию безопасность программного обеспечения сталкивается с новым парадоксом: ИИ может генерировать код более эффективно, но также и обнаруживать уязвимости более эффективно. Для криптоиндустрии этот вопрос особенно критичен. В случае обнаружения дефектов в смарт-контрактах, ZK-доказательствах, алгоритмах консенсуса и системах ончейн-активов последствия часто не сводятся к обычным программным ошибкам, а ведут к необратимым финансовым потерям и разрушению доверия.
В данной статье Виталик обсуждает другой путь обеспечения безопасности кода в эпоху ИИ: формальную верификацию. Проще говоря, это не полагается на проверку кода человеком-аудитором построчно, а заключается в формулировании математических утверждений о свойствах, которым программа должна удовлетворять, и последующей проверке этих свойств с помощью машинно-проверяемых доказательств. В прошлом формальная верификация из-за высокой сложности и громоздкости процесса оставалась относительно нишевой областью исследований и инженерии; но с развитием ИИ, способного помогать в написании кода и доказательств, этот метод вновь обретает практическую значимость.
Ключевой вывод статьи не в том, что «формальная верификация может решить все проблемы безопасности». Напротив, Виталик неоднократно напоминает, что так называемая «доказуемая безопасность» не равна абсолютной безопасности: доказательства могут упускать ключевые предположения, спецификация может быть написана с ошибкой, неверифицированный код, границы оборудования и атаки по сторонним каналам также могут стать новыми источниками риска. Но она по-прежнему предлагает более надежную парадигму безопасности: выражение намерений разработчика различными способами с последующей автоматической проверкой их совместимости.
Это особенно важно для Ethereum. Будущий Ethereum будет все больше зависеть от сложных низкоуровневых компонентов, включая STARK, ZK-EVM, квантово-устойчивые подписи, алгоритмы консенсуса и высокопроизводительные реализации EVM. Реализация этих систем чрезвычайно сложна, но их ключевые цели безопасности часто могут быть относительно четко формализованы. Именно в таких сценариях формальная верификация с помощью ИИ может раскрыть максимальную ценность: ИИ берет на себя написание эффективного кода и доказательств, а человек проверяет, действительно ли доказанные утверждения соответствуют желаемым целям безопасности.
В более широком смысле, эта статья также является ответом Виталика на вопросы кибербезопасности в эпоху ИИ. Перед лицом более сильных ИИ-атак ответ заключается не в отказе от открытого исходного кода, смарт-контрактов или возврате к зависимости от централизованных институтов, а в сжатии критически важных систем до более компактного, верифицируемого и доверенного «безопасного ядра». ИИ приведет к появлению огромного количества некачественного кода, но также может сделать действительно важный код более безопасным, чем когда-либо прежде.
Далее следует оригинальный текст:
Особая благодарность Йоичи Хираи, Джастину Дрейку, Надиму Кобейсси и Алекс Хиксу за отзывы и рецензирование этой статьи.
За последние несколько месяцев в передовых кругах исследований Ethereum и во многих других уголках вычислительной сферы стремительно набирает популярность новая парадигма программирования: разработчики пишут код непосредственно на очень низкоуровневых языках, таких как байткод EVM, ассемблер или Lean, и проверяют его корректность с помощью автоматически проверяемых математических доказательств, также написанных в Lean.
При правильном использовании этот подход способен порождать чрезвычайно эффективный код и обеспечивать гораздо более высокий уровень безопасности по сравнению с прошлыми методами разработки программного обеспечения. Йоичи Хираи назвал это «конечной формой разработки программного обеспечения». Эта статья попытается объяснить основную логику этого подхода: что на самом деле может делать формальная верификация программного обеспечения и где лежат её ограничения и границы — как в контексте Ethereum, так и в более широкой сфере разработки ПО.
Что такое формальная верификация?
Формальная верификация — это написание доказательств математических теорем таким способом, который может быть автоматически проверен машиной.
В качестве относительно простого, но всё же интересного примера можно рассмотреть базовую теорему о последовательности Фибоначчи: каждое третье число является четным, а остальные два — нечетными.
Простой метод доказательства — использование математической индукции, продвигаясь вперед на три шага каждый раз.
Сначала рассмотрим базовый случай. Пусть F1 = F2 = 1, F3 = 2. Непосредственным наблюдением видно, что утверждение — «когда i кратно 3, Fi четно; в остальных случаях Fi нечетно» — выполняется для x <= 3.
Далее, индукционный шаг. Предположим, что утверждение выполняется для всех чисел до 3k+3 включительно, то есть мы знаем четность F3k+1, F3k+2, F3k+3: нечетное, нечетное, четное. Тогда мы можем вычислить четность следующей тройки чисел:
Таким образом, мы перешли от «утверждение выполняется до 3k+3» к «утверждение выполняется до 3k+6». Продолжая это рассуждение, мы убеждаемся, что закономерность верна для всех целых чисел.
Для человека это аргумент убедительный. Но что, если то, что вы пытаетесь доказать, в сто раз сложнее, и вам действительно хочется убедиться, что вы не допустили ошибку? Тогда вы можете построить доказательство, которое убедит и компьютер.
Оно будет выглядеть примерно так:
Это то же самое рассуждение, но выраженное на Lean — языке программирования, часто используемом для написания и проверки математических доказательств.
Он выглядит иначе, чем моё «человеческое» доказательство выше, и на то есть веская причина: то, что интуитивно понятно компьютеру (в старом смысле этого слова — детерминированным программам из операторов if/then, а не большим языковым моделям), и то, что интуитивно понятно человеку, — это совершенно разные вещи.
В этом доказательстве вы не заостряете внимание на факте, что fib(3k+4) = fib(3k+3) + fib(3k+2); вы утверждаете, что fib(3k+3) + fib(3k+2) нечетно, и тактика omega в Lean, несмотря на своё громкое название, автоматически объединит это с её пониманием определения fib(3k+4).
В более сложных доказательствах иногда приходится явно указывать на каждом шаге, какой именно математический закон позволяет вам сделать этот шаг, и эти законы иногда имеют туманные названия вроде Prod.mk.inj. С другой стороны, вы можете в один шаг развернуть огромное полиномиальное выражение, используя всего одну строку с вызовом omega или ring.
Эта неинтуитивность и громоздкость — важная причина, по которой машинно-проверяемые доказательства, существующие почти 60 лет, оставались нишевой областью. Но в то же время многие вещи, которые раньше казались почти невозможными, быстро становятся достижимыми благодаря быстрому прогрессу ИИ.
Верификация компьютерных программ
Здесь вы можете подумать: Хорошо, значит, мы можем заставить компьютер проверять доказательства математических теорем, и теперь мы наконец сможем выяснить, какие из новых безумных открытий о простых числах верны, а какие — ошибки, скрытые в сотнях страниц PDF-статей. Может быть, мы даже сможем разобраться, верно ли доказательство Шиничи Мочидзуки гипотезы ABC! Но какая практическая польза от этого, кроме удовлетворения любопытства?
Ответов может быть много. Для меня один очень важный ответ таков: верификация корректности компьютерных программ, особенно тех, которые связаны с криптографией или безопасностью. В конце концов, компьютерная программа сама по себе является математическим объектом. Следовательно, доказательство того, что программа ведет себя определенным образом, по сути является доказательством математической теоремы.
Например, предположим, вы хотите доказать, действительно ли безопасно шифрованное коммуникационное ПО, такое как Signal. Сначала вы математически определяете, что именно означает «безопасность» в данном контексте. В общих чертах, вы хотите доказать, что при определенных криптографических предположениях любой, кто не обладает приватным ключом, не может получить никакой информации о содержимом сообщения. На практике, конечно, существует множество видов действительно важных свойств безопасности.
И оказывается, что действительно есть команда, пытающаяся это выяснить. Одна из предложенных ими теорем безопасности выглядит примерно так:
Вот резюме Leanstral о значении этой теоремы:
Теорема passive_secrecy_le_ddh представляет собой компактную редукцию, показывающую, что в модели случайного оракула (Random Oracle Model) пассивная секретность сообщений X3DH не менее стойка, чем предположение DDH.
Другими словами, если атакующий может скомпрометировать пассивную секретность сообщений X3DH, то он также может скомпрометировать DDH. Поскольку DDH обычно считается сложной проблемой, X3DH также можно считать устойчивым к пассивным атакам.
Теорема доказывает, что если атакующий может только пассивно наблюдать за сообщениями обмена ключами Signal, то он не может отличить сформированный сеансовый ключ от случайного ключа с вероятностью выше пренебрежимо малой.
Объединив это с доказательством корректной реализации шифрования AES, вы получите доказательство того, что механизм шифрования протокола Signal устойчив к пассивному атакующему.
Аналогичные верификационные проекты существуют для доказательства безопасности реализаций TLS и других криптографических компонентов в браузерах.
Если вы можете осуществить сквозную формальную верификацию, то вы доказываете не только то, что теоретическое описание протокола безопасно, но и то, что конкретный код, который фактически запускают пользователи, безопасен на практике. С точки зрения пользователя, это значительно повышает степень «недоверия» (trustlessness): чтобы полностью доверять этому коду, вам не нужно построчно проверять всю кодовую базу, достаточно проверить уже доказанные утверждения.
Конечно, здесь есть очень важные оговорки, особенно касающиеся того, что именно означает слово «безопасный». Легко забыть доказать действительно важное утверждение; легко столкнуться с ситуацией, когда доказываемое утверждение не имеет более лаконичного описания, чем сам код; легко незаметно внести в доказательство предположения, которые в итоге не выполняются. Также легко решить, что только часть системы действительно требует формального доказательства, но затем подвергнуться критической атаке через другую часть или даже на уровне аппаратного обеспечения. Даже сама реализация Lean может содержать ошибки. Но прежде чем углубляться в эти неприятные детали, давайте посмотрим, какую почти утопическую перспективу может открыть идеально и правильно выполненная формальная верификация.
Формальная верификация для безопасности
Ошибки (баги) в компьютерном коде сами по себе вызывают беспокойство.
Когда вы помещаете криптовалюту в неизменяемые ончейн смарт-контракты, баги становятся ещё страшнее. Потому что если в коде есть ошибка, северокорейские хакеры могут автоматически перевести все ваши деньги, и у вас почти не будет возможности их вернуть.
Когда всё это обернуто в нуль-знание доказательства (ZK-доказательства), баги становятся ещё страшнее. Потому что если кому-то удастся скомпрометировать ZK-систему, они смогут вывести все средства, и мы можем вообще не понять, что пошло не так — или, что ещё хуже, можем даже не знать, что проблема уже возникла.
Когда у нас есть мощные модели ИИ, баги также становятся ещё страшнее. Например, модель вроде Claude Mythos после двух лет улучшений, возможно, уже сможет автоматически находить такие уязвимости.
Некоторые, столкнувшись с этой реальностью, начали выступать за отказ от самой идеи смарт-контрактов и даже полагать, что киберпространство в принципе не может быть областью, где защищающаяся сторона имеет асимметричное преимущество перед атакующей.
Вот несколько цитат:
Чтобы укрепить систему, вам нужно потратить на поиск уязвимостей больше токенов, чем атакующий потратит на их использование.
И ещё:
Наша индустрия строилась вокруг детерминированного кода. Напиши код, протестируй, запусти и знай, что он работает — но, по моему опыту, этот договор нарушается. Среди лучших операторов по-настоящему нативных ИИ-компаний кодовая база уже начинает превращаться во что-то, «во что ты веришь, что оно работает», и вероятность, соответствующая этой вере, уже не может быть точно определена.
Что ещё хуже, некоторые считают, что единственное решение — отказаться от открытого исходного кода.
Для кибербезопасности это было бы мрачное будущее. Особенно мрачное для тех, кто заботится о децентрализации и свободе интернета. Весь дух крипто-панков по сути основан на идее, что в интернете защищающаяся сторона имеет преимущество. Построить цифровой «замок» — будь то шифрование, подпись или доказательство — легче, чем разрушить его. Если мы потеряем это, то безопасность в интернете будет обеспечиваться только за счёт экономии на масштабе, за счёт преследования потенциальных атакующих по всему миру и, в более широком смысле, выбором между двумя вариантами: либо властвуй над всем, либо погибай.
Я не согласен с такой оценкой. У меня гораздо более оптимистичное видение будущего кибербезопасности.
Я считаю, что вызов, создаваемый мощными способностями ИИ к обнаружению уязвимостей, действительно серьёзен, но это переходный вызов. Когда пыль уляжется и мы войдём в новое равновесие, мы окажемся в состоянии, более благоприятном для защищающейся стороны, чем когда-либо прежде.
Mozilla также согласна с этим. Процитируем их:
Возможно, вам придётся пересмотреть приоритеты всех других дел и посвятить себя этой задаче последовательно и целенаправленно. Но в конце туннеля есть свет. Мы очень гордимся тем, как команда взялась за этот вызов, и другие тоже смогут. Наша работа ещё не завершена, но мы миновали переломный момент и начинаем видеть лучшее будущее, которое не сводится к простому «не отставать». У защищающейся стороны наконец-то появился шанс на решающую победу.
......
Количество дефектов конечно, и мы вступаем в мир, где наконец можно найти их все.
Теперь, если вы нажмёте Ctrl+F в этой статье Mozilla и поищете «formal» и «verification», вы обнаружите, что ни одного из этих слов там нет. Позитивное будущее кибербезопасности не зависит строго от формальной верификации или любой другой отдельной технологии.
От чего же оно зависит? По сути, вот от этой диаграммы:
За последние десятилетия многие технологии способствовали тренду «снижения количества уязвимостей»:
Системы типов;
Языки с безопасной памятью;
Улучшения архитектуры ПО, включая песочницы, модели разрешений и, в более общем плане, чёткое разграничение «доверенной вычислительной базы» (trusted computing base) и «остального кода»;
Улучшенные методы тестирования;
Накопление знаний о безопасных и небезопасных шаблонах кодирования;
Всё больше предварительно написанных и проверенных библиотек.
Формальную верификацию с помощью ИИ не следует рассматривать как совершенно новую парадигму, а скорее как мощный ускоритель: она ускоряет тренд и парадигму, которые уже продвигались вперёд.
Формальная верификация — не панацея. Но в некоторых сценариях она особенно применима: когда цель гораздо проще конкретной реализации. Это особенно заметно в некоторых из самых сложных технологий, которые необходимо развернуть для следующей крупной итерации Ethereum, таких как квантово-устойчивые подписи, STARK, алгоритмы консенсуса и ZK-EVM.
STARK — это очень сложное программное обеспечение. Но ключевое свойство безопасности, которое оно реализует, легко понять и формализовать: если вы видите доказательство, указывающее на хеш H программы P, входа x и выхода y, то либо хеш-алгоритм, используемый STARK, скомпрометирован, либо P(x) = y. Поэтому существует проект Arklib, пытающийся создать полностью формально верифицированную реализацию STARK. Другой связанный проект — VCV-io, предоставляющий базовую инфраструктуру оракульных вычислений, которую можно использовать для формальной верификации различных криптографических протоколов, многие из которых сами являются зависимостями STARK.
Более амбициозен evm-asm: проект, пытающийся построить полную реализацию EVM и формально её проверить. Здесь свойства безопасности менее очевидны. Проще говоря, его цель — доказать, что эта реализация эквивалентна другой реализации EVM, написанной на Lean; последняя же может стремиться к максимальной интуитивности и читаемости без учёта эффективности выполнения.
Конечно, теоретически возможна ситуация, когда у нас есть десять реализаций EVM, все доказаны как эквивалентные друг другу, но все они имеют один и тот же фатальный недостаток, который каким-то образом позволит атакующему перевести все ETH с адреса, которым он не управляет. Но вероятность этого гораздо ниже, чем вероятность наличия такого недостатка в одной отдельной реализации EVM сегодня. Другое важное свойство безопасности, которое мы по-настоящему осознали благодаря горькому опыту, — устойчивость к DoS-атакам — относительно легко конкретизировать.
Ещё два важных направления:
Византийские отказоустойчивые алгоритмы консенсуса. Здесь также нелегко формально определить все желаемые свойства безопасности. Но, учитывая, что связанные баги были очень распространены, попытка формальной верификации всё же стоит того. Поэтому уже ведутся работы над реализацией консенсуса на Lean и её доказательствами.
Языки программирования для смарт-контрактов. Примеры включают работу по формальной верификации в Vyper и Verity.
Во всех этих случаях огромная добавочная ценность формальной верификации заключается в том, что доказательства являются действительно сквозными. Многие самые сложные баги — это интерактивные баги, возникающие на стыке двух подсистем, рассматриваемых отдельно. Для человека сквозное рассуждение о всей системе слишком сложно; но автоматизированная система проверки по правилам может с этим справиться.
Формальная верификация для эффективности
Вернёмся к evm-asm. Это реализация EVM.
Но это реализация EVM, написанная прямо на ассемблере RISC-V.
Буквально на ассемблере.
Вот опкод ADD:
RISC-V выбран потому, что создаваемые в настоящее время ZK-EVM провераторы обычно работают, доказывая выполнение RISC-V и компилируя клиенты Ethereum в RISC-V. Следовательно, если вы напишете реализацию EVM прямо на RISC-V, теоретически это должна быть самая быстрая возможная реализация. RISC-V также может очень эффективно эмулироваться на обычных компьютерах, и существуют ноутбуки на RISC-V. Конечно, для настоящей сквозной проверки вам также потребуется формально проверить саму реализацию RISC-V или арифметизированное представление провератора. Но не беспокойтесь — такая работа тоже уже ведётся.
Писать код прямо на ассемблере — это то, что мы часто делали пятьдесят лет назад. С тех пор мы постепенно перешли к написанию кода на языках высокого уровня. Языки высокого уровня жертвуют некоторой эффективностью, но взамен позволяют писать код гораздо быстрее и, что важнее, понимать чужой код гораздо быстрее — что необходимо для безопасности.
Благодаря сочетанию формальной верификации и ИИ у нас есть шанс «вернуться в будущее». А именно: позволить ИИ писать ассемблерный код, а затем писать формальные доказательства, проверяющие, что этот ассемблерный код обладает нужными свойствами. По крайней мере, этим целевым свойством может быть просто полная эквивалентность реализации, написанной на удобном для человека языке высокого уровня и оптимизированной для читаемости.
Таким образом, больше не нужно балансировать между читаемостью и эффективностью в одном объекте кода. У нас будет два отдельных объекта: ассемблерная реализация, оптимизированная только для эффективности и адаптированная к конкретным требованиям среды выполнения; и утверждение о безопасности (или реализация на языке высокого уровня), оптимизированная только для читаемости. Затем мы используем математическое доказательство для доказательства их эквивалентности. Пользователь может один раз автоматически проверить это доказательство; после этого ему нужно будет просто запускать быструю версию.
Это очень мощно. Недаром Йоичи Хираи называет это «конечной формой разработки программного обеспечения».
Формальная верификация — не панацея
В криптографии и информатике существует традиция, почти столь же древняя, как и сами формальные методы: критика формальных методов или, в более широком смысле, критика зависимости от «доказательств». В литературе есть множество практических примеров. Начнём с более простых рукописных доказательств ранней криптографии. Менезес и Коблиц критиковали их в 2004 году:
В 1979 году Рабин предложил шифрующую функцию, которая в некотором смысле «доказуемо» безопасна, то есть обладает свойством безопасности с редукцией.
Утверждение о безопасности с редукцией гласит: любой, кто может найти сообщение m по шифртексту y, также должен уметь факторизовать n.
Вскоре после того, как Рабин представил свою схему шифрования, Ривест отметил, что ирония в том, что именно та характеристика, которая придавала ей дополнительную безопасность, также делает систему полностью уязвимой для другого типа атакующего. Такие атакующие называются «атакующими с выбранным шифртекстом». Конкретно, предположим, что атакующий может каким-то образом заставить Алису расшифровать шифртекст, выбранный самим атакующим. Тогда атакующий может факторизовать n, используя тот же процесс, который использовал Сэм в предыдущем абзаце.
Затем Менезес и Коблиц приводят ещё несколько примеров. Вместе они демонстрируют паттерн: проектирование криптографических протоколов вокруг того, что «легче доказать», часто делает протокол менее «естественным» и более уязвимым к компрометации в сценариях, которые проектировщик вообще не рассматривал.
Теперь вернёмся к машинно-проверяемым доказательствам и коду. Вот пример из статьи 2011 года, где авторы нашли баг в формально верифицированном C-компиляторе:
Вторая обнаруженная нами проблема в CompCert проявляется в двух багах. Эти баги генерируют код, похожий на следующий: stwu r1, -44432(r1)
Здесь выделяется большой кадр стека PowerPC. Проблема в том, что происходит переполнение 16-битного поля смещения. Семантика PPC в CompCert не определяет ограничений на ширину этого непосредственного значения, поскольку предполагается, что ассемблер перехватит значения вне диапазона.
Ещё одна статья 2022 года:
В CompCert-KVX коммит e2618b31 исправляет баг: инструкция «nand» выводилась как «and»; а «nand» выбиралась только в редком режиме ~(a & b). Этот баг был обнаружен при компиляции случайно сгенерированных программ.
Сегодня, в 2026 году, Надим Кобейсси, описывая уязвимости в формально верифицированном ПО от Cryspen, пишет:
В ноябре 2025 года Филиппо Вальсорда независимо сообщил, что libcrux-ml-dsa v0.0.3 генерирует разные открытые ключи и подписи на разных платформах при одинаковых детерминированных входных данных. Этот баг находился в обёртке встроенной функции _vxarq_u64, которая реализует операцию XAR, используемую в перестановке Keccak-f SHA-3. Резервный путь передавал неверные параметры операции сдвига, что приводило к порче дайджестов SHA-3 на платформах ARM64 без аппаратной поддержки SHA-3. Это провал типа I: эта встроенная функция была помечена как проверенная, в то время как весь бэкенд NEON не имел завершённых доказательств безопасности или корректности во время выполнения.
И ещё:
Крейт libcrux-psq реализует постквантовый протокол предварительного общего ключа. В методе decrypt_out путь расшифровки AES-GCM 128 вызывает .unwrap() для результата расшифровки вместо передачи ошибки дальше. Некорректный шифртекст может привести к краху процесса.
Все четыре вышеуказанные проблемы можно отнести к двум категориям:
Первая: проверена только часть кода, потому что проверить остальное слишком сложно; и оказывается, что непроверенный код содержит более критические баги, чем предполагали авторы.
Вторая: авторы забыли явно определить какое-то ключевое свойство, которое следовало доказать.
Статья Надима классифицирует режимы отказов формальной верификации; он также перечисляет другие типы отказов. Например, ещё один основной тип: формальная спецификация сама по себе неверна, или доказательство содержит ошибочное утверждение, которое система сборки молча принимает.
Наконец, можно рассмотреть отказы формальной верификации на стыке программного и аппаратного обеспечения. Здесь частая проблема — способность системы проверки противостоять атакам по сторонним каналам. Даже если вы защищаете сообщение теоретически совершенно безопасным шифрованием, но кто-то в нескольких метрах может уловить электрические колебания и извлечь ваш приватный ключ после сотен тысяч шифрований, вы всё равно не в безопасности.
«Дифференциальный анализ энергопотребления» (differential power analysis) — это ныне хорошо изученный пример такой техники.
Дифференциальный анализ энергопотребления — распространённая атака по стороннему каналу. Источник: Wikipedia
В прошлом также предпринимались попытки доказать, что системы устойчивы к таким атакующим. Однако любое такое доказательство требует какой-то математической модели атакующего, в рамках которой можно доказать безопасность. Иногда используется «d-probing model»: предполагается, что существует известный предел количества точек в цепи, которые атакующий может зондировать. Но проблема в том, что некоторые формы утечек не улавливаются этой моделью.
Одна из распространённых проблем, отмеченных в этой статье, — утечка при переходах (transitional leakage): если наблюдаемый сигнал зависит не от конкретного значения в точке, а от изменения этого значения, то часто можно восстановить нужную информацию из двух значений — старого и нового — а не полагаясь только на одно значение. В статье также классифицируются другие формы утечек.
На протяжении десятилетий эта критика формальной верификации, в свою очередь, помогала улучшать её. По сравнению с прошлым, мы теперь лучше осведомлены об этих проблемах. Но даже сегодня она всё ещё не идеальна.
Если взглянуть шире, здесь есть общая нить: формальная верификация мощна. Но как бы её ни рекламировали как средство достижения «доказуемой корректности», эта самая «доказуемая корректность» по своей сути не доказывает, что программное или аппаратное обеспечение «корректно» в истинном смысле слова.
Для большинства людей «корректность» в целом означает: вещь ведёт себя в соответствии с пониманием пользователем намерений разработчика.
А «безопасность» в целом означает: вещь не ведёт себя таким образом, который отклоняется от ожиданий пользователя и наносит ему ущерб.
В обоих случаях корректность и безопасность в конечном итоге сводятся к сравнению: с одной стороны — математический объект, с другой — человеческие намерения или ожидания. Строго говоря, человеческие намерения и ожидания сами являются математическими объектами — в конце концов, человеческий мозг — часть вселенной, а вселенная подчиняется законам физики; при достаточной вычислительной мощности их теоретически можно смоделировать. Но это чрезвычайно сложные математические объекты, которые ни компьютер, ни мы сами не можем по-настоящему понять или даже прочитать. Для практических целей мы можем считать их чёрными ящиками. Мы вообще имеем какое-то понимание своих намерений и ожиданий только благодаря многолетнему опыту наблюдения за собственными мыслями и вывода о мыслях других.
И именно потому, что мы не можем напрямую засунуть исходные человеческие намерения в компьютер, формальная верификация не может доказать сравнение между системой и человеческим намерением. Следовательно, «доказуемая корректность» и «доказуемая безопасность» на самом деле не доказывают «корректность» и «безопасность» в человеческом понимании — ни один метод не сможет сделать этого, пока мы не сможем смоделировать человеческий мозг.
Так в чём же реальная польза формальной верификации?
Я склонен рассматривать тестовые наборы, системы типов и формальную верификацию как разные реализации одного и того же базового подхода к безопасности языков программирования — возможно, это единственный разумный взгляд. Их общая черта: избыточное описание наших намерений разными способами с последующей автоматической проверкой их совместимости.
Например, рассмотрим следующий код на Python:
Здесь вы выразили своё намерение тремя разными способами:
Первый, прямой способ: через код, реализующий формулу Фибоначчи.
Второй, косвенный способ: через систему типов, указывающую, что вход, выход и промежуточные шаги рекурсии являются целыми числами.
Третий, способ «пакета примеров»: тестовые случаи.
При запуске этого файла система использует эти примеры для проверки выполнения формулы. Проверка типов может удостовериться, что типы совместимы: сложение двух целых чисел — допустимая операция, результатом которой будет другое целое число. Системы типов часто полезны и в физических вычислениях: если вы рассчитываете ускорение, но получаете результат в м/с, а не в м/с², вы знаете, что где-то ошиблись. А определения в стиле «пакетов примеров», одним из видов которых являются тестовые случаи, часто также ближе к тому, как люди обрабатывают концепции, чем прямые, явные определения.
Чем большим количеством разных способов вы сможете выразить своё намерение, тем лучше; в идеале эти способы должны достаточно сильно отличаться, чтобы заставить вас думать об одной и той же проблеме по-разному. Таким образом, если все эти выражения окажутся совместимыми, то выше вероятность того, что вы действительно выразили то, что хотели.
Суть безопасного программирования — выразить ваши намерения множеством разных способов, а затем автоматически проверить, совместимы ли эти выражения друг с другом.
Формальная верификация может продвинуть этот метод дальше. С её помощью вы можете описывать свои намерения практически любым количеством избыточных способов; программа пройдёт проверку только в том случае, если все эти описания будут совместимы.
Вы можете одновременно написать оптимизированную реализацию и очень неэффективную, но удобочитаемую для человека реализацию, а затем проверить их эквивалентность. Вы можете попросить десять друзей перечислить математические свойства, которым, по их мнению, должна удовлетворять программа, а затем проверить, удовлетворяет ли программа всем им; если нет — определить, ошибочна ли программа или само математическое свойство. А ИИ может сделать всю эту работу чрезвычайно эффективной.
Как же мне начать?
Реалистично говоря, вы, вероятно, не будете лично писать доказательства. Фундаментальная причина, по которой формальные методы так и не стали по-настоящему массовыми, в том, что большинству людей очень трудно понять, как, чёрт возьми, писать эти самые доказательства.
Можете ли вы сказать, что означает следующий код?
(Если интересно, это один из многих вспомогательных лемм в доказательстве конкретного утверждения безопасности для одного из вариантов подписи SPHINCS: а именно, что если не произошло коллизии хешей, то для генерации подписи для одного сообщения по сравнению с подписью любого другого сообщения требуется использование значения, находящегося выше по цепочке хешей хотя бы в одной позиции. Следовательно, информацию, необходимая для этого, невозможно вычислить из другой подписи.)
Вам не нужно писать код и доказательства вручную; вместо этого позвольте ИИ написать программу за вас — прямо на Lean или, если вам нужна скорость, на ассемблере — и в процессе доказать все нужные вам свойства.
Одно из преимуществ этой задачи в том, что она по своей сути самопроверяема, поэтому вам не нужно постоянно следить за ней. Вы вполне можете позволить ИИ работать самостоятельно несколько часов подряд. В худшем случае он будет топтаться на месте, не добиваясь прогресса; или, как однажды сделал мой Leanstral, чтобы облегчить себе работу, просто заменит утверждение, которое его просили доказать.
В конечном итоге вам нужно будет проверить: действительно ли доказанное утверждение — это то, что вы хотели доказать.
В этом варианте подписи SPHINCS окончательное утверждение выглядит так:
Это уже почти на грани «читаемости»:
Если число (dig1), сгенерированное из одного хеш-дайджеста, не равно числу (dig2), сгенерированному из другого хеш-дайджеста, то следующее утверждение ложно:
Для всех цифр, каждая цифра dig1 меньше или равна соответствующей цифре dig2;
Для всех цифр, каждая цифра dig2 меньше или равна соответствующей цифре dig1.
Здесь сравниваются «расширенные цифры» (wotsFullDigits), сгенерированные после добавления контрольной суммы (checksum). То есть, неизбежно, на некоторых позициях расширенная цифра dig1 будет выше, а на других — расширенная цифра dig2 будет выше.
В написании доказательств с помощью больших языковых моделей я обнаружил, что Claude уже достаточно хорош, DeepSeek 4 Pro также вполне справляется. Leanstral — многообещающая альтернатива: это модель с открытыми весами, специализированно дообученная для написания на Lean. Она имеет 119 миллиардов параметров, но активирует только 6 миллиардов параметров на токен, поэтому может работать локально, хотя и медленно — на моём ноутбуке примерно 15 токенов в секунду.
Согласно бенчмаркам, Leanstral превосходит многие гораздо более крупные общие модели:
По моему текущему личному опыту, он немного слабее, чем DeepSeek 4 Pro, но всё же эффективен.
Формальная верификация не решит всех наших проблем. Но если мы хотим построить модель интернет-безопасности, при которой не все доверяют нескольким могущественным организациям, то нам нужно иметь возможность доверять коду — даже перед лицом мощных ИИ-противников. Формальная верификация с помощью ИИ может стать важным шагом в этом направлении.
Как блокчейн и ZK-SNARK, ИИ и формальная верификация — высоко взаимодополняющие технологии.
Блокчейн обеспечивает открытую проверяемость и устойчивость к цензуре ценой приватности и масштабируемости; а ZK-SNARK возвращают приватность и масштабируемость — фактически, даже сильнее, чем раньше.
ИИ позволяет писать код в больших масштабах, но ценой снижения точности; а формальная верификация возвращает точность — фактически, тоже сильнее, чем раньше.
По умолчанию ИИ породит огромное количество очень сырого кода, и количество багов увеличится. Действительно, в некоторых сценариях увеличение количества багов может быть правильным компромиссом: если их влияние невелико, то даже несовершенное ПО лучше, чем его отсутствие. Но здесь по-прежнему существует оптимистичное будущее для кибербезопасности: программное обеспечение продолжит разделяться на «небезопасные периферийные компоненты», окружающие «безопасное ядро».
Эти небезопасные периферийные компоненты будут запускаться в песочницах и получать минимально необходимые привилегии для выполнения своих задач. Безопасное ядро будет управлять всем. Если безопасное ядро падёт, падёт всё — ваши личные данные, ваши деньги и многое другое. Но если небезопасный периферийный компонент выйдет из строя, безопасное ядро всё равно сможет защитить вас.
Когда дело доходит до безопасного ядра, мы не позволим распространяться коду с багами. Мы будем активно контролировать размер безопасного ядра, сохраняя его достаточно небольшим или даже сокращая дальше. Вместо этого мы направим все дополнительные возможности, предоставляемые ИИ, на повышение безопасности самого безопасного ядра, позволяя ему нести высокое бремя доверия в высокоцифровом обществе.
Ядро вашей операционной системы, или по крайней мере его часть, станет одним из таких безопасных ядер. Ethereum станет другим. В идеале, по крайней мере во всех не высокопроизводительных вычислениях, используемое вами аппаратное обеспечение станет третьим безопасным ядром. Некоторые системы, связанные с Интернетом вещей, станут четвёртым.
По крайней мере в этих безопасных ядрах старое утверждение — «баги неизбежны, вы можете лишь попытаться найти их раньше атакующего» — перестанет быть верным. Его заменит более многообещающий мир, в котором мы можем достичь подлинной безопасности.
Конечно, если вы захотите доверить свои активы и данные плохо написанному ПО, которое может случайно отправить их все в чёрную дыру, у вас по-прежнему будет такая свобода.
Ссылка на оригинал
