Ethereum共同創業者のVitalik Buterin氏は、AIによるハッキングの進展によってサイバーセキュリティが勝ち目のない競争になるわけではなく、ソフトウェアの安全性を証明する手段として形式的検証を指し示している。脆弱性の発見に依存するのではなく、開発者はプログラムが定義されたセキュリティ要件を満たしていることを数学的に示せると同氏は主張する。

5月18日のブログ投稿で、同氏はXで共有し、AIによってこうした検証を大規模に実用的にできると主張した。このアプローチは、暗号技術、メッセージプロトコル、ブロックチェーンソフトウェアを含む重要なシステムにとって特に重要だとしている。

セキュリティは証明される前に定義されなければならない

Buterin氏は、プログラムが安全であることを証明するには、まずセキュリティが実際に何を意味するのかを定義する必要があると述べた。同氏は暗号化メッセージングアプリSignalを例に挙げ、暗号化だけではすべてのセキュリティ上の懸念をカバーできるわけではないと指摘した。完全な定義には、メッセージの偽造、配信失敗、リプレイされたメッセージ、ハッキングされたデバイス、漏洩した鍵への対応が含まれる可能性がある。

ハードウェアはさらに複雑さを加える。物理的な信号から情報が漏れる可能性があり、メッセージサイズ、送信者の識別、タイミングといった詳細自体が情報を明かしうる。これらの考慮事項が組み合わさると、セキュリティ定義は1,000行を超えることもある。それでもButerin氏は、定義は基盤となる実装よりも検証対象としては小さいと主張した。

形式的検証の対象はプログラム全体

形式的検証は新しい概念ではない。失敗のコストが高い航空機や医療ソフトウェアといった安全が重要視される分野で長く用いられてきたが、その負担の大きさから汎用開発ではまれだった。歴史的に、開発者は自身がセキュリティ上重要と特定した部分だけを検証してきたが、それは主に検証が多大な労力を要したためだ。Buterin氏は、AIがこの方程式を変え、プログラム全体の検証をより実用的にし、データベース、ネットワーキング、キャッシュ層、その他のコンポーネントまでカバー範囲を広げられると主張した。

同はこの目標を、防御側が攻撃者に先んじて脆弱性を発見する競争をするという従来のモデルとは異なるものとして位置付けた。このアプローチでは、セキュリティ要件を満たしていることを証明することでソフトウェアの耐障害性が高まる。異なるグループが別々の要件を定めた場合には定義を組み合わせることもでき、2つの定義が共存できない場合は、根底にある設計上の矛盾を切り分けられると述べた。ただし、一部のユーザーインターフェースは依然として扱いが難しいことを認めた。

Ethereumソフトウェアの複雑な検証ニーズ

Buterin氏は、メッセージパッシングプロトコル、サンドボックス、SNARKs—計算が正しく実行されたことを示すコンパクトな暗号学的証明—、そして暗号化されたデータのまま計算を可能にする完全準同型暗号を、定義と実装の区別が重要となりうる分野として挙げた。同氏はこのアプローチをEthereumの開発の方向性に直接結び付け、ブロックチェーンにはより強固なソフトウェアセキュリティが必要であり、特にスケーラビリティとプライバシーを追求するシステムにおいてそうだと述べた。

この状況はリスクの大きさを浮き彫りにする。ブロックチェーンソフトウェアはオープンソースであり、それが支えるネットワークは資産を直接保持している。そのため、同じコードが攻撃者と防御者の双方の目にさらされている—こうした条件下では、誰が先に脆弱性を見つけるかに依存しない保証が特に重みを持つ。

同氏の主張の中心は、脆弱性の発見だけに頼るのではなく、数学的な検証に置かれている。検証は選択されたコード部分にとどまらず、定義には綿密な作業が求められ、実装も形式的な検証の対象であり続けるという。AIはそのプロセスの規模に対応し、データベース、ネットワーキング、キャッシュ、その他のコンポーネントをカバーできると同氏は考えている。注目すべきは、AI支援ツールがプログラム全体の検証を、同氏が最も難しいケースとして挙げたユーザーインターフェースを含め、本番規模の日常的な実践にまで持ち込めるかどうかである。