イーサリアムのVitalik ButerinがAIによってスマートコントラクトを真に安全にする方法を解説

この記事はCoinpedia Fintech Newsに最初に掲載されました：イーサリアムの共同創設者Vitalik Buterinが、AIがスマートコントラクトを真にセキュアにする方法を解説

イーサリアムの共同創設者Vitalik Buterinは、AIを活用した形式検証がセキュアなソフトウェアの構築方法を根本的に変える可能性があると詳しく論じる記事を公開した。これは、AI 駆動の攻撃がますます強力になる中で、トラストレスなシステムが生き残れるかどうかについて、サイバーセキュリティコミュニティで高まる悲観論に対する反論でもある。

「AIを活用したバグ発見により、セキュアなコードは不可能になると多くの人が主張している」とButerinは記した。「私はもっと楽観的な見方をしており、AIを活用した形式検証がその主な理由の一つだ。」

形式検証とは何か

形式検証とは、コンピューターが自動的にチェックできる数学的証明をコードについて記述する手法である。ソフトウェアをテストしてバグが現れないことを願うのではなく、開発者はあらゆる条件下でコードが意図した通りに動作することを数学的に保証する証明を記述する。

この技術は数十年前から存在するが、これらの証明を手作業で書くことは非常に難しく時間がかかるため、ニッチな存在にとどまってきた。Buterinの主張は、AIがこの方程式を劇的に変えるというものだ。AIはコードと証明の両方を書くことができ、人間は証明されている内容が実際にソフトウェアに求めることと一致しているかを確認するだけでよい。

彼はこの組み合わせを、研究者の平井洋一氏が「ソフトウェア開発の最終形態」と呼ぶものとして説明した。

イーサリアムにとっての重要性

Buterinは、イーサリアムの開発エコシステム内ですでに形式検証が適用されているいくつかの分野を挙げた。量子耐性署名、STARKプルーフシステム、コンセンサスアルゴリズム、ZK-EVMなどが含まれており、これらはいずれも基盤となるコードが極めて複雑であるにもかかわらず、セキュリティ特性の定義が比較的シンプルな分野だ。

Arklibのようなプロジェクトは、完全に形式検証されたSTARK実装に向けて取り組んでいる。evm-asmプロジェクトは、RISC-Vアセンブリで直接記述されたEVM全体を構築し、人間が読めるリファレンス実装に対して数学的に検証している。ビザンチン障害耐性コンセンサスプロトコルも、Leanで形式的に仕様化・検証が進められている。

重要な洞察は、これらのシステムにおいて、コードが実際に行うことと本来すべきことの間のギャップを、確率的なテストではなく数学的な確実性によって埋められるということだ。

認められている限界

Buterinは、主張を誇張しないよう注意を払っていた。形式検証には実際の失敗モードが存在する。証明はシステムの一部についてのみ記述され、重要なバグが未検証の部分に潜む可能性がある。開発者が重要な特性の仕様を忘れることもある。形式仕様そのものが誤っている場合もある。サイドチャネル攻撃のようなハードウェアの脆弱性は、数学的に正しいソフトウェアでさえも回避できる。

「証明可能な正しさは、多くの人間がソフトウェアの正しさを理解する方法でそれを証明するものではない」と彼は記した。形式検証が実際に行うことは、開発者が複数の異なる冗長な方法で意図を表現し、それらの表現がすべて互いに適合しているかを自動的にチェックすることを可能にするものだ。

より広いビジョン

Buterinは、ソフトウェアが二つの層に分かれる楽観的な未来を描いた。セキュアでないエッジ層は重要度の低い機能を担い、サンドボックス内で動作し、最小限の権限で稼働する。セキュアなコアは、イーサリアム自体、OSカーネル、センシティブなIoTインフラを含む重要なすべてを担う。

セキュアなコアは意図的に小さく保たれ、積極的な形式検証にさらされる。AIは検証を大規模に実用的なものにする計算能力をもたらす。その結果は、バグゼロのソフトウェアではなく、最も重要なコンポーネントを希望ではなく数学的な確信をもって信頼できるソフトウェアだ。

「守る側がついに、決定的に勝てるチャンスがある」と彼は締めくくり、AI 駆動の攻撃ツールに対してコードベースを強化したMozillaの実際の経験を引用した。