ヴィタリック：イーサリアムの次の段階の鍵は何ですか？

著者：Vitalik Buterin

翻訳：佳欢，ChainCatcher

特に Yoichi Hirai、Justin Drake、Nadim Kobeissi、Alex Hicks に感謝します。

過去数ヶ月間、イーサリアムの最前線の研究開発圈や計算分野の多くの他の場所で、新しいプログラミングパラダイムが急速に人気を集めています：非常に低レベルの言語（例えば EVM バイトコード、アセンブリ言語）や Lean を使ってコードを書くこと、そして自動的に検証可能な、Lean で書かれた数学的証明を使用してその正しさを検証することです。

適切に操作すれば、これは極めて効率的なコードを出力する可能性があるだけでなく、従来のプログラミング方法よりもはるかに安全です。Yoichi Hirai はこれを「ソフトウェア開発の究極の形態」と呼んでいます。

この記事では、その基本原理を明らかにし、ソフトウェアの形式的検証が何をできるのか、またイーサリアムや他の分野におけるその弱点と限界について探ります。

形式的検証とは？

形式的検証とは、自動的にチェックできる方法で数学的定理の証明を書くことを指します。比較的単純ですが興味深い例として、フィボナッチ数列に関する基本定理を見てみましょう：3番目ごとの数字は偶数であり、残りは奇数です。

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

これを証明する簡単な方法は数学的帰納法で、毎回3ステップ前進します。

まず基本ケースです。F1 = F2 = 1、F3 = 2 とします。観察すると、この命題（「Fi は 3 の倍数のとき偶数、そうでないときは奇数」）は x = 3 の前に成立しています。

次に帰納ケースです。この命題が 3k+3 の前に成立すると仮定します。すなわち、F3k+1、F3k+2、F3k+3 の奇偶性がそれぞれ奇数、奇数、偶数であることがわかっています。次の3つの数の奇偶性を計算できます：

F3k+4 = F3k+2 + F3k+3 = 奇数 + 偶数 = 奇数 F3k+5 = F3k+3 + F3k+4 = 偶数 + 奇数 = 奇数 F3k+6 = F3k+4 + F3k+5 = 奇数 + 奇数 = 偶数

したがって、3k+3 の前にこの命題が成立することを知っていると、3k+6 の前にも成立することを導き出せます。この推論を繰り返し適用することで、この規則がすべての整数に対して成立することを確信できます。

この論点は人間を納得させるには十分です。しかし、もしあなたが100倍複雑なものを証明したい場合、そして自分が間違っていないことを非常に確信したい場合はどうでしょう？そうです、コンピュータに信じられる証明を提供することができます。

以下はその具体的な表現方法です：

-- Fibonacci with fib 0 = 0, fib 1 = 1, fib 2 = 1 (indices offset by 1)
def fib : Nat → Nat
  | 0     => 0
  | 1     => 1
  | n + 2 => fib (n + 1) + fib n

-- Claim: fib (3k+1) is odd, fib (3k+2) is odd, fib (3k+3) is even.
-- Equivalently: every third Fibonacci number starting from fib 3 is even.
-- We prove all three at once by induction on k, since each case
-- of the next block is built from the previous block.
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 =>
    -- Rewrite the new indices into the form (something) + 2 so fib unfolds.
    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 で表現されています。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 の実装自体にもバグがあるかもしれません。しかし、これらの煩わしい詳細について議論する前に、まずは形式的検証を正しく理想的に完了することがもたらすユートピアについて深く探求しましょう。

安全のために生まれた形式的検証

コンピュータコードのバグは恐ろしいものです。

暗号通貨を不変のチェーン上のスマートコントラクトに入れたとき、北朝鮮がコードにバグが発生した場合に自動的にあなたのすべての資金を引き出すことができ、あなたが異議を唱えることができない場合、コードのバグはさらに恐ろしいものになります。

これがゼロ知識証明の中に包まれると、バグはさらに恐ろしいものになります。なぜなら、誰かがゼロ知識証明システムに侵入することができれば、彼らはすべてのお金を引き出すことができ、私たちは何が問題だったのか全くわからないからです（さらに悪いことに、いつ問題が発生したのかさえわからないのです）。

強力な AI モデルが登場し、例えば二年後の Claude Mythos がこれらのバグを自動的に発見できるようになると、コードのバグはさらに恐ろしいものになります。

この現実に対する反応の一部は、スマートコントラクトの基本的な理念を放棄することを主張することです。さらには、ネットワークの領域は防御者が攻撃者に対して非対称的な優位性を持つことができる領域ではないと考える人もいます。

いくつかの引用：

システムを強化するには、攻撃者が脆弱性を利用するために費やすよりも多くのトークンを使ってそれらの脆弱性を発見する必要があります。

そして：

私たちの業界は決定論的なコードに基づいています。それを書き、テストし、リリースし、動作することを確信しますが、私の経験では、この契約は崩れつつあります。

真の AI ネイティブ企業のトップオペレーターの中で、コードベースは「信じる」ものに変わり、その成功の確率を正確に説明することができなくなっています。

さらに悪いことに、一部の人々は唯一の解決策はオープンソースを放棄することだと考えています。

ネットワークセキュリティにとって、これは暗い未来です。特にインターネットの分散化と自由を気にかける私たちにとっては、非常に悲観的な展望です。

サイバー・パンク精神は根本的に、インターネット上で防御者が優位に立つという理念に基づいています。デジタル「城」（暗号、署名、証明のいずれか）を構築することは、破壊することよりもはるかに容易です。

もし私たちがこれを失ったら、インターネットの安全は規模の経済から、潜在的な攻撃者を世界中で追いかけることから、そしてより広い意味で、支配と破壊の間で二者択一をすることからしか得られなくなります。

私は同意しません。私はネットワークセキュリティの未来に対してより楽観的なビジョンを持っています。

強力な AI の脆弱性発見能力がもたらす挑戦は厳しいですが、それは過渡的な挑戦です。一度塵が落ち着けば、新しい均衡点に達し、私たちは過去よりも防御者に有利な環境を得ることができるでしょう。

Mozilla は私の見解に同意しています。彼らの言葉を引用します：

あなたは他のすべての事柄の優先順位を再調整し、このタスクに持続的かつ全神経を注ぐ必要があるかもしれませんが、トンネルの先には光があります。

私たちはこの挑戦にどのようにチームが取り組むかを非常に誇りに思っています。他の人々もできるでしょう。私たちの仕事はまだ終わっていませんが、私たちは困難を乗り越え、単に追いつくだけでなく、はるかに良い未来を垣間見ることができています。

防御者はついに決定的に勝利する機会を得ました。... 欠陥は限られており、私たちはついにそれらをすべて見つけ出すことができる世界に入っています。

今、もしあなたが Mozilla の投稿で「形式化」と「検証」という二つの言葉を Ctrl+F で検索すると、マッチするものはゼロです。ネットワークセキュリティの明るい未来は、形式的検証や他の単一の技術に完全に依存しているわけではありません。

それは何に依存しているのでしょうか？基本的にはこのグラフです：

CVE 脆弱性の数の時間的な減少傾向

数十年にわたり、多くの技術が脆弱性の数の減少に寄与してきました：

• 型システム
• メモリ安全な言語
• ソフトウェアアーキテクチャの改善（サンドボックス化、権限管理、そして「信頼できる計算基盤」と「他のコード」を明確に区別することを含む）
• より良いテスト方法
• セキュリティと非セキュリティのコーディングパターンに関する知識体系の豊富さ
• 事前に書かれ、監査されたソフトウェアライブラリの増加

AI 支援下の形式的検証は、新しいパラダイムとして見なされるべきではなく、すでに進行中のトレンドとパラダイムの強力な加速器として見なされるべきです。

形式的検証は万能ではありません。しかし、実現よりも目標がはるかに簡単な状況に特に適しています。これは、イーサリアムの次の主要なイテレーションで展開する必要があるいくつかの極めて複雑な厄介な技術において特に真実です：量子耐性署名、STARKs、コンセンサスアルゴリズム、そして ZK-EVMs。

STARK は非常に複雑なソフトウェアです。しかし、それが実現する核心的な安全属性は理解しやすく、形式化することができます：もしプログラム P のハッシュ H、入力 x、出力 y の証明を見た場合、次のいずれかが成り立ちます：(i) STARK で使用されるハッシュアルゴリズムが破られた、または (ii) P(x) = y です。

したがって、私たちは Arklib プロジェクトを持ち、これは完全に形式的に検証された STARK 実装を作成しようとしています（VCV-io を参照してください。これは、さまざまな他の暗号プロトコルの形式的検証に使用できる基盤のオラクル計算インフラを提供します。その多くは STARK の依存関係です）。

さらに野心的なのは evm-asm：完全に形式的に検証された全 EVM 実装を構築するプロジェクトです。

ここでの安全属性はそれほど単純明快ではありません：基本的には、Lean で書かれた別の EVM 実装と等価であることを証明することが目標ですが、その実装は直感性と可読性を最大化するために書かれ、具体的な実行効率を考慮する必要はありません。

私たちは、十の EVM 実装を得る可能性があります。それらは証明可能に互いに等価であり、偶然にも同じ致命的な欠陥を含んでいて、攻撃者が権限のないアドレスからすべての ETH を引き出すことができるかもしれません。

しかし、これは現在のどの EVM 実装にもこのような欠陥が存在する可能性よりもはるかに小さいです。そして、私たちが痛い教訓を経てその重要性を理解したもう一つの安全属性、すなわち DoS 攻撃に対する耐性は、簡単に規範化できます。

他の二つの重要な分野は：

• バイザンチン耐障害コンセンサス。ここでは、期待されるすべての安全属性を形式化することが同様に困難ですが、バグが非常に一般的であったことを考えると、試みる価値があります。したがって、私たちは Lean で進行中のコンセンサスプロトコルの Lean 実装と証明を持っています。
• スマートコントラクトプログラミング言語：Vyper と Verity における形式的検証を参照してください。

これらのすべての状況において、形式的検証がもたらす巨大な付加価値の一つは、これらの証明が本当にエンドツーエンドであることです。通常、最も厄介なバグは相互作用バグであり、これは独立して考慮された二つのサブシステムの境界に潜んでいます。

人間にとって、システム全体をエンドツーエンドで推論することは非常に困難です。しかし、自動化されたルールチェックシステムはそれを実現できます。

効率のために生まれた形式的検証

evm-asm を再度見てみましょう。これは EVM 実装ですが、直接 RISC-V アセンブリで書かれた EVM 実装です。

本物です。

これは ADD オペコードです：

import EvmAsm.Rv64.Program
namespace EvmAsm.Evm64
open EvmAsm.Rv64

/-- 256-bit EVM ADD: binary, pops 2, pushes 1.
    Limb 0: LD, LD, ADD, SLTU (carry), SD (5 instructions).
    Limbs 1-3: LD, LD, ADD, SLTU (carry1), ADD (carryIn), SLTU (carry2), OR (carryOut), SD (8 each).
    Then ADDI sp, sp, 32.
    Registers: x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1. -/
def evm_add : Program :=
  -- Limb 0 (5 instructions)
  LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;
  
  -- Limb 1 (8 instructions)
  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 ;;
  
  -- Limb 2 (8 instructions)
  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 ;;
  
  -- Limb 3 (8 instructions)
  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 adjustment
  ADDI .x12 .x12 32
end EvmAsm.Evm64

RISC-V を選んだ理由は、構築中の ZK-EVM 証明器が通常 RISC-V を証明し、イーサリアムクライアントを RISC-V にコンパイルすることで機能するからです。したがって、直接 RISC-V で書かれた EVM 実装があれば、これが最も速い実装になるはずです。

RISC-V は通常のコンピュータ内でも非常に効率的にシミュレーションできます（市場には RISC-V ノートパソコンもあります）。

もちろん、エンドツーエンドを実現するためには RISC-V の実装（または証明器の算術化）自体を形式的に検証する必要がありますが、心配しないでください。この分野の作業もすでに存在しています。

アセンブリでコードを書くことは、50年前に私たちがよくやっていたことです。それ以来、私たちはこの方法を放棄し、高級言語でコードを書くようになりました。

高級言語は効率に妥協しますが、その代わりに、コードを書く速度がはるかに速く、他の人のコードを理解する速度もはるかに速くなります。これは安全性にとって不可欠です。

形式的検証と人工知能の組み合わせにより、私たちは「未来に戻る」機会を得ました。

具体的には、人工知能にアセンブリコードを書かせ、そのアセンブリコードが必要な属性を持つことを検証する形式的証明を書くことができます。

少なくとも、必要な属性は、可読性を高めるために最適化され、何らかの人間に優しい高級言語で書かれた実装と完全に等価であることができます。

私たちはもはや単一のコードオブジェクトが可読性と効率の間でバランスを取る必要はなく、二つの独立したオブジェクトを持っています：一つ（アセンブリ実装）は効率を最適化し、その実行の特定の環境のニーズを考慮します；もう一つ（安全声明または高級言語実装）は可読性を最適化し、そして私たちは数学的証明を通じて両者の間の等価性を証明します。

ユーザーは（自動的に）その証明を一度検証でき、その時点からは迅速なバージョンを実行するだけで済みます。

この方法は非常に強力であり、Yoichi Hirai が「ソフトウェア開発の究極の形態」と呼ぶのも納得です。

形式的検証は万能薬ではない

暗号学と計算機科学の分野には、形式的手法の歴史とほぼ同じくらい古い伝統があります。それは、形式的手法（またはより広く「証明」に対する依存）を批判する伝統です。

これらの文献には実際のケースが満載です。初期の単純な暗号学の時代に手書きされた証明から始めましょう。ここでは、Menezes と Koblitz の2004年の批判を引用します：

1979年、Rabinはある暗号関数を提案しました。この関数はある意味で「証明可能」な安全性を持つものであり、すなわちそれには還元主義的な安全属性があります。

還元主義的な安全声明は、暗号文 y からメッセージ m を見つけることができる人は、n を分解することもできなければならないというものです。... Rabin がその暗号スキームを提案した後すぐに、Rivest は皮肉なことに、その追加の安全性を与える特性が「選択暗号文」と呼ばれる攻撃者に直面した場合に全てが崩壊することを指摘しました。

つまり、攻撃者が何らかの方法で Alice を騙して彼女が選んだ暗号文を解読させることができれば、攻撃者は Sam が前の段落で n を分解するために使ったのと同じ手順を踏むことができるのです。

Menezes と Koblitz はさらに多くの例を挙げています。一般的な傾向は、暗号プロトコルをより「証明可能」にするための設計が、しばしばそれらをより「自然」でなくし、設計者が考慮していない状況で崩壊する可能性を高めるということです。

さて、機械検証可能な証明とコードに戻りましょう。これは2011年に形式的に検証されたCコンパイラにバグが存在することを発見した論文です：

私たちが発見した第二の CompCert の問題は、次のコードを生成する二つのバグに現れます： stwu r1, -44432(r1) ここでは大きな PowerPC スタックフレームが割り当てられています。

問題は、16ビットのシフトフィールドがオーバーフローしたことです。CompCert の PPC セマンティクスはこの即値の幅に制限を規定しておらず、アセンブラが範囲外の値を捕捉することを仮定しています。

もう一つの2022年の論文：

CompCert-KVX では、e2618b31 が修正されたバグがありました：「nand」命令が「and」として印刷されます。「nand」は非常にまれな ~(a & b) モードでのみ使用されます。このバグはランダムに生成されたプログラムをコンパイルすることで発見されました。

そして今日、2026年には、Nadim Kobeissi が Cryspen における形式的に検証されたソフトウェアのバグを次のように説明しています：

2025年11月、Filippo Valsorda が独立して libcrux-ml-dsa v0.0.3 が同じ決定論的入力を与えた場合に異なるプラットフォームで異なる公開鍵と署名を生成することを報告しました。

このバグは _vxarq_u64 内部ラッパー関数に存在し、この関数は SHA-3 の Keccak-f 置換で使用される XAR 操作を実装しています。バックアップメカニズムはシフト操作に不正なパラメータを渡し、ハードウェア SHA-3 サポートのない ARM64 プラットフォームで SHA-3 ハッシュを破損させました。

これはタイプ I 障害に該当します：この内部関数はマークされていましたが、全体の NEON バックエンドは実行時の安全性や正しさの証明を完了していませんでした。

さらに：

libcrux-psq ライブラリは、後量子の事前共有鍵プロトコルを実装しています。decrypt_out メソッドでは、AES-GCM 128 の復号パスが復号結果に .unwrap() を呼び出し、エラーを伝播させません。形式的に不正な暗号文がプロセスをクラッシュさせることができます。

上記の四つの問題は、以下の二つのタイプのいずれかに該当します：

• 一部のコードのみが検証された場合（残りの部分を検証するのが難しすぎるため）、結果として未検証のコードが著者が想像していたよりも多くの脆弱性を持っていることが判明した（かつその方法がより致命的である）。
• 著者が証明すべき重要な属性を規定することを忘れた場合。

Nadim の記事には形式的検証の失敗パターンの分類が含まれています。彼は他の失敗パターンのタイプも挙げています（例えば、もう一つの主要なケースは「形式的規範自体が間違っているか、証明に構築システムが静かに受け入れる虚偽の声明が含まれている」ということです）。

最後に、ソフトウェアとハードウェアの境界における形式的検証の失敗を見てみましょう。ここでの一般的な問題の一つは、サイドチャネル攻撃に対する耐性を検証することです。

たとえあなたがメッセージを保護するために完璧に安全な暗号形式を持っていたとしても、数メートル離れた人が電気信号の変動をキャッチし、数十万回の暗号化の後にあなたの秘密鍵を抽出できるなら、あなたは安全ではありません。

これは「差分電力解析」に関する記事であり、これは現在十分に理解されているこの種の技術の例です。

差分電力解析はサイドチャネル攻撃の一般的なタイプの一つです。出典：ウィキペディア

常にこのような攻撃者に対抗するための安全性を証明しようとする試みがありました。しかし、そのような証明は、特定の攻撃者の数学モデルを必要とし、そのモデルに対して安全性を証明することができます。

時には「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)

ここでは、あなたの意図を三つの異なる方法で表現しています：

• 明示的に、フィボナッチ公式をコードに実装することによって
• 暗黙的に、型システムを通じて（入力、出力、再帰の中間ステップがすべて整数であることを指定する）
• 「サンプルパッケージ」メソッドを通じて：テストケース

ファイルを実行すると、公式がサンプルと照合されます。型チェッカーは型が互換性があるかどうかを検証できます：二つの整数を加算することは合規な操作であり、別の整数を生成します。

型システムは物理学の宿題をチェックするのに良い方法であることが多いです：もしあなたが加速度を計算していて、単位がメートル/秒ではなくメートル/秒²の答えを得た場合、あなたは間違っていることがわかります。

そしてテストケースは「サンプルパッケージ」で定義された一つのインスタンスです。人間にとって、概念を扱う際にこの方法はしばしば直接的な明示的な定義よりも自然です。

あなたの意図を規範化するために異なる方法を多く持つほど、理想的には問題を解決するために異なる思考方法を要求する全く異なる方法で、すべてのこれらの表現形式が互いに互換性があることが証明されれば、あなたが本当に望んでいるものを実際に表現できる可能性が高くなります。

安全なプログラミングは、あなたの意図を異なる方法で表現し、それらの表現がすべて互いに互換性があるかどうかを自動的に検証することです。

形式的検証はこのアプローチをさらに拡張することを可能にします。形式的検証を通じて、あなたはほぼ無限の異なる冗長な方法であなたの意図を規範化し、プログラムはそれらがすべて互換性がある場合にのみ検証を通過できます。

高度に最適化された実装と、効率は非常に低いが人間にとって読みやすい実装を規範化し、それらが一致するかどうかを検証できます。あなたは十人の友人に、あなたのプログラムが持つべき数学的属性のリストを提供してもらい、それがすべて通過するかどうかを確認できます。

もし通過しなければ、プログラムが間違っているのか、数学的属性が間違っているのかを見つけ出します。そして、あなたは人工知能を使ってこれらすべての操作を非常に効率的に行うことができます。

それでは、どのように始めればよいのでしょうか？

現実的に言えば、あなたは自分で証明を書くことはありません。形式的手法が流行しなかった理由は、大多数の人々がこれらの難解な内容を書く方法を理解できなかったからです。以下のコードの意味を教えてもらえますか？

  /-- Helper: pointwise ≤ at the foldl level with an accumulator. -/
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 を記述するために特別に微調整された小さなオープンソースの重みモデルであり、有望な代替手段です。

それは 119B のパラメータを持ち、各トークンが 6B を活性化します。あなたはそれをローカルで実行できますが、速度は遅く（私のノートパソコンでは約 15 tok/sec の速度です）。ベンチマークによると、Leanstral ははるかに大きな汎用モデルよりも優れています：

私の現在の個人的な経験によれば、Deepseek 4 Pro よりはやや劣りますが、それでも非常に効果的です。

形式的検証は私たちのすべての問題を解決することはできません。

しかし、もし私たちがインターネットの安全モデルを、誰もが少数の強力な組織を信頼することに依存しないものにしたいのであれば、コードを信頼する必要があります。これは、強力な人工知能の対抗者に直面してもコードを信頼できることを含みます。

AI 支援下の形式的検証は、私たちがこの目標を達成するための道を着実に進める一歩を踏み出させます。

ブロックチェーンや ZK-SNARKs と同様に、人工知能と形式的検証も非常に補完的な技術です。

ブロックチェーンはプライバシーとスケーラビリティの代償を払って、あなたにオープンな検証性と検閲耐性を与え、ZK-SNARKs は再びプライバシーとスケーラビリティをあなたに返します（実際には以前よりも多く）。

人工知能は正確性の代償を払って、あなたに大量のコードを書く能力を与え、形式的検証は再び正確性をあなたに返します（実際には以前よりも高い）。

デフォルトでは、人工知能は大量の非常に粗雑なコードを生み出し、バグの数は増加します。

実際、バグの増加を許容することが正しいトレードオフである場合もあります：もしバグが軽微であれば、バグが存在するソフトウェアであっても、そのソフトウェアがないよりはましです。

しかし、ここでネットワークセキュリティには楽観的な未来があります：ソフトウェアは（引き続き）「安全なコア」を中心に「不安全な周辺部分」に分裂します。

不安全な周辺部分はサンドボックス内で実行され、作業を完了するために必要な最小限の権限しか与えられません。

安全なコアはすべてを管理します。安全なコアが崩壊すれば、すべてが崩壊します。あなたの個人データ、あなたのお金などが含まれます。しかし、もし不安全な周辺部分が崩壊しても、安全なコアはあなたを守ることができます。

安全なコアに関しては、バグのあるコードが氾濫することを許してはいけません。私たちは安全なコアの規模を小さく保つために過激な行動を取ります。さらにそれを縮小します。

その代わりに、私たちは人工知能がもたらすすべての追加の性能を、安全なコアをより安全にするタスクに完全に投入し、私たちが高度にデジタル化された社会の中でそれに与える極めて高い信頼の重任を耐えられるようにします。

オペレーティングシステムのカーネル（または少なくともその一部）は、そのような安全なコアになります。

イーサリアムもまた別のものになります。

少なくとも、すべての非性能集中的な計算において、あなたが使用するハードウェアは第三のものになるでしょう。

IoT に関連するシステムは第四のものになります。

少なくともこれらの安全なコアの中では、「バグは避けられない。あなたはただ攻撃者よりも早くそれらを見つける努力をするしかない」という古い格言は反証され、真に安全を得られる希望に満ちた世界に取って代わられるでしょう。

しかし、もしあなたが自分の資産やデータを、拙劣なコードを記述し、それが偶然にもそれらをブラックホールに飲み込む可能性があるソフトウェアに委ねることを甘んじて受け入れるのであれば、もちろんあなたにはその自由もあります。