ヴィタリック、イーサリアムなどの安全性や効率性の向上策を分析

この記事のポイント

形式的検証×AIでETHの安全性向上へ
防御側有利な安定局面到来をブテリン氏が予測

イーサリアムなどの向上策を分析

暗号資産（仮想通貨）イーサリアム（ETH）の共同創設者のヴィタリック・ブテリン氏は18日、形式的検証（formal verification）に関するブログを公開した。

形式的検証とは一般的に、ソフトウェアなどのシステムの正しさを数学的に証明する手法のこと。ブテリン氏は、形式的検証とAI（人工知能）を組み合わせてイーサリアムなどの安全性や開発の効率性を高めることができると分析している。

ブテリン氏は冒頭で、この数カ月の間にイーサリアムの最先端の研究開発コミュニティやコンピューティングに関する他の多くの領域で、プログラミングの新しい手法が急速に普及しつつあると指摘した。

そして、具体的に新しい手法とは、機械語に近いプログラミング言語（EVMバイトコードなどの低級言語）かLeanで直接コードを書き、Leanで書いた自動チェックが可能な数学的証明でコードの正しさを検証するという方法だとしている。

この手法が正しく行えれば、非常に効率的なコードを出力したり、以前のプログラミングよりもはるかに高い安全性を確保したりできる可能性があると主張。ブテリン氏は「この手法はソフトウェア開発の最終形態である」との言葉を引用している。

その上で、今回のブログは、イーサリアムなどにおいて現在何が起きているか、ソフトウェアの形式的検証は何ができるのか、どのような弱点や制限があるかの基礎をわかりやすく説明することを目指すものだと説明した。

ブテリン氏は、現在はAIの発展によって形式的検証が行いやすくなっていると指摘。形式的検証の定義については「数学的な定理の証明を、それらの定理が自動的にチェックされることが可能な方法で記述することを指す」と説明した。

安全性の向上策

今回のブログは最初のパートのタイトルである「形式的検証とは」や次の「コンピュータープログラムの検証」などと順に展開する、非常に長くて一般の人々には難解な内容である。

その中でブテリン氏は今回、「セキュリティのための形式検証」というパートで、最近注視されている北朝鮮に関連する攻撃やAIモデル「クロード・ミュトス（Claude Mythos）に言及した。

ブロックチェーンセキュリティ企業CertiKは最新レポートで、北朝鮮は近年、仮想通貨ハッキングを国家的な資金調達手段として組織化・産業化していると指摘した。2016年以降、263件の攻撃で約67.5億ドルを窃取。少数の「高価値ターゲット」に狙いを定め、国家の支援により、粘り強く高度な潜入活動を行う傾向がある。

ブテリン氏は、コンピューターのコードに潜むバグについて、変更不可能なブロックチェーンのスマートコントラクトに仮想通貨を預け、そこから北朝鮮の関連組織が自動的に資産を引き出すことが可能で、なおかつバグが原因であるために救済手段がない時に恐怖が増すと指摘している。

また、クロード・ミュトスのような強力なAIモデルが登場し、さらに改良が重ねられて自動的にバグを発見できるようになれば、さらに恐怖感が高まるとも指摘。他にも、ゼロ知識証明にバグが含まれている場合の恐ろしさにも触れた。

片山さつき財務大臣が24日、アンソロピックの新型AI「クロード・ミトス」のリスクをめぐり3メガバンク幹部や日銀植田総裁と緊急会合を開く。OSの脆弱性を悪用できる能力が金融システムへの脅威として国際的に注目されている。

このような恐怖に対し「唯一の解決策はオープンソースという特徴自体を手放すことだ」などの悲観的な意見もあるが、ブテリン氏は将来的なサイバーセキュリティについて、もっと楽観的な見方をしていると述べている。

強力なAIによるバグの発見という課題は深刻だが、これは過度期の課題であると考えていると説明。事態が落ち着き、新たな安定局面に入れば、以前よりも防御側に有利な状況が生まれるとの見方を示した。

ブテリン氏は、形式的検証は万能薬ではないが、「目的が実装よりもシンプルな場合」に特に有効であると指摘。イーサリアムがこれから実装しようとしている量子耐性のある署名やZK-EVMなどの、展開が極めて困難な技術にも有効性が当てはまるとした。