Виталик: В чём ключ к следующему этапу развития 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 …

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

Первый случай — базовый. Пусть F1 = F2 = 1, F3 = 2. По наблюдениям, утверждение ("Fi — четное число, когда i кратно 3, иначе — нечетное") верно до x = 3.

Далее рассмотрим индуктивный случай. Предположим, что утверждение верно до 3k+3, то есть нам уже известно, что четность чисел F3k+1, F3k+2 и F3k+3 нечетная, нечетная и четная соответственно. Мы можем вычислить четность следующей группы из трех чисел:

F3k+4 = F3k+2 + F3k+3 = нечетное + четное = нечетное

F3k+5 = F3k+3 + F3k+4 = четное + нечетное = нечетное

F3k+6 = F3k+4 + F3k+5 = нечетное + нечетное = четное

Таким образом, зная, что утверждение верно до 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

— Утверждение: функция Фибоначчи (3k+1) — нечётная, функция Фибоначчи (3k+2) — нечётная, функция Фибоначчи (3k+3) — чётная.

— Аналогично: каждое третье число Фибоначчи, начиная с Фибоначчи 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

индукция k с

| ноль => решить

| succ k ih =>

— Перепишите новые индексы в виде (что-то) + 2, чтобы развернулось уравнение Фибоначчи.

уточнить ⟨?_, ?_, ?_⟩

· show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1

омега

· show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1

омега

· show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)

+ (фиб (3 * k + 3) + фиб (3 * k + 2))) % 2 = 0

омега

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

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

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

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

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

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

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

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

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

Но если отбросить любопытство, то что с того?

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

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

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

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

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

теорема пассивной_секретности_le_ddh

(гарантированная победа)

(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:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Несколько цитат:

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

И:

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

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

Хуже того, некоторые считают, что единственное решение — отказаться от открытого исходного кода.

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

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

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

Я не согласен; у меня более оптимистичный взгляд на будущее кибербезопасности.

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

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

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

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

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

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

От чего это зависит? По сути, от этой диаграммы:

Динамика уязвимостей 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, написанной с использованием принципов бережливого производства, хотя эта реализация может быть написана таким образом, чтобы максимально повысить интуитивность и читаемость без учета конкретной эффективности во время выполнения.

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

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

Две другие важные области:

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

Языки программирования смарт-контрактов: см. формальную верификацию в Vyper и Verity.

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

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

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

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

Подлинный.

Вот код операции ADD:

импорт EvmAsm.Rv64.Program

пространство имен EvmAsm.Evm64

открыть 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 ;;

ИЛИ' .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 ;;

ИЛИ' .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 ;;

ИЛИ' .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 генерирует разные открытые ключи и подписи на разных платформах при одинаковых детерминированных входных данных.

Ошибка существовала во внутренней функции обертывания vxarqu64, которая реализовывала операцию XAR, используемую в перестановке SHA-3 с помощью Keccak-f. Механизм резервного копирования передавал некорректные параметры операции сдвига, что приводило к повреждению дайджеста SHA-3 на платформах ARM64 без аппаратной поддержки SHA-3.

Это относится к типу I ошибки: внутренняя функция была помечена, но весь бэкэнд NEON не завершил проверку безопасности или корректности во время выполнения.

И:

Библиотека libcrux-psq реализует постквантовый протокол с предварительно разделенным ключом. В методе decrypt_out путь расшифровки AES-GCM 128 вызывает метод .unwrap() для результата расшифровки вместо распространения ошибок. Некорректно сформированный зашифрованный текст может привести к сбою процесса.

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

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

Случаи, когда авторы забыли указать ключевые свойства, которые необходимо было доказать.

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

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

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

Это статья о «дифференциальном анализе мощности», хорошо известном примере подобных методов: статья.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Рассмотрим в качестве примера следующий код на Python:

def fib(n: int) -> int:

если n < 0:

вызвать исключение("Отрицательные значения не поддерживаются")

elif 0 <= n < 2:

вернуть n

еще:

return fib(n-1) + fib(n-2)

если __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) (ab : 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

сопоставить ds1, ds2, hLE с

| [], [], .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

точный Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

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

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

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

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

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

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

В случае с вариантом подписи SPHINCS, заключительное утверждение выглядит следующим образом:

теорема 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 станет еще одним таким проектом.

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

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

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

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