先週のOOPSALA '25で、Actの開発者は、ブロックチェーンプロトコルのゲーム理論的セキュリティを正式に検証するための自動証明者であるCheckMateの改良されたスケーラブルなバージョンを発表しました。 要するに、このツールは、プロトコル内のインセンティブが不正行為に価値がないものにするかどうかをチェックします。
プロトコルには、次の 3 種類のセキュリティが必要です。 •暗号化:キー/パスワードは強力ですか? • 実装: コードにバグはありますか? • ゲーム理論: 不正行為が報われないようにインセンティブが調整されていますか? 最後のものは重要ですが、無視されがちです。
ゲーム理論的なセキュリティとは、合理的で利己的な行為者でさえ、ルールに従うことを好むようにすることです - 逸脱すると、収入よりもコストがかかるためです。 それは安全保障の「経済学」です。
CheckMateは、SMTソルバーを使用してゲーム理論上のセキュリティを正式かつ自動的に証明します。この論文では、数百万のノードに拡張され、モデルの生成と分析をインターリーブして効率を高める構成的な「分割統治」アルゴリズムを紹介しています。
なぜこれが重要なのか: ブロックチェーンプロトコルのインセンティブが不正行為を不合理にしていることを、展開前に自動的、正式に、大規模に証明できるようになりました。
273