ヴィタリック・ブテリン、スマートコントラクトのバグフリーな未来を予測

セキュリティを最優先する開発者であれば、イーサリアムの共同創設者であるヴィタリック・ブテリン氏によると、バグのないコーディングが実現可能になるのは2030年代になると予想されます。 

Gnosis Chainの940万ドルのBalancerハッキングからの資金回収をめぐる論争の的となったハードフォークの後、イーサリアムの共同創設者であるヴィタリック・ブテリン氏は、「バグは避けられず、バグのないコードは作れない」という信念は2030年代には真でなくなるだろうと述べました。

ヴィタリック・ブテリン氏はコーディングについて何と言ったのか？ 

ヴィタリック・ブテリン氏は、ソーシャルメディアプラットフォームXでのやり取りを通じて、2030年代にはバグのないコードが一般的になるだろうと予測しました。 

この議論は、Gnosis Chainが12月22日にハードフォークを実行したと発表したことから始まりました。これは 報告しました。これには完全な準備預金と独立監査が含まれます。 Cryptopolitanによって報じられました。このハードフォークにより、2024年11月のBalancerの脆弱性攻撃中に盗まれた940万ドルが回収されました。この攻撃では複数のブロックチェーンにわたって1億2800万ドル以上が盗まれました。回収にはほとんどのバリデーターが新しいソフトウェアを採用する必要があり、更新しなかったバリデーターはペナルティに直面しています。

もちろん、この動きはブロックチェーン支持者からの抵抗を受けました。彼らはこの動きが不変性の原則に反すると批判しました。『colluding node』というハンドル名のXユーザーは、本当の問題はブロックチェーンアプリケーションがどのように構築されているかだと述べました。彼らは、プログラム可能な仮想マシンでスマートコントラクトを使用することは間違ったアプローチだと主張しました。 

「書くべきコントラクトは7つだけであり、それらはベースレイヤーに刻み込まれ、クライアントの多様性からセキュリティを得るべきです」とそのユーザーは書き込みました。 

ブテリン氏はその後 は 形式的検証が証明可能なバグフリーと等しいわけではないことを明確にするために発言しました。さらに、証明可能なバグフリーのコードが不可能である可能性さえ示唆しました。

「『証明可能なバグフリー』は不可能だとさえ言えます。なぜなら、『バグフリー』とは『意図とコード実行の間のギャップがない』ことを意味しますが、私たちの意図は非常に複雑なオブジェクトであり、私たちはそれに限られたアクセスしか持っていないからです。」 

形式的検証は、安全上重要なシステムが正しく動作するかどうかを確認するために数学的な手法を使用します。この技術は1960年代から航空宇宙工学などの分野で使用されてきました。 

スマートコントラクトで使用される場合、形式的検証により、コントラクトのビジネスロジックが事前に定義された仕様を満たしていることを証明できます。しかし、 Balancerのコントラクト 4つの異なるセキュリティ企業によって11回監査されましたが、致命的な欠陥がまだ見逃されました。 

バグフリーなコードの未来は可能なのか？ 

ブテリン氏は、意図と実行の間のギャップをフィルタリングするための多重の冗長性の層が解決策だと提案しました。彼は、型システムを冗長性の一種として、そしてコードに関する特定の主張を形式的に検証することを別の層として挙げました。

形式的検証は、監査人やテスターの見逃しうる整数のアンダーフローやオーバーフロー、リエンタント、およびガスの最適化の欠如などの問題を検出できます。一方、従来のテストはエラーの存在を確認するだけで、その欠如を確認することはできません。

ブテリン氏は、特定のケースでは機能の向上が完璧さよりも重要であるため、一部のソフトウェアにはバグが残るだろうと指摘しました。しかし、セキュリティを最優先する開発者には、真にバグのないコードを達成するためのツールが備わっています。