再入バグの再発防止：TLA+モデルとRustコードの連携

再入バグは、最初の「The DAO」契約から始まり、すべてのブロックチェーン上のスマートコントラクトを悩ませ続けています。その後、数億ドル、場合によっては数十億ドルがスマートコントラクトから盗まれるという大規模な攻撃が続きました。

これらのバグはテストでは非常に見つけにくいです。なぜなら、それらはスマートコントラクトコードの異なる部分が特定の順序で実行されるときにのみ発生するからです。この順序の数は膨大であり、単純なテストでは不可能です。

これまでのブログ記事では、TLA+を使用した形式的検証が、インターネットコンピュータのスマートコントラクト（またはカニスター）から再入バグを排除するためにどれだけ効果的かを示しました。これらの記事は次の通りです：

• TLA+でスマートコントラクトのバグを排除する: TLA+の紹介、ckBTCのケーススタディを使って、モデルチェックが再入バグを発見し、修正に役立つ方法を示します。
  

• TLA+モデルでバグを取り除く: DFINITYのオープンソースのTLA+モデル（NNS、ckBTCなど）と開発者向けの実例を紹介します。
  

• チュートリアル：インターネットコンピュータのカニスターにTLA+を使用する方法: インターネットコンピュータのカニスターをモデリングし、TLA+とPlusCalを使ってその特性をチェックするステップバイステップの技術ガイド。

再入バグの排除にTLA+が効果的であることが分かりましたが、TLA+の使用には制限がありました。TLA+モデルは、ある時点のコードのスナップショットに対応しているため、コードが進化するとモデルが古くなり、再入バグが再びコードベースに現れる可能性があります。この記事では、この問題に対処するアプローチを紹介します。それは、RustカニスターとそのTLA+仕様との整合性をテストする自動化フレームワークです。

TLA+と同期の課題

TLA+のアプローチでは、コードを直接テストする代わりに、コードの簡略化されたモデルを作成します。次に、TLA+ツール（特にTLCモデルチェッカー）に指示を出して、モデル内で可能なすべての実行シーケンスを系統的にチェックし、シーケンスが何であっても指定された特性が成り立つことを確認します。

例えば、NNSガバナンスのモデルでは、ニューロンの投票力がそのステーキングされたICPに正しく基づいていることを確認できます。TLCは、その実行シーケンスが攻撃者に投票力を増加させる可能性がある再入バグを発見することができます。あるいは、再入バグが存在しないことを確認することもできます。

このアプローチの大きな利点は、TLA+モデルがコードよりも簡素であり、モデルを効果的に分析できることです。そのため、MicrosoftやAWSなどのビッグテック企業もTLA+を使って重要なインフラを検証しています。

しかし、検証保証はモデルにのみ適用され、コード自体には適用されません。モデルは手動でコードとの整合性を確認できますが、コードが進化するにつれて、モデルがコードを正しく反映しているかどうかを確認するのは手間がかかります。そのため、モデルとコードが時間とともに同期しなくなり、モデル作成時に提供された強力な保証が最終的には失われることになります。

これが私たちが最近取り組んだ問題です。私たちは、RustカニスターのコードとそのTLA+モデルとの対応を自動的にテストするフレームワークを開発し、ガバナンスカニスターに適用しました。現在、私たちのCI（継続的インテグレーション）パイプラインは、ガバナンスコードのモデルからの逸脱を常にテストしています。これにより、私たちとICPコミュニティ全体は、NNSが安全であり、再入バグを通じてNNSの乗っ取りを試みる攻撃者からも安全であることを安心して確認できます。さらに、このフレームワークはガバナンス特有のものではなく、他のインターネットコンピュータのカニスター（コミュニティカニスターを含む）にも適用できます。

仕組み

TLA+モデルは、システムを遷移システムとして記述します。このようなシステムでは、いわゆる遷移述語がシステムが1つの状態から別の状態にどのように変わるかを記述します。述語が「true」となっている2つの状態s1とs2がある場合、システムは状態s1からs2に移行することができます。述語がs2とs3にも「true」であれば、システムはs1からs2、次にs3に移行でき、という具合です。遷移述語と「初期」の述語を指定することで、モデルチェッカーはすべての有効な状態のシーケンス（トレースとも呼ばれます）を構築できます。さらに、ユーザーは「良い」状態と「悪い」状態を定義する述語を指定でき、モデルチェッカーは「悪い」状態に達する有効なシーケンスがある場合に警告を出します。

これが私たちのカニスターにどう関係するのでしょうか？カニスターはメッセージを処理することで状態を変化させます。このメッセージはユーザーメッセージ、他のカニスターからのメッセージ、またはシステム生成の「ハートビート」や「タイマーメッセージ」である場合があります。メッセージは「メッセージハンドラー」と呼ばれるものによって処理されます。ICPはメッセージハンドラーの実行がアトミックであることを保証しているため、私たちはTLA+でカニスターをモデル化する際に、遷移述語を「関連するカニスターのメッセージハンドラーのいずれかが実行された」と定義し、（TLA+の述語で）各メッセージハンドラーが何をするのかを定義します。

問題は次のようになります：私たちはTLA+で、メッセージハンドラーが実際に何をするかを正しく反映させましたか？

これに答えるために、私たちは既存のカニスターのテストを再利用して、テスト実行から状態ペアを収集するツールを作成しました。収集された各状態ペアは、各メッセージハンドラーの開始時と終了時のカニスターの状態、または少なくともTLA+モデルに関連する状態の部分を記述します（関連するかどうかはユーザーが決定します）。

これで、TLA+モデルの遷移述語を呼び出し、私たちが観察した状態ペアが実際に述語を満たしているかどうかを尋ねることができます。もし満たしていなければ、コードがTLA+モデルでは考慮していなかった何かを行ったことが分かり、アラートが上がります（CIが失敗します）。前述のように、これはコードが進化するにつれて特に重要です。意図しない変更がTLA+モデルとの不整合を引き起こした場合、その検出が自動的に行われます。

どれくらいの作業が必要か？

ツールの使用には、以下の3つの主要なステップが必要です。

1. TLA+モデルの構築 まずはTLA+モデル自体を作成します。
   

2. Rustのキャニスターコードへのインスツルメンテーション 各メッセージハンドラの開始と終了を検出するため、またキャニスターの状態をTLA+の値にマッピングする方法を記述するために、Rustコードにインスツルメンテーション（計測用のコード）を加えます。　このインスツルメンテーションには2種類あります：　- 本番コード内に直接挿入するタイプ　- 別モジュールとして分離して保持するタイプ　前者についてはできるだけ小さく抑えることを重視しており、例えばガバナンス機能では本番コードに追加される行数は100行未満です。　後者についてはコンパクトに保つことを特に意識していませんが、それでも1000行未満に収まっています。
   

3. テストへのインスツルメンテーション

   記録された状態が遷移述語を満たしているかどうかをチェックするコードをテストに追加します。　Rustのみのテスト（つまり、実際にWasmをビルドしてレプリカにアップロードしないもの）であれば、テストごとに1行のコードを追加するだけで済みます。　Wasmベースのテストでは、記録された状態をクエリで取得できるようにするために若干の追加作業が必要ですが、それでもテストごとに1行のコードでチェックを呼び出せます。

   
   

ツールの詳細な技術的セットアップ手順は、ICのGitHubリポジトリに掲載されています。

結論

このツールは、モデルとRustカニスターコードの対応関係を安価で効果的にチェックすることに焦点を当てています。しかし、これにより検出されるのは、すでに書かれたテストの中で観察された逸脱のみです。未テストのシナリオでのみ発生する逸脱は検出できません。したがって、この設定で得られる保証は、特にコードレベルの検証に比べて弱いものです。

しかし、コードレベルの検証はTLA+モデルを記述し、それを自動でモデルチェックし、提供されたツールを使ってコードにインストゥルメントを施すことに比べてかなり労力がかかります。このアプローチは、必要な労力と提供される利益のバランスが取れていると私たちは考えています。さらに、これはテストと相乗効果を持ちます。テストカバレッジが広ければ広いほど、コードがTLA+モデルと同期しており、再入バグから安全であるという自信を持つことができます。

もし自分のカニスター用にTLA+モデルの作成を始めているのであれば、モデルとコードをリンクさせるためのツール（およびドキュメント）はICリポジトリから取得できます。

TLA+を使って自分のカニスターをモデリングし始めたばかりの方は、以下のリソースが役立ちます：

• 再入バグを防ぐためにTLA+がどのように役立つかを紹介するブログ記事

• インターネットコンピュータのカニスターをTLA+でモデリングする技術チュートリアル（パート1、パート2）

• 無料で利用できるTLA+リソース：**Learn TLA+**の本、Specifying Systemsの本、TLA+ビデオコース

• インターネットコンピュータのTLA+に関するドキュメンテーションページ