Виталик: Что является ключевым для следующего этапа развития Ethereum?

Автор: Виталик Бутерин

Перевод: Цзя Хуань, ChainCatcher

Особая благодарность Юичи Хираи, Джастину Дрейку, Надиму Кобейсси и Алексу Хиксу за обратную связь и рецензирование.

В последние несколько месяцев новая парадигма программирования стремительно набирает популярность в передовых кругах исследований Ethereum, а также во многих других областях вычислительной техники: написание кода непосредственно на очень низкоуровневых языках (например, байт-коде EVM, ассемблере) или на Lean с последующей верификацией его корректности с помощью автоматически проверяемых математических доказательств, также написанных на Lean.

При правильном применении это не только может порождать чрезвычайно эффективный код, но и обеспечить значительно более высокий уровень безопасности по сравнению со всеми предыдущими методами программирования. Юичи Хираи называет это «окончательной формой разработки программного обеспечения».

В этой статье мы попытаемся раскрыть её основные принципы, обсудить возможности формальной верификации программного обеспечения, а также её слабые стороны и ограничения в контексте Ethereum и других областей.

Что такое формальная верификация?

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

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 ...

Простой способ доказать это — математическая индукция с шагом три.

Сначала базовый случай. Пусть F₁ = F₂ = 1, F₃ = 2. Непосредственным наблюдением видно, что утверждение («Fᵢ чётно при i, кратном трём, и нечётно в остальных случаях») выполняется для всех i < 3.

Затем индукционный переход. Предположим, что утверждение верно до 3k+3, то есть нам известна чётность F₃ₖ₊₁, F₃ₖ₊₂ и F₃ₖ₊₃: нечётное, нечётное, чётное. Мы можем вычислить чётность следующей тройки чисел:

F₃ₖ₊₄ = F₃ₖ₊₂ + F₃ₖ₊₃ = нечётное + чётное = нечётное
F₃ₖ₊₅ = F₃ₖ₊₃ + F₃ₖ₊₄ = чётное + нечётное = нечётное
F₃ₖ₊₆ = F₃ₖ₊₄ + F₃ₖ₊₅ = нечётное + нечётное = чётное

Таким образом, из предположения о справедливости утверждения до 3k+3 мы вывели его справедливость до 3k+6. Повторяя этот вывод многократно, мы можем убедиться, что правило выполняется для всех целых чисел.

Это рассуждение убеждает человека. Но что, если нужно доказать нечто в сто раз более сложное и быть абсолютно уверенным в отсутствии ошибок? В таком случае можно предоставить компьютеру доказательство, которое он сможет принять как достоверное.

Вот как это выглядит на практике:

-- Последовательность Фибоначчи: fib 0 = 0, fib 1 = 1, fib 2 = 1 (индексы смещены на 1)
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n + 1) + fib n
-- Утверждение: fib (3k+1) нечётно, fib (3k+2) нечётно, fib (3k+3) чётно.
-- Эквивалентно: каждое третье число Фибоначчи, начиная с fib 3, чётно.
-- Мы доказываем все три утверждения одновременно по индукции по k,
-- поскольку каждый следующий блок строится на основе предыдущего.
theorem fib_triple (k : Nat) :
    fib (3 * k + 1) % 2 = 1 ∧
    fib (3 * k + 2) % 2 = 1 ∧
    fib (3 * k + 3) % 2 = 0 := by
  induction k with
  | zero => decide
  | succ k ih =>
    -- Переписываем новые индексы в форме (что-то) + 2, чтобы fib раскрылся.
    refine ⟨?_, ?_, ?_⟩
    · show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1
      omega
    · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1
      omega
    · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)
        + (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0
      omega

Это то же самое рассуждение, но выраженное на языке Lean — языке программирования, широко используемом для написания и верификации математических доказательств.

Оно выглядит иначе по сравнению с приведённым выше «человеческим» доказательством — и не без причины: то, что интуитивно понятно компьютеру (в традиционном смысле — детерминированной программы, состоящей из if/then-конструкций, а не крупных языковых моделей), кардинально отличается от того, что интуитивно понятно человеку.

В приведённом выше доказательстве вы не акцентируете внимание на факте, что fib(3k+4) = fib(3k+3) + fib(3k+2), а вместо этого указываете, что fib(3k+3) + fib(3k+2) — нечётное число, и стратегия Lean с громким названием «omega» автоматически сопоставляет это с её знанием определения fib(3k+4).

В более сложных доказательствах иногда требуется явно указывать на каждом шаге, какой именно математический закон позволяет совершить данный шаг, а иногда даже использовать такие экзотические имена, как Prod.mk.inj.

С другой стороны, вы можете раскрыть огромное полиномиальное выражение за один шаг и доказать его корректность одной строкой, например «omega» или «ring».

Эта неинтуитивность и трудоёмкость в значительной степени объясняют, почему, несмотря на существование машинно-проверяемых доказательств почти 60 лет, эта область остаётся нишевой. Однако с быстрым развитием искусственного интеллекта многие ранее невозможные задачи сейчас становятся достижимыми.

Когда математические доказательства начинают защищать код

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

Может быть, нам даже удастся понять, верны ли утверждения Синъити Мотидзуки о гипотезе ABC!

Но отбросив любопытство, какая от этого польза?

На этот вопрос существует множество возможных ответов. Для меня особенно важен один: верификация корректности компьютерных программ, особенно тех, которые выполняют криптографические или иные задачи, связанные с безопасностью.

В конце концов, компьютерная программа — это математический объект, и доказательство того, что программа работает определённым образом, само по себе является математической теоремой.

Например, предположим, вы хотите доказать, действительно ли безопасно шифрованное коммуникационное ПО Signal. Вы можете строго определить, что «безопасность» означает в данном контексте с математической точки зрения.

На высоком уровне вы должны доказать, что при выполнении некоторых криптографических допущений только владелец закрытого ключа может получить какую-либо информацию о содержании сообщения. На практике существует множество различных свойств безопасности, каждое из которых критически важно.

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

theorem passive_secrecy_le_ddh
  (g : G)
  (adv : PassiveAdversary G SK) :
  passiveSecrecyAdvantage (F := F) g adv ≤
    ProbComp.boolDistAdvantage
      (DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))
      (DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

Вот краткое описание смысла этого утверждения от Leanstral:

Теорема passive_secrecy_le_ddh представляет собой компактное сведение, показывающее, что пассивная конфиденциальность сообщений X3DH не легче, чем гипотеза DDH в модели случайного оракула. Если противник может взломать пассивную конфиденциальность сообщений X3DH, он также может взломать DDH.

Поскольку мы предполагаем, что DDH взломать сложно, X3DH безопасен против пассивных атак. Теорема доказывает, что если противник может пассивно наблюдать сообщения обмена ключами Signal, он не сможет отличить полученный им сессионный ключ от случайного ключа с вероятностью, превышающей пренебрежимо малую величину.

Если совместить это с доказательством корректности реализации AES, получится полное доказательство того, что протокол Signal криптографически безопасен против пассивных атак.

Аналогичные проекты доказали безопасность реализаций TLS и других частей криптографии в браузерах.

Если провести полную формальную верификацию «от начала до конца», вы докажете не просто безопасность некой теоретической абстракции протокола, а то, что конкретный исполняемый код, запускаемый пользователями, безопасен на практике.

С точки зрения пользователя это резко повышает доверие без необходимости проверки: чтобы полностью доверять коду, вам не нужно просматривать весь код, достаточно лишь проверить заявления, для которых он был формально доказан.

Тем не менее, необходимо помнить ряд важнейших оговорок, особенно касающихся самого слова «безопасность» и того, что оно на самом деле означает.

Легко забыть доказать действительно важные утверждения. Часто оказывается, что формулировка доказываемого утверждения не проще, чем сам код.

Легко незаметно ввести в доказательство предположения, которые на самом деле неверны. Легко решить, что формально верифицировать нужно лишь одну часть системы, а затем оказаться уязвимым из-за серьёзных ошибок в других частях (или даже в аппаратном обеспечении).

Даже сама реализация Lean может содержать ошибки. Но прежде чем углубляться во все эти досадные детали, давайте сначала подробнее рассмотрим утопическую перспективу, которую открывает правильная и идеальная формальная верификация.

Формальная верификация ради безопасности

Ошибки в компьютерном коде ужасны.

Они становятся ещё ужаснее, когда вы помещаете криптовалюту в неизменяемый смарт-контракт на блокчейне, а Северная Корея может мгновенно опустошить ваш счёт при первой же ошибке кода, и вы ничего не сможете с этим поделать.

Они становятся ещё ужаснее, когда всё это завёрнуто в доказательства с нулевым разглашением: если злоумышленник взломает систему ZK-доказательств, он сможет вывести все средства, и мы даже не узнаем, что пошло не так (а ещё хуже — не узнаем, когда это произошло).

Они становятся ещё ужаснее, когда у нас есть мощные ИИ-модели, например Claude Mythos через два года, способные автоматически находить такие ошибки.

Реакция некоторых людей на такую реальность — призыв отказаться от самой идеи смарт-контрактов и даже утверждение, что киберпространство вообще не может стать областью, где защитники обладают асимметричным преимуществом над атакующими.

Некоторые цитаты:

«Чтобы укрепить систему, вам нужно потратить больше токенов на поиск уязвимостей, чем атакующий тратит на их эксплуатацию».

И:

«Наша отрасль основана на детерминированном коде. Мы пишем его, тестируем, выпускаем и уверены, что он будет работать. Но, по моему опыту, этот договор разрушается».

«В лучших операционных компаниях, ориентированных на ИИ, кодовая база уже превратилась в то, во что вы «верите», что она будет работать, но вы уже не можете точно указать вероятность её успешного выполнения».

Ещё хуже то, что некоторые считают единственным решением отказ от открытого исходного кода.

Для кибербезопасности это будет мралое будущее. Особенно для тех из нас, кто заботится о децентрализации и свободе интернета, это крайне пессимистичный сценарий.

Весь криптопанковский дух основан на идее, что в интернете защитники имеют преимущество: построить цифровой «замок» (будь то шифрование, подпись или доказательство) гораздо проще, чем его разрушить.

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

Я с этим не согласен и вижу более оптимистичное будущее кибербезопасности.

Я считаю, что вызов, связанный с мощными возможностями ИИ по поиску уязвимостей, серьёзен, но он временный. После того как пыль уляжется и установится новое равновесие, мы получим среду, ещё более благоприятную для защитников, чем раньше.

Mozilla разделяет мою точку зрения. Вот их слова:

«Возможно, вам придётся переприоритизировать все остальные задачи и сконцентрировать на этом постоянное и всестороннее внимание, но в конце туннеля есть свет».

«Мы очень гордимся тем, как наша команда приняла этот вызов, и другие тоже справятся. Наша работа ещё не завершена, но мы уже преодолели самый сложный этап и можем заглянуть в будущее, которое будет не просто «по успеванию», а гораздо прекраснее».

«Защитники наконец получили возможность одержать решающую победу… Дефекты конечны, и мы вступаем в эпоху, когда наконец сможем найти их все».

Если вы выполните поиск по слову «формальная» и «верификация» в посте Mozilla с помощью Ctrl+F, вы найдёте ноль совпадений. Позитивное будущее кибербезопасности не зависит исключительно от формальной верификации или какой-либо другой единой технологии.

От чего же оно зависит? В основном от следующей диаграммы:

Снижение количества уязвимостей CVE со временем

На протяжении десятилетий снижение количества уязвимостей обеспечивалось множеством технологий:

• Системы типов
• Языки с безопасностью памяти
• Улучшения программной архитектуры (включая песочницы, управление правами доступа и более чёткое разделение «доверенной вычислительной базы» и «остального кода»)
• Улучшенные методы тестирования
• Постоянное расширение знаний о безопасных и небезопасных шаблонах кодирования
• Постоянный рост числа заранее написанных и аудированных программных библиотек

Формальная верификация с поддержкой ИИ не должна рассматриваться как совершенно новая парадигма, а скорее как мощный ускоритель уже развивающихся тенденций и парадигм.

Формальная верификация не является панацеей. Она особенно эффективна, когда цель проще реализации. Это особенно актуально для некоторых чрезвычайно сложных и проблемных технологий, которые нам придётся развернуть в следующей главной итерации Ethereum: квантово-устойчивые подписи, STARK-доказательства, алгоритмы консенсуса и ZK-EVM.

STARK — это чрезвычайно сложное программное обеспечение. Однако его основные свойства безопасности легко понять и формализовать: если вы видите доказательство для хеша H программы P, входа x и выхода y, то либо (i) хеш-функция, используемая в STARK, скомпрометирована, либо (ii) P(x) = y.

Поэтому существует проект Arklib, который пытается создать полностью формально верифицированную реализацию STARK (см. VCV-io — она предоставляет базовую инфраструктуру оракулов для формальной верификации различных других криптографических протоколов, многие из которых являются зависимостями STARK).

Более амбициозный проект — evm-asm: попытка построить полностью формально верифицированную реализацию всего EVM.

Здесь свойства безопасности уже не так очевидны: в целом цель состоит в том, чтобы доказать её эквивалентность другой реализации EVM, написанной на Lean, но такая реализация может быть написана исключительно с учётом наглядности и читаемости, без каких-либо требований к производительности.

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

Но вероятность такой ошибки в одной из нынешних реализаций EVM значительно выше. А ещё одно важное свойство безопасности, значение которого мы осознали лишь после болезненных уроков — устойчивость к DoS-атакам — легко формализуется.

Ещё две важные области применения:

• Консенсус с устойчивостью к византийским сбоям. Здесь формализация всех требуемых свойств безопасности также затруднена, но учитывая, насколько распространены ошибки, это стоит попробовать. Поэтому в Lean уже существуют текущие реализации и доказательства консенсусных протоколов.
• Языки программирования для смарт-контрактов: см. формальную верификацию в Vyper и Verity.

Во всех этих случаях одна из главных добавленных ценностей формальной верификации — её по-настоящему «сквозная» природа. Обычно самые неприятные ошибки — это ошибки взаимодействия, скрывающиеся на стыке двух подсистем, рассматриваемых независимо.

Для человека рассуждать о всей системе «от начала до конца» слишком сложно. Автоматизированные системы проверки правил справляются с этим.

Формальная верификация ради эффективности

Вернёмся к evm-asm. Это реализация EVM. Но это реализация EVM, написанная непосредственно на ассемблере RISC-V.

Совершенно буквально.

Вот операция ADD:

import EvmAsm.Rv64.Program
namespace EvmAsm.Evm64
open EvmAsm.Rv64
/-- 256-битная EVM ADD: бинарная операция, извлекает 2 значения, помещает 1.
    Разряд 0: LD, LD, ADD, SLTU (перенос), SD (5 инструкций).
    Разряды 1–3: LD, LD, ADD, SLTU (перенос1), ADD (переносВх), SLTU (перенос2), OR (переносВых), SD (по 8 инструкций).
    Затем ADDI sp, sp, 32.
    Регистры: x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1. -/
def evm_add : Program :=
  -- Разряд 0 (5 инструкций)
  LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;
  -- Разряд 1 (8 инструкций)
  LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;
  -- Разряд 2 (8 инструкций)
  LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;
  -- Разряд 3 (8 инструкций)
  LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;
  -- Корректировка sp
  ADDI .x12 .x12 32
end EvmAsm.Evm64

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() для результата расшифровки вместо распространения ошибки. Некорректный шифртекст приводит к аварийному завершению процесса».

Все четыре проблемы относятся к одному из двух типов:

• Верифицирована лишь часть кода (потому что верификация остальной части слишком сложна), и оказалось, что неверифицированный код содержит больше ошибок, чем предполагали авторы (и более фатальных по характеру).
• Авторы забыли сформулировать ключевые свойства, которые необходимо было доказать.

Статья Надима содержит классификацию режимов отказа формальной верификации; он также приводит и другие типы (например, ещё один основной тип — «сама формальная спецификация ошибочна, или доказательство содержит ложные утверждения, которые система молча принимает»).

Наконец, рассмотрим отказы формальной верификации на границе программного и аппаратного обеспечения. Распространённой проблемой здесь является верификация устойчивости к атакам по побочным каналам.

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

Вот статья о «дифференциальном анализе потребляемой мощности» — это хорошо изученный пример подобной техники.

Дифференциальный анализ потребляемой мощности — один из распространённых типов атак по побочным каналам. Источник: Википедия

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

Иногда используется «модель d-запросов»: мы предполагаем, что у атакующего есть известное ограничение на количество позиций в схеме, к которым он может обращаться. Однако некоторые формы утечек эта модель не охватывает.

Как отмечено в этой статье, распространённой проблемой является переходная утечка: если вы можете наблюдать сигнал, зависящий не только от значения в какой-то позиции, но и от того, как это значение изменяется, этого часто достаточно, чтобы восстановить нужную информацию не из одного значения, а из двух (старого и нового).

В статье приводится классификация других форм утечек.

На протяжении десятилетий эти критические замечания помогали совершенствовать формальную верификацию. Сегодня мы гораздо лучше умеем обнаруживать подобные проблемы. Но даже сейчас она несовершенна.

В общем плане здесь прослеживается главная нить: формальная верификация мощна.

Но независимо от маркетинговых формулировок, делающих её похожей на «доказуемую корректность», такая «доказуемая корректность» принципиально не доказывает, что программное (или аппаратное) обеспечение является «корректным».

Согласно наиболее распространённому человеческому пониманию, «корректность» означает что-то вроде: «поведение объекта соответствует представлению пользователя о намерениях разработчика».

А «безопасность» означает что-то вроде: «поведение объекта не нарушает ожиданий пользователя и не причиняет вреда его интересам».

В обоих случаях корректность и безопасность сводятся к сравнению математического объекта с человеческими намерениями или ожиданиями.

Человеческие намерения и ожидания технически тоже являются математическими объектами, ведь человеческий мозг — часть Вселенной и следует физическим законам, которые можно смоделировать при достаточной вычислительной мощности.

Но они представляют собой невероятно сложные математические объекты, которые ни компьютеры, ни мы сами не можем понять или даже прочитать.

Для всех практических целей они являются «чёрными ящиками»; мы имеем какое-либо представление о собственных намерениях и ожиданиях лишь потому, что каждый из нас много лет наблюдает за своими мыслями и пытается делать выводы о мыслях других.

И поскольку мы не можем «впихнуть» первичные человеческие намерения в компьютер, формальная верификация не может доказать соответствие человеческим намерениям.

Следовательно, «доказуемая корректность» и «доказуемая безопасность» на самом деле не доказывают «корректность» и «безопасность» в том смысле, в котором их понимают люди. Ничто не сможет этого сделать, пока мы не научимся полностью моделировать человеческий мозг.

Так для чего же она тогда нужна?

Я склонен рассматривать наборы тестов, системы типов и формальную верификацию как различные реализации одного и того же базового подхода к безопасности языков программирования (это, возможно, единственный разумный подход).

Все они сводятся к тому, чтобы избыточно описывать наши намерения разными способами, а затем автоматически проверять, совместимы ли эти описания между собой.

Вот пример кода на Python:

def fib(n: int) -> int:
  if n < 0:
    raise Exception("Negative values not supported")
  elif 0 <= n < 2:
    return n
  else:
    return fib(n-1) + fib(n-2)
if __name__ == '__main__':
  assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]
  assert fib(15) == 610

Здесь вы выражаете своё намерение тремя различными способами:

• Явно — реализуя формулу Фибоначчи в коде
• Неявно — через систему типов (указывая, что вход, выход и промежуточные рекурсивные шаги — целые числа)
• Методом «пакета примеров» — тестовыми случаями

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

Системы типов часто хорошо подходят для проверки вычислений в физике: если вы вычисляете ускорение, но получаете ответ с размерностью метры/секунда вместо метров/секунда², вы сразу понимаете, что ошиблись.

А тестовые случаи — это конкретный пример определения «пакета примеров», которое для человека часто естественнее, чем прямое явное определение при работе с понятиями.

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

Безопасное программирование — это выражение своих намерений множеством различных способов и автоматическая проверка совместимости всех этих выражений.

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

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

Если нет — выяснить, ошибка в программе или в математическом свойстве. И вы можете выполнять все эти действия чрезвычайно эффективно с помощью ИИ.

С чего мне начать?

Реалистично говоря, вы не будете писать доказательства самостоятельно. Одна из причин, по которой формальные методы никогда не стали популярными, — это то, что большинству людей не удаётся понять, как писать эти загадочные конструкции. Сможете ли вы объяснить, что означает следующий фрагмент кода?

  /-- Вспомогательная функция: покомпонентное ≤ на уровне foldl с аккумулятором. -/
private theorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (a b : Nat) (hAcc : a ≤ b)
    (hLE : Forall₂ (· ≤ ·) ds1 ds2) :
  List.foldl (λ acc d => acc * w + d) a ds1 ≤
  List.foldl (λ acc d => acc * w + d) b ds2 := by
  match ds1, ds2, hLE with
  | [], [], .nil => exact hAcc
  | d1::ds1', d2::ds2', .cons hd htl =>
    simp [List.foldl]
    refine foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl
    exact Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

(Если вам интересно, это один из многих вспомогательных лемм в доказательстве определённого утверждения безопасности для варианта подписи SPHINCS.

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

Вам не нужно писать код и доказательства вручную. Просто поручите ИИ написать программу (либо напрямую на Lean, либо на ассемблере ради скорости) и доказать любые требуемые свойства в процессе.

Эта задача самопроверяема, поэтому вам не нужно контролировать процесс — просто запустите ИИ на несколько часов подряд.

Худший сценарий — он будет крутиться на месте без прогресса (или, как это делал мой leanstral, самостоятельно заменит утверждение, которое ему поручили доказать, чтобы облегчить себе работу).

Единственное, что вам нужно будет проверить в конце, — это то, что доказанное утверждение соответствует вашим требованиям.

В варианте подписи SPHINCS это финальное утверждение:

theorem wots_fullDigits_incomparable
  {dig1 dig2 : List Nat} {w l1 l2 : Nat}
  (hw : 0 < w)
  (hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)
  (hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)
  (hL2suff : l1 * (w - 1) < w ^ l2)
  (hNeq : dig1 ≠ dig2) :
  ¬ Forall₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧
  ¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

Это на грани того, что ещё можно прочитать:

Если цифры, сгенерированные из одного хеш-сводки (dig1), не равны цифрам, сгенерированным из другой хеш-сводки (dig2),

то ни одно из следующих утверждений не выполняется:

• Для всех цифр: цифра из dig1 ≤ цифра из dig2
• Для всех цифр: цифра из dig2 ≤ цифра из dig1

То же самое верно и для «расширенных цифр» (wotsFullDigits), сгенерированных с добавлением контрольной суммы. То есть в расширенной версии dig1 обязательно будут места, где цифры выше, а в других местах — цифры в расширенной версии dig2 будут выше.

При использовании крупных языковых моделей для написания доказательств я обнаружил, что и Claude, и Deepseek 4 Pro справляются хорошо. Leanstral — небольшая открытая модель с тонкой настройкой специально для написания Lean, и это многообещающая альтернатива.

У неё 119 млрд параметров, активируется 6 млрд на токен, и её можно запускать локально, хотя и медленно (на моём ноутбуке скорость около 15 ток/сек). По бенчмаркам Leanstral превосходит значительно более крупные универсальные модели:

Согласно моему текущему личному опыту, она немного уступает Deepseek 4 Pro, но остаётся весьма эффективной.

Формальная верификация не решит все наши проблемы.

Однако, если мы хотим, чтобы модель безопасности интернета больше не основывалась на всеобщем доверии к нескольким могущественным организациям, нам необходимо перейти к доверию коду — в том числе к доверию коду даже перед лицом мощных ИИ-противников.

Формальная верификация с поддержкой ИИ делает огромный шаг на пути к достижению этой цели.

Как и блокчейны и ZK-SNARKs, ИИ и формальная верификация — чрезвычайно взаимодополняющие технологии.

Блокчейны ценой конфиденциальности и масштабируемости предоставляют вам открытую верифицируемость и устойчивость к цензуре, а ZK-SNARKs возвращают вам конфиденциальность и масштабируемость (фактически даже больше, чем раньше).

ИИ ценой точности предоставляет вам возможность писать огромные объёмы кода, а формальная верификация возвращает вам точность (фактически даже выше, чем раньше).

По умолчанию ИИ породит огромное количество крайне небрежного кода, и количество ошибок возрастёт.

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

Но здесь кибербезопасность имеет оптимистичное будущее: программное обеспечение будет (продолжать) разделяться на «небезопасные периферийные части» вокруг «безопасного ядра».

Небезопасные периферийные части будут работать в песочницах и получать только минимальные права, необходимые для выполнения работы.

Безопасное ядро будет управлять всем. Если безопасное ядро выйдет из строя, всё рухнет — ваши личные данные, ваши деньги и т.д. Но если выйдет из строя какая-либо небезопасная периферийная часть, безопасное ядро по-прежнему защитит вас.

Когда речь идёт о безопасном ядре, мы не можем допустить распространения ошибочного кода. Мы примем решительные меры для минимизации его размера и даже дальнейшего сокращения.

Вместо этого мы направим всю дополнительную производительность, полученную от ИИ, исключительно на повышение безопасности безопасного ядра, чтобы оно могло выдержать чрезвычайно высокий уровень доверия, который мы возлагаем на него в высокодигитализованном обществе.

Ядро операционной системы (или, по крайней мере, его часть) станет таким безопасным ядром.

Ethereum станет другим.

Надеемся, что по крайней мере для всех вычислений, не требующих высокой производительности, ваше оборудование станет третьим.

Системы, связанные с Интернетом вещей, станут четвёртыми.

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

Но если вы добровольно готовы передать свои активы и данные программному обеспечению, написанному плохо и способному случайно поглотить их в чёрную дыру, — конечно, у вас есть на это полное право.