ヴィタリック、「形式検証」活用を解説。AI時代のEthereum安全性向上で

AI時代の防御技術として「形式検証」に注目

イーサリアム（Ethereum）共同創設者ヴィタリック・ブテリン（Vitalik Buterin）氏が、ソフトウェアの正しさを数学的に証明する「形式検証（Formal Verification）」について解説するブログ記事を5月18日に公開した。 　

同記事のタイトルは「A shallow dive into formal verification（形式検証の基礎を理解する）」だ。ブテリン氏は、AIによるコード生成や脆弱性発見能力が急速に向上する中、暗号資産（仮想通貨）や暗号技術基盤の安全性をどのように担保するかが重要な課題になっているとの認識を示している。

ブテリン氏は記事冒頭で、イーサリアム研究開発コミュニティなどでの、「リーン（Lean）」と呼ばれるプログラミング言語を用いた形式検証が急速な広がりについて説明している。

リーンは、数学的証明を機械的に検証するためのプログラミング言語だ。開発者は、ソフトウェアが仕様通り動作することを数学的定理として記述し、その証明をコンピュータによって検証できる。

ブテリン氏は、こうした手法について、「適切に実行できれば、極めて効率的なコードを生成できるだけでなく、従来のプログラミングよりもはるかに安全になる可能性がある」と述べている。

また同氏は、イーサリアム研究者ヨイチ・ヒライ（Yoichi Hirai）氏が、この手法を「ソフトウェア開発の最終形態（the final form of software development）」と表現していることも紹介した。

今回のブテリン氏の投稿の背景には、AIによる脆弱性発見能力の急速な向上がある。近年では、大規模言語モデル（LLM）がソフトウェア脆弱性の探索や攻撃コード生成を高度化させているとの認識が、暗号資産業界やサイバーセキュリティ領域で広がっている。

同氏は、「暗号資産を扱うスマートコントラクトでは、コードの不具合によって資金が自動的に流出し、取り戻せなくなる可能性がある」と説明している。さらに同氏は、将来的にAIが脆弱性探索を自動化することで、こうした問題がさらに深刻化する可能性にも言及した。

そのうえで同氏は、形式検証について、AI時代における防御技術のひとつとして位置付けている。

一方でブテリン氏は、形式検証について「万能薬ではない」とも述べている。

同氏によると、形式検証では、「何を証明すべきか」を誤って定義した場合、実際には重要な問題を見落とす可能性があるという。また、検証対象外のコードやハードウェア側に脆弱性が残る可能性もあると指摘した。

そのうえで同氏は、「人間が本当に意図していること」そのものを、形式検証が完全に証明できるわけではないとの考えも示している。

一方で同氏は、AIと形式検証を組み合わせることで、暗号技術やブロックチェーン基盤の安全性を大きく向上できる可能性があると説明している。

日本ではNyxがLean活用を推進

日本では、イーサリアム研究機関「ニックス・ファウンデーション（Nyx Foundation）」が、リーンや形式検証を活用した開発を進めている。

Nyxは今年4月、イーサリアム次世代コンセンサス「リーン・コンセンサス（Lean Consensus）」へ対応するクライアント「ベリティ（Verity）」の開発開始を発表している。同クライアントでは、リーンの最新版である「リーン4（Lean4）」を用いてプロトコル仕様を形式化し、仕様と実装の整合性を数学的に検証する方針だ。

またNyxは5月、仕様書から検証チェックリストを生成するAI監査システム「スペカ（SPECA）」について、イーサリアム財団（Ethereum Foundation）の研究助成金に採択されたことも発表している。

Nyx創業メンバーのバンリ（banri）氏は、自身のXアカウントにおいてブテリン氏の投稿を引用した上で「AIと形式検証は非常に相補的な技術」と述べている。

同氏は、AIによってリーン形式検証コードが蓄積されることで、さらに高度な検証やコード生成が可能になる「複利的な相補技術」になるとの見解も示している。また同氏は、形式検証には「モデル検査」と「定理証明」が存在すると説明している。

そのうえで、ブテリン氏が今回主に言及しているものは、Nyxが進めている数学的証明を用いる「定理証明」型のアプローチに近いとの認識を示した。

参考：ブログ
画像：大津賀（あたらしい経済）

関連ニュース

参照元：ニュース – あたらしい経済

コメント

タイトルとURLをコピーしました