Buterinは、逆のことが最終的に起こる可能性があると自信を持っています。AIは、防御側に最初から悪用されにくいソフトウェアを構築するためのツールを提供するかもしれません。
「AIハッキングによってサイバーセキュリティは終末を迎えるという意見が増えてきていますが、私はそれに同意しません」とButerinは、水曜日にXソーシャルネットワークで長文かつ特徴的に内容の濃い投稿をしました。
Ethereum共同創設者によれば、開発者が正式な検証（フォーマル・ベリフィケーション）を完全に活用し始めれば、サイバーセキュリティは自然に防御側に有利になるはずだと述べています。
Buterinはこの考えを自身の暗号資産への関与と直接結び付け、彼の純資産の約90%が暗号資産にあることを明かしました。
大量の暗号資産を保持し続ける人は、より高度な攻撃者がいる中でも十分に安全なデジタルシステムが構築できると暗黙のうちに賭けている、と彼は主張しています。
「もしAIがNavier-Stokes問題やFLT（フェルマーの最終定理）を証明できるなら、AIは『このプログラムは安全である』という命題も数学的定理として証明できる」とButerinは述べ、Navier-Stokes問題とフェルマーの最終定理に言及しました。
彼の主張は、ソフトウェアが特定の条件を満たしていることを数学的に証明する正式な検証に基づいています。
Buterinは、5月のエッセイでもこのアイデアを詳しく考察し、AI支援によるフォーマル・ベリフィケーションはセキュリティ重視のソフトウェアにとって極めて変革的なツールになると述べました。しかし、そのようなソフトウェアが本当に安全であると証明するのは難題となる可能性もあります。
定義の問題
Buterinは暗号化メッセージングアプリSignalを例に挙げ、これがなぜ難しいのかを説明しました。
攻撃者はメッセージを偽造したり、配信を妨害したり、過去のメッセージを再送信したり、サーバーを侵害したり、他ユーザーの公開鍵を発見するプロセスを操作したり、オペレーティングシステム上の脆弱性を突いたりすることが可能です。
他にも、データベースの破損、悪意あるライブラリやコンパイラ、ハードウェアレベルの情報漏洩などによってトラブルが発生することもあります。
会話内容が暗号化されたままでも、攻撃者が誰と誰が通信しているかを知ることができる場合もあり、「安全」とは何かという数学的定義自体が極めて複雑になり得ます。
「ですから…定義だけでも千行以上のコードになることがあり、それを理解するためには深い慎重な思考が必要なのです」とButerinは述べています。
攻撃者と防御者
間違いなく、より高度なAIシステムは脆弱性の発見を容易にするでしょう。
しかし、同じ機械的推論の進歩によって、慎重に設計されたセキュリティ仕様に従ってソフトウェアが動作することを正式に証明するコストも劇的に下がる可能性があります。
両者ともAIを持つことになるでしょう。
