Keetaの2相コンセンサスを形式検証、永久ロックアウトの条件を発見
Modeling and Verification of Keeta's Consensus [pdf]
Keetaは、国境を越えた高額決済向けに設計されたブロックチェーンネットワークで、クライアント主導の2相コンセンサスアルゴリズムを採用しています。本論文では、このアルゴリズムをQuintで形式仕様化し、TLCモデルチェッカーを用いてビザンチン障害モデル下で検証しました。その結果、固定された等重みの代表者集合の下で合意が保持されることを確認し、任意の代表者数への一般化を論じるとともに、競合するアカウントが恒久的にロックアウトされる条件を明らかにしました。ステーク加重投票下での安全性は未解決のままです。
コンセンサスアルゴリズムの正しさは、その設計に固有であり、各プロトコルごとに独立して確立されなければならない。
- rkeene2
Keetaの開発者です。状態を持つ実行と持たない実行の両方で、私たちのコード実行の扱い方はSuiとはかなり異なるものになると思います。
- dlahoda
> クライアントは競合を管理し、必要に応じてトランザクションを再送信する責任があります。
「太った」クライアントは、多数の「RPC」に同時に話しかけ、トランザクションに対する「2相」コミットの最終投票を得る必要があります。
クライアントは、Proposer-Builder分離におけるBuilderのようなものです。
各代表者は、すべてのアカウントのすべてのデータを保存します。彼らはDAを行います。
- xescure
Keetaは、新しい高スループットの決済ブロックチェーンです。その起源は、手数料無料のDAG DLTであるNanoと、FacebookのFastPayに遡りますが、正式な検討に値する多くの新しい貢献があります。
ここでは、そのコンセンサスプロトコルの形式的なQuint仕様を提示し、ビザンチン障害モデルの下でモデル検査を行いました。安全性は、障害範囲内かつ一定の重みモデルの下で維持されることが判明し、FastPayスタイルのロックアウトの可能性が予想通り再現されました。
今後の研究の方向性は、Keetaが取る方向性に依存します。チェックポイントとエポック（Suiに類似）が、注目すべき機能です。
前提となる論文: https://keeta.com/whitepaper.pdf
Googleのマーケティングスロップ: https://cloud.google.com/blog/topics/financial-services/how-...