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

著者：ヴィタリック・ブテリン

翻訳者：Jiahua、ChainCatcher

フィードバックとレビューをいただいた平井洋一氏、ジャスティン・ドレイク氏、ナディム・コベイシ氏、アレックス・ヒックス氏に心より感謝申し上げます。

ここ数ヶ月、イーサリアムの開発サークルやコンピューティング分野の他の多くの領域で、新しいプログラミングパラダイムが急速に支持を集めている。それは、EVMバイトコードやアセンブリ言語などの非常に低レベルな言語、あるいはLeanで直接コードを記述し、Leanで記述された自動的に検証可能な数学的証明を用いてその正当性を検証するというものだ。

正しく行えば、これは非常に効率的なコードを生み出す可能性を秘めているだけでなく、従来のプログラミング手法よりもはるかに安全です。平井洋一氏はこれを「究極のソフトウェア開発形態」と呼んでいます。

本稿では、ソフトウェアの形式検証の根底にある原理を明らかにし、形式検証が達成できることを探り、イーサリアムやその他の分野におけるその弱点と限界を特定することを試みる。

形式検証とは何ですか？

形式検証とは、数学の定理の証明を自動的に検証できる形で記述するプロセスを指します。比較的単純でありながら興味深い例として、フィボナッチ数列に関する基本的な定理、すなわち、3つおきの数は偶数であり、それ以外は奇数であるという定理を考えてみましょう。

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

これを証明する簡単な方法の一つは、数学的帰納法を用いて、一度に３段階ずつ進めていくことである。

まず基本ケースです。F1 = F2 = 1、F3 = 2 とします。観察すると、(「i が 3 の倍数の場合、Fi は偶数であり、それ以外の場合は奇数である」) という記述が 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より前に真であることが導き出されます。この推論を繰り返し適用することで、この規則がすべての整数に対して成り立つことを確認できます。

この議論は人間を納得させるには十分です。しかし、もしあなたがもっと複雑なことを証明したい場合、そして自分が絶対に間違いを犯していないことを確信したい場合はどうでしょうか？そんな時は、コンピュータが納得できるような証明を提供すればよいのです。

以下のように表示されます。

-- フィボナッチ数列（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) は偶数です。

言い換えれば、フィボナッチ数列の3番目から始まる3番目の数は偶数である。

-- 我々は、k に関する帰納法によって、3 すべてを一度に証明します。各ケースは、

次のブロックは前のブロックから構築されます。

定理 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)

+ (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0

オメガ

これは同じ推論ロジックをLean言語で表現したものです。Leanは、数学的証明の記述と検証によく用いられるプログラミング言語です。

これは、上記で示した「人間」の証明とは明らかに異なっているが、それには正当な理由がある。コンピュータ（従来の意味での「コンピュータ」、つまり大規模な言語モデルではなく、if/then文で構成された「決定論的」プログラム）にとって直感的なものは、人間にとって直感的なものとは根本的に異なるからである。

上記の証明では、fib(3k+4) = fib(3k+3) + fib(3k+2) という事実を強調せず、fib(3k+3) + fib(3k+2) が奇数であることを強調しましたが、リーンにおけるオメガと呼ばれる戦略は、これを自動的に fib(3k+4) の定義に関する知識と組み合わせます。

より複雑な証明では、現在のステップを実行することを可能にする数学法則を明示的に述べる必要がある場合があり、Prod.mk.inj のような分かりにくい名前を使用する必要がある場合もあります。

一方、巨大な多項式をたった1ステップで展開し、「オメガ」や「リング」のようなたった1行の式でその妥当性を証明することも可能です。

この直感に反する煩雑な性質こそが、機械検証可能な証明が60年近く前から存在しているにもかかわらず、この分野がニッチな領域にとどまっている大きな理由である。しかし一方で、人工知能の急速な発展により、これまで不可能だった多くのことが急速に可能になりつつある。

数学的証明がコードの保護を始めるとき

ここまで読んで、あなたはこう考えているかもしれません。「コンピュータは数学の定理の証明を検証できるのだから、素数に関する突飛な新しい結論のうち、どれが真実で、どれが何百ページにも及ぶPDF論文の単なる誤りなのかを、ついに判断できるはずだ。」

もしかしたら、望月真一氏のABC予想に関する見解が正しいかどうかさえ解明できるかもしれない！

しかし、好奇心はさておき、それがどうしたというのか？

考えられる答えはたくさんありますが、私にとって非常に重要な答えの一つは、コンピュータプログラム、特に暗号化やセキュリティ関連のタスクを実行するプログラムの正確性を検証することです。

結局のところ、コンピュータプログラムは数学的な対象物であるため、コンピュータプログラムが特定の方法で実行されることを証明すること自体が数学的な定理となる。

例えば、Signalのような暗号化通信ソフトウェアが本当に安全かどうかを証明したいとしましょう。この場合、「安全」とはどういう意味かを数学的に書き出すことができます。

大まかに言えば、特定の暗号化の前提条件が満たされると仮定すれば、秘密鍵を所有する者だけがメッセージの内容に関する情報を知ることができる、ということをあなたは証明しているのです。実際には、重要なセキュリティ特性は数多く存在します。

実は、まさにこの問題の解明に取り組んでいるチームが存在するのです！彼らのセキュリティ定理の一つは次のようになっています。

定理 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によるその意味の要約は以下のとおりです。

passivesecrecycle_ddh定理は、X3DHの受動的なメッセージ機密性が、ランダムオラクルモデルにおけるDDH仮定と同等以上の難しさであることを示す簡潔な還元定理である。攻撃者がX3DHの受動的なメッセージ機密性を破ることができれば、DDHも破ることができる。

DDHは解読が困難であると仮定すると、X3DHも受動的な攻撃に対して安全である。この定理は、攻撃者がSignalの鍵交換メッセージを受動的に傍受できたとしても、Signalが生成するセッション鍵とランダムな鍵を区別できる確率はごくわずかであることを証明する。

これをAES暗号化実装の正しい証明と組み合わせると、Signalプロトコルの暗号化が受動的な攻撃者に対して安全であるという証明が得られます。

同様のプロジェクトによって、TLSやブラウザ内部の暗号化技術のその他の実装が安全であることが証明されている。

エンドツーエンドの完全な形式検証を実施すれば、プロトコルの理論的な記述が安全であるだけでなく、ユーザーが実際に実行する具体的なコードも安全であることを証明できる。

ユーザーの視点から見ると、これは信頼性を大幅に向上させる。コードを完全に信頼するために、コードベース全体をチェックする必要はなく、証明済みの記述だけをチェックすればよい。

ここで、特に「安全」という極めて重要な言葉が実際に何を意味するのかに関して、いくつか重要な注意点を念頭に置いておく必要があります。

本当に重要な命題を証明することを忘れがちです。証明すべき命題は、コードそのものを説明するよりも簡単ではない場合があることに気づくことも少なくありません。

証明の過程で、最終的に成り立たない仮定を意図せず持ち込んでしまうことはよくある。また、システムの特定の部分だけを形式的に証明すればよいと判断した途端、他の部分（ハードウェアを含む）に深刻な脆弱性が露呈してしまうこともよくある。

リーン実装自体にもバグが存在する可能性がある。しかし、こうした厄介な詳細について議論する前に、まずは形式検証を正しく理想的に完了することで実現しうるユートピアについて掘り下げてみよう。

セキュリティのために生まれた形式検証

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

暗号通貨を不変のチェーン型スマートコントラクトに組み込んだ場合、コードにバグが発生した際に北朝鮮が自動的にすべての資金を抜き取ることができ、しかもあなたには何の対処手段もないとなると、コードのバグはさらに恐ろしいものとなる。

これらすべてがゼロ知識証明に包まれている場合、バグはさらに恐ろしいものになります。なぜなら、誰かがゼロ知識証明システムに侵入することに成功すれば、すべてのお金を抜き取ることができ、何が問題だったのか（さらに悪いことに、いつ問題が起きたのかさえ）全く分からないからです。

今から2年後には、クロード・ミトスのような強力なAIモデルが登場し、こうしたバグを自動的に発見できるようになるだろう。そうなれば、コードのバグはさらに恐ろしいものになる。

こうした現実に対する反応として、スマートコントラクトの根本的な考え方を放棄すべきだと主張する人もおり、インターネットは防御側が攻撃側に対して非対称的な優位性を持つことができる領域にはなり得ないと考えている。

いくつかの引用：

システムを強化するには、攻撃者が脆弱性を悪用するために使用するトークンよりも多くのトークンを消費する必要があります。

そして：

私たちの業界は決定論的なコードに基づいて成り立っています。コードを書いて、テストして、デプロイして、確実に動作するという確信を持つ。しかし、私の経験では、この前提が崩れつつあります。

真にAIネイティブな企業のトップレベルの運営者の間では、コードベースは「信頼できる」実行手段となっており、その成功確率を正確に指定することはもはや不可能になっている。

さらに悪いことに、オープンソースを放棄することこそが唯一の解決策だと考える人もいる。

サイバーセキュリティにとって、これは暗い未来と言えるでしょう。特に、インターネットの分散化と自由を重視する私たちにとって、これは極めて悲観的な見通しです。

サイファーパンクの精神全体は、インターネット上では防御側が有利であり、デジタル上の「城」（暗号化、署名、証明など）を築くことは、それを破壊するよりもはるかに容易であるという考えに基づいている。

もし私たちがこれを失えば、インターネットのセキュリティは規模の経済、世界中の潜在的な攻撃者を追跡することによってのみ実現可能となり、より広義には、支配か破壊かの二者択一しか選択肢がなくなるだろう。

私はそうは思いません。サイバーセキュリティの未来については、もっと楽観的な見方をしています。

強力なAIによる脆弱性発見能力がもたらす課題は深刻ですが、これは過渡的な課題だと考えています。混乱が収まり、新たな均衡状態が確立されれば、防御側にとってこれまで以上に有利な環境が実現するでしょう。

Mozillaも私の見解に同意しています。彼らの言葉を引用すると次のようになります。

他のすべてのことの優先順位を見直し、この課題に持続的かつ集中的なエネルギーを注ぐ必要があるかもしれませんが、トンネルの先には光が見えています。

私たちのチームがこの困難に立ち向かっていることを大変誇りに思いますし、他の人たちもきっと同じように感じるでしょう。私たちの仕事はまだ終わっていませんが、嵐を乗り越え、現状維持どころか、はるかに優れた未来を垣間見ることができます。

守備側はついに決定的な勝利を収める機会を得た。…欠陥は限られており、我々はついにそれらすべてを見つけ出すことができる世界に突入しようとしている。

さて、Mozillaの投稿でCtrl+Fを使って「formal」と「verification」という単語を検索しても、一致する結果はゼロです。サイバーセキュリティの明るい未来は、形式検証やその他の単一の技術だけに完全に依存しているわけではありません。

何に依存するのか？基本的には、この表に表れる。

CVE脆弱性の経時的な推移

数十年にわたり、多くの技術が脆弱性の数の減少に貢献してきた。

タイプシステム

メモリ安全言語

ソフトウェアアーキテクチャの改善（サンドボックス化、権限制御、そしてより広範には「信頼できるコンピューティング基盤」と「その他のコード」の区別を含む）

より良いテスト方法

安全なコーディングパターンと安全でないコーディングパターンに関する知識ベースは、常に拡大し続けている。

事前に作成され、監査済みのソフトウェアライブラリが増加している

AIを活用した形式検証は、全く新しいパラダイムとして捉えるべきではなく、むしろ既に進展しているトレンドやパラダイムを強力に加速させるものとして捉えるべきである。

形式検証は万能薬ではありません。しかし、目標が実装よりもはるかに単純な状況には特に適しています。これは、イーサリアムの次期メジャーバージョンで導入する必要のある、非常に複雑で扱いにくい技術、例えば量子耐性署名、STARK、コンセンサスアルゴリズム、ZK-EVMなどに特に当てはまります。

STARKは非常に複雑なソフトウェアです。しかし、STARKが実装するコアセキュリティ特性は理解しやすく、形式化も容易です。ハッシュHがプログラムP、入力x、出力yを指している場合、(i) STARKで使用されているハッシュアルゴリズムが破られているか、(ii) P(x) = yのいずれかです。

そこで、完全な形式検証済みのSTARK実装を作成しようとしているArklibプロジェクトが登場しました（VCV-ioを参照してください。VCV-ioは、STARKに依存する多くの他の暗号プロトコルの形式検証のための基礎的なオラクルコンピューティングインフラストラクチャを提供します）。

さらに野心的なプロジェクトとして、evm-asmがあります。これは、完全に形式的に検証されたEVM実装全体を構築することを目指すプロジェクトです。

ここでのセキュリティ特性はそれほど単純ではありません。基本的に、目標は、Leanで書かれた別のEVM実装との同等性を証明することですが、その実装は、特定の実行時効率を考慮せずに、直感性と可読性を最大限に高めるように記述することができます。

10種類のEVM実装が登場する可能性があり、それらはすべて同等であることが証明されているにもかかわらず、攻撃者がアクセス権限のないアドレスからすべてのETHを抜き取ることができるという致命的な欠陥を全て含んでいる可能性がある。

しかし、これは現在のEVM実装にそのような欠陥が存在する可能性よりもはるかに低い。また、痛ましい経験を経て初めてその重要性に気づいたもう一つのセキュリティ特性、すなわちDoS攻撃への耐性も、形式化するのは容易である。

その他重要な分野は以下の2つです。

ビザンチン耐障害性コンセンサス。ここでも、期待されるすべてのセキュリティ特性を形式化することは同様に困難ですが、バグの発生頻度を考えると、試みる価値はあります。そのため、Lean を用いたコンセンサスプロトコルの実装と証明を継続的に行っています。

スマートコントラクトのプログラミング言語：VyperおよびVerityにおける形式検証を参照してください。

これらすべてのケースにおいて、形式検証によってもたらされる大きな付加価値の一つは、これらの証明が真にエンドツーエンドであるということです。一般的に、最も厄介なバグは、独立して考えられる2つのサブシステムのインターフェースに潜む相互作用バグです。

人間にとって、システム全体を最初から最後まで推論することは非常に困難です。しかし、自動化されたルールチェックシステムであればそれが可能です。

形式検証は効率性を追求して生まれた

evm-asmをもう一度見てみましょう。これはEVMの実装ですが、RISC-Vアセンブリ言語で直接記述されたEVMの実装です。

本物。

ADD命令のオペコードは以下のとおりです。

import 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（carry1）、ADD（carryIn）、SLTU（carry2）、OR（carryOut）、SD（各8）。

次に、ADDI sp、sp、32。

レジスタ: x12=sp、x7=acc、x6=オペランド、x5=キャリー、x11=キャリー1。-/

def evm_add : プログラム :=

-- 肢体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

EvmAsm.Evm64 の終了

RISC-Vが選ばれた理由は、構築中のZK-EVMプローバーが通常、RISC-Vの検証とイーサリアムクライアントのRISC-Vへのコンパイルによって動作するためです。したがって、RISC-Vで直接記述されたEVM実装があれば、これが最速の実装となるはずです。

RISC-Vは、一般的なコンピュータ上でも非常に効率的にシミュレートできます（そして、RISC-V搭載のノートパソコンも市販されています）。

もちろん、真のエンドツーエンドを実現するには、RISC-V自体の実装（または証明器の算術演算）を形式的に検証する必要がありますが、心配はいりません。この分野の研究は既に存在しています。

アセンブリ言語で直接コードを記述することは、50年前にはよく行われていた手法です。しかし、それ以降、私たちはこの手法を捨て、より高水準の言語でコードを記述するようになりました。

高水準言語は効率性において妥協を強いられるが、その代わりに、はるかに高速なコーディングを可能にし、さらに重要なことに、他者のコードをはるかに高速に理解することを可能にする。これはセキュリティにとって不可欠である。

形式検証と人工知能を組み合わせることで、「未来へ戻る」機会が得られる。

具体的には、AIにアセンブリコードを書かせ、その後、そのアセンブリコードが望ましい特性を備えていることを検証する形式的な証明を書かせることができる。

最低限必要な特性としては、可読性を最適化し、人間にとって分かりやすい高水準言語で記述された実装と完全に同等であることが挙げられる。

可読性と効率性のバランスを取るために単一のコードオブジェクトはもはや必要ありません。代わりに、2つの独立したオブジェクトを用意します。1つは（アセンブリ実装）特定の実行環境の要求を考慮しつつ、効率性のみを最適化したもので、もう1つは（セキュリティステートメントまたは高水準言語実装）可読性のみを最適化したものです。そして、数学的な証明によって両者の等価性を証明します。

ユーザーは（自動的に）その証明を一度検証すれば、その後は高速版を実行するだけで済みます。

このアプローチは非常に強力であり、平井洋一氏がこれを「究極のソフトウェア開発形態」と呼ぶのには理由がある。

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

暗号学やコンピュータ科学の分野には、形式手法の歴史そのものとほぼ同じくらい古い伝統がある。それは、形式手法（あるいはより広く言えば、「証明」への依存）を批判する伝統である。

これらの文書には、実践的な事例が数多く含まれています。まずは、初期の単純な暗号理論の時代に書かれた手書きの証明から始め、2004年のメネゼスとコブリッツによる批判を引用してみましょう。

1979年、ラビンは、ある意味で「証明可能な」安全性を持つ暗号関数を提案した。これは、還元主義的な安全性特性を持つことを意味する。

還元主義的なセキュリティステートメントは、暗号文 y からメッセージ m を見つけることができる人は、n を因数分解できる必要があることを示しています。… ラビンが暗号化方式を提案した直後、リベストは、皮肉なことに、追加のセキュリティを提供するこの特徴が、「選択暗号文」と呼ばれる攻撃者に直面した場合、完全な崩壊につながると指摘しました。

つまり、攻撃者が何らかの方法でアリスをだまして選択した暗号文を復号させることができれば、攻撃者は前の段落でサムがnを因数分解するために使用したのと同じ手順に従うことができます。

メネゼスとコブリッツは、さらに例を挙げた。共通するパターンは、暗号化プロトコルをより「証明可能」にするための設計が、往々にしてプロトコルを「不自然」にし、設計者が想定もしなかったような形で失敗する可能性を高めるということだ。

さて、機械検証可能な証明とコードに戻りましょう。以下は、形式的に検証されたCコンパイラの脆弱性を発見した2011年の論文です。論文：

発見された 2 番目の CompCert の問題は、次のコードの生成につながる 2 つのバグとして現れます: 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が同じ決定論的な入力を与えたにもかかわらず、異なるプラットフォームで異なる公開鍵と署名を生成することを報告した。

このバグは、SHA-3のKeccak-f順列で使用されるXAR演算を実装する内部ラッパー関数vxarqu64に存在していました。フォールバックメカニズムがシフト演算に誤ったパラメータを渡したため、ハードウェアSHA-3をサポートしていないARM64プラットフォーム上でSHA-3ダイジェストが破損しました。

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

そして：

libcrux-psqライブラリは、ポスト量子事前共有鍵プロトコルを実装しています。decrypt_outメソッドでは、AES-GCM 128復号パスにおいて、エラーを伝播させる代わりに復号結果に対して.unwrap()を呼び出します。不正な形式の暗号文は、処理をクラッシュさせる可能性があります。

これら4つの問題はすべて、以下の2つのカテゴリーのいずれかに分類されます。

コードの一部のみが検証されたケース（残りの検証が困難だったため）。その結果、検証されていないコードには、作成者が想像していたよりも多くの脆弱性（しかもより致命的な脆弱性）が存在することが判明した。

著者が証明すべき重要な特性を明記し忘れたケース。

ナディム氏の記事には、形式検証における失敗モードの分類が含まれています。彼はまた、他の種類の失敗モードも提示しています（例えば、もう一つの主要なケースは「形式仕様自体が間違っている、または証明に誤った記述が含まれているにもかかわらず、構築されたシステムがそれを黙って受け入れてしまう」というものです）。

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

たとえメッセージを保護するために完全に安全な暗号化形式を使用していたとしても、数メートル離れた場所にいる誰かが電気信号の変動を捉え、何十万回もの暗号化を経て秘密鍵を抽出できるとしたら、依然として安全とは言えません。

これは、そのような手法のよく知られた例である「差分電力分析」に関する記事です。

差分電力解析は、一般的なサイドチャネル攻撃の一種である。出典：Wikipedia

こうした攻撃者に対するセキュリティを証明しようとする試みはこれまでも常に行われてきた。しかし、そのような証明には、攻撃者に対するセキュリティを証明できるような、攻撃者の数学的モデルが必要となる。

時には「dプロービングモデル」が用いられる。これは、攻撃者が回路内で照会できる場所の数には既知の制限があると仮定するモデルである。しかし、このモデルでは捉えきれない漏洩の形態も存在する。

この記事で述べたように、よくある問題は過渡的なリーク信号です。ある特定の場所の値だけでなく、その値がどのように変化するかにも依存する信号を観測できれば、多くの場合、1つの値からではなく、2つの値（古い値と新しい値）から必要な情報を復元できます。

この記事では、その他の漏洩形態の分類について説明します。

数十年にわたり、形式検証に対するこうした批判は、形式検証の改善に役立ってきた。過去と比較すると、私たちは現在、こうした問題への対策をより効果的に講じることができるようになっている。しかし、今日においても、形式検証は完璧ではない。

全体像を見ると、ここには一つの重要な流れがある。形式検証は強力だ。

しかし、マーケティング用語で形式検証が「証明可能な正しさ」を提供するように聞こえたとしても、いわゆる「証明可能な正しさ」は、ソフトウェア（またはハードウェア）が「正しい」ことを根本的に証明するものではありません。

一般的に「正しい」とは、「物事の挙動が、開発者の意図に対するユーザーの理解と一致する」といった意味合いを持つ。

そして「安全」とは、例えば「物事の動作がユーザーの期待に反せず、ユーザーの利益を損なうようなことをしない」といった意味合いを持つ。

どちらの場合も、正しさと安全性は、数学的な対象と人間の意図や期待との比較に帰着する。

人間の意図や期待は、それ自体が数学的に複雑な対象である。結局のところ、人間の脳は宇宙の一部であり、十分な計算能力があればシミュレーション可能な物理法則に従っているのだから。

しかし、それらは非常に複雑な数学的対象であり、コンピュータも私たち自身も理解したり読み取ったりすることさえできない。

実際的な意味では、それらはブラックボックスのようなものです。私たちが自分の意図や期待を理解できるのは、それぞれが長年にわたり自分の思考を観察し、他人の思考を推測してきた経験があるからに他なりません。

そして、生の人間的な意図をコンピュータに詰め込むことはできないため、形式検証によって人間的な意図との比較を証明することはできない。

したがって、「証明可能な正当性」や「証明可能な安全性」は、私たち人間が理解する「正当性」や「安全性」を実際に証明するものではありません。人間の脳を完全にシミュレートできない限り、それは不可能です。

では、それは何に役立つのでしょうか？

私は、テストスイート、型システム、形式検証を、プログラミング言語の安全性に対する同じ根本的なアプローチの異なる実装として捉える傾向があります（そして、それはおそらく唯一合理的なアプローチでもあるでしょう）。

それらはすべて、私たちの意図をさまざまな方法で冗長に指定し、それらの異なる仕様が互いに互換性があるかどうかを自動的にチェックすることに関するものです。

このPythonコードを例にとってみましょう。

def fib(n: int) -> int:

n < 0 の場合:

例外を発生させる（「負の値はサポートされていません」）

elif 0 <= n < 2:

nを返す

それ以外：

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

ここでは、あなたの意図を3つの異なる方法で表現します。

具体的には、コードにフィボナッチ数式を実装することで

暗黙のうちに、型システムを通じて（再帰における入力、出力、および中間ステップがすべて整数であることを指定する）

「サンプルパッケージ」方式によるテストケース

ファイルを実行すると、数式がサンプルと照合されます。型チェッカーは、型の互換性を検証できます。2つの整数を加算することは互換性のある操作であり、結果は別の整数になります。

物理の分野では、単位系はしばしば計算ミスを確認する良い方法となります。例えば、加速度を計算しているのに、メートル/秒ではなくメートル/秒²で答えが出てしまった場合、間違いがあったことが分かります。

テストケースは「サンプルパッケージ」定義の一例であり、これは直接的な明示的定義よりも、人間が概念を扱う上でより自然な方法となることが多い。

自分の意図を具体的に示す方法が多ければ多いほど、理想的には問題について異なる視点から考える必要があるような方法で表現すればするほど、それらの表現が互いに矛盾しないことが証明されたときに、自分が本当に望んでいることを表現できる可能性が高くなります。

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

形式検証を用いることで、このアプローチをさらに拡張できます。形式検証では、意図をほぼ無限の数の異なる冗長な方法で指定することができ、それらすべてが互換性がある場合にのみプログラムを検証できます。

高度に最適化された実装と、非常に非効率的だが人間が読みやすい実装を指定して、それらが一致することを検証できます。また、10人の友人に、プログラムが満たすべき数学的特性のリストを提供してもらい、それらがすべて満たされているかどうかを確認することもできます。

合格しない場合は、プログラムに誤りがあるのか、数学的な特性の指定が間違っているのかを調べてください。そして、これらの操作はすべてAIを使って非常に効率的に実行できます。

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

現実的に考えて、自分で証明を書くことはないでしょう。形式手法が普及しなかった理由は、ほとんどの人がこうした難解なコードの書き方を理解できないからです。以下のコードの意味を教えていただけますか？

/-- ヘルパー: アキュムレータを使用して、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 => 正確な 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署名の変種に対する特定のセキュリティステートメントの証明における多くの副補題の1つです。）

具体的には、この記述は「ハッシュ衝突が発生しない限り、あるハッシュダイジェスト（dig1）から生成されたメッセージの署名は、ハッシュラダー上の少なくともどこかで、他のどのメッセージの署名よりも高い値を必要とするため、他の署名からは計算できない情報が含まれる」というものである。

コードや証明を手動で記述する必要はありません。AIにプログラムを作成させ（Leanで直接記述する場合でも、高速化のためにアセンブリ言語を使用する場合でも）、その過程で必要な特性を証明させるだけで済みます。

このタスクの利点は、自己検証機能があるため、監視する必要がないことです。AIを数時間連続して実行させるだけで済みます。

最悪の場合、何の進展もなく空回りしてしまう（あるいは、私の研究室の実験のように、証明を求められた主張を置き換えて、作業量を減らしてしまう）。

最後に確認する必要があるのは、証明された主張があなたの要件を満たしているかどうかだけです。

SPHINCS署名バリアントの場合、最終的な声明は以下のとおりです。

定理 wots_fullDigits_incomparable

{dig1 dig2 : リスト 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) :

¬ すべての 2 に対して (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧

¬ すべての 2 (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

これは実際にはほとんど読めないレベルです。

あるハッシュダイジェスト（dig1）から生成された数値が、別のハッシュダイジェスト（dig2）から生成された数値と一致しない場合

すると、以下の2つの条件のいずれも満たされない。

すべての数値について、dig1 の数値≦dig2 の数値である。

すべての数値について、dig2 の数値は dig1 の数値以下である。

チェックサムを加算して生成される「拡張された数字」（wotsFullDigits）において、dig1の拡張では必然的に数字が大きい箇所があり、また別の箇所ではdig2の拡張の数字が大きい箇所があります。

大規模な言語モデルを用いて証明を作成するという点では、ClaudeとDeepseek 4 Proはどちらも十分な能力を備えていると思います。Leanstralは、Lean言語の記述に特化して微調整された、より小規模なオープンソースの重みモデルであり、有望な代替手段です。

パラメータ数は119Bで、トークン1つあたり6Bをアクティブ化します。ローカルで実行することも可能ですが、処理速度は遅くなります（私のノートパソコンでは約15トークン/秒）。ベンチマークによると、Leanstralははるかに大規模な汎用モデルよりも優れたパフォーマンスを発揮します。

私の現在の個人的な経験に基づくと、Deepseek 4 Proよりは若干効果が劣りますが、それでも非常に効果的です。

形式検証だけでは、すべての問題を解決できるわけではない。

しかし、インターネットセキュリティのモデルが、少数の強力な組織への信頼に基づくものでなくなることを望むのであれば、コードを信頼することに目を向けなければならない。それは、強力なAIの敵対者に直面した場合でも、コードを信頼することを含む。

AIを活用した形式検証は、この目標達成に向けて確かな一歩を踏み出した。

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

ブロックチェーンは、プライバシーとスケーラビリティを犠牲にする代わりに、オープンな検証可能性と検閲耐性を提供しますが、ZK-SNARKsはプライバシーとスケーラビリティを取り戻します（実際には、以前よりもさらに向上します）。

人工知能は、正確性を犠牲にして膨大な量のコードを書く能力を与えてくれますが、形式検証は正確性を取り戻してくれます（実際には、以前よりもさらに高い精度が得られます）。

デフォルトでは、AIは非常に急いで大量のコードを生成するため、バグの数が増加します。

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

しかし、サイバーセキュリティには明るい未来が待っている。ソフトウェアは（今後も）「安全なコア」の周囲に「安全でないエッジ部分」が分割されていくだろう。

安全性の低いエッジ部分はサンドボックス内で実行され、タスクを完了するために必要な最小限の権限のみが付与されます。

セキュアコアがすべてを管理します。セキュアコアがクラッシュすると、個人データや資金など、すべてが失われます。しかし、安全でないエッジ部分がクラッシュした場合でも、セキュアコアはユーザーを保護することができます。

セキュアコアに関しては、バグのあるコードが蔓延することを許容することはできません。セキュアコアを小型化し、さらに縮小するために、抜本的な対策を講じます。

その代わりに、AIによってもたらされるあらゆる追加性能を、セキュアコアのセキュリティ強化に投資し、高度にデジタル化された社会において私たちがセキュアコアに課す極めて高い信頼の負担に耐えられるようにします。

オペレーティングシステムのカーネル（あるいは少なくともその一部）が、そのような安全なコアとなるだろう。

イーサリアムもその一つになるだろう。

少なくとも、パフォーマンスをそれほど要求しない計算においては、使用するハードウェアが3分の1の要素となることを期待したい。

モノのインターネット（IoT）関連システムは4番目になるだろう。

少なくともこうしたセキュアなコアにおいては、「バグは避けられない。攻撃者がバグを見つける前に、それを見つけようと努力するしかない」という古い格言は覆され、真のセキュリティを実現できる、より希望に満ちた世界が到来するだろう。

しかし、もしあなたが、ずさんなソフトウェアに資産やデータを預け、それが誤ってブラックホールに飲み込まれてしまう可能性があっても構わないというのであれば、もちろん、あなたにもその自由があります。