2016 年 6 月、イーサリアム ブロックチェーン上に構築された「The DAO」が世界初の完全デジタルの分散型投資ファンドになろうとしているという興奮が高まっていました。
しかし、攻撃者がそこから 5,000 万ドル相当のイーサを盗んだ後、数週間以内に、代わりに DeFi ハッキングの代表的な存在になりました。
DAO をクラックするために、攻撃者はいわゆる再入性の脆弱性、つまり、特定のスマート コントラクトの 1 つのメソッドが実行中に別のメソッドが呼び出される同時実行性の脆弱性を悪用しました。DAO は、DAO の長期開発の一部にすぎません。スマート コントラクト 最初のものは、このようなエラーに悩まされます。
著名な後継者には、2020年に2,500万ドルが盗まれたUniswap/Lendf.Me、2021年に1,800万ドルが盗まれたCREAM、2022年に8,000万ドルが盗まれたFeiなどがあります。
これらのバグが存続する理由は、スマート コントラクト全体に散在する予期しないコードの相互作用、場合によっては完全に異なるスマート コントラクトに含まれる可能性があり、そのようなコードの相互作用の数が非常に多くなり、人間が意図しないスマート コントラクトを検出して排除することが困難になるためです。 .コードが必要です。
さらに、これらのインタラクションは、多くの場合、自動的かつ体系的にテストすることが困難です。
TLA+: エクスターミネーター
複雑なシステムを指定および検証するための言語である Temporal Logic of Actions (TLA+) を使用すると、エラーを検出するだけでなく、その存在も検証できます。
どうしてそんなことが可能なのでしょうか？ TLA+ には、いわゆるモデル チェックの形式で軽量の形式的検証を行うためのツール セットが付属しています。モデル チェックを通じて、コード モデルの考えられるすべての同時対話 (まさにテストが難しい領域) を徹底的に調査し、バグを発見します。
隅々まで照らして、見落とされたり無視されたりしがちな暗い隅に隠れている不要な害虫を明らかにし、排除する害虫駆除業者を想像してみてください。重要なのは、コード モデルの構築後は、モデル チェックを実行するために人による入力がほとんど必要ないため、コスト効率が非常に高いことです。
いくつかの作られた数字で説明すると、テストやセキュリティ レビューなどの業界標準の手法によってバグの 80% が排除され、「強力な」形式的検証によって 99% が排除される場合、TLA+ を使用すると、少数の強力な検証作業を 1 回行うだけで 90% が排除されます。
TLA+ とインターネット コンピューター
当社のエンジニアリング チームは、TLA+ を使用して、プラットフォーム上で実行されるセキュリティ クリティカルなスマート コントラクトを含む、インターネット コンピューティングのあらゆる側面を分析します。イーサリアムとインターネット コンピューターの実行モデルは異なりますが、両方のブロックチェーンのスマート コントラクトで再入エラーが発生する可能性があります。
実際、インターネット コンピュータはスループットが高いため、単一のスマート コントラクトへの複数の同時呼び出しが可能です。そのため、スマート コントラクトの作成者は、不要な同時インタラクションを排除するためにより注意する必要があります。インターネット上でコンピュータが成功するためにはセキュリティが不可欠であるため、TLA+ は開発段階でエラーを検出するために多くのスマート コントラクトで使用されています。
最近、新しくリリースされたチェーンキー ビットコイン (ckBTC) に対して TLA+ 分析コンテナ (インターネット上のコンピューター用のスマート コントラクト) が実施されました。その結果を以下に共有します。
ckBTC スマートコントラクト
ckBTC の TLA+ 分析について話すために、ckBTC の概要から始めましょう。 ckBTC は、1:1 の比率でビットコイン (BTC) によって安全に裏付けられたインターネット コンピューター ネイティブ トークンです。
ckBTC 台帳は、インターネットのコンピューター ブロックチェーン上のコンテナ スマート コントラクトで、各エンド ユーザーが所有する ckBTC の量を追跡します。この同じ台帳により、エンド ユーザーはビットコイン ネットワーク上で BTC を転送するよりも速く、安価に ckBTC を他のエンド ユーザーに転送できます。
ckBTC を BTC に変換したり、逆に変換したりするために、エンドユーザーは別のスマート コントラクトである ckBTC ミンターと対話します。
大まかに言うと、BTC から ckBTC への変換操作は次のようになります。
ckBTCを取得する手順:
1. エンドユーザーは最初に一部の BTC をユーザー固有のビットコイン デポジット アドレスに転送します。すべてのデポジット アドレスは、チェーン キー ECDSA 署名により、ckBTC minter スマート コンテナーのコードによって完全に制御され、デポジットが所有する新しい UTXO が作成されます。住所;
2. エンドユーザーは、ユーザー残高の更新を造幣局に依頼することで、ckBTC 造幣局スマートコントラクトに新しく預けられた UTXO を通知します。
3. 次に、ミンターのスマート コントラクトは、インターネット コンピューターのビットコイン統合を使用して、ミンターが制御するユーザー固有の入金アドレスが所有するすべての UTXO を取得します。次に、ミンターは、クロスチェックを送信することで、ビットコイン ネットワークから新しい UTXO を厳選します。処理した UTXO の内部簿記リスト。
4. 最後に、ミンターは台帳に対して、すべての新しい UTXO に対して新しい ckBTC を 1:1 の比率でミントするように指示し、完了すると、新しく発見された UTXO を処理済み UTXO のリストに追加します。
免責事項: 上記のプロセスでは、簡略化するために KYT (Know Your Transaction) プロセスを省略しています。
ckBTC スマート コントラクトが TLA+ に適合
上に示した概要図には、実際には同時実行性に関する微妙な問題が隠されていますが、幸いなことに、TLA+ ツールキットを使用して問題を検出できるということです。
ただし、TLA+ が何かを検出できるようにするには、まず次の 2 つのものを TLA+ に提供する必要があります。
TLA+ 言語を使用してシステムのモデルを作成する
システムが実装することが期待される TLA+ プロパティを指定します
このモデルは、簡略化されていますが、完全に定義されたシステムのバージョンです。この例では、ミンター スマート コントラクトだけでなく、システムの他のすべての関連部分、つまり台帳コントラクトとビットコイン ネットワークも含まれています。
各コンポーネントについて、その状態と、エンドユーザーが実行する関連アクション (つまり、BTC または ckBTC の転送、BTC の入金、ミンターによって公開されるさまざまなアクションの呼び出し) によって状態がどのように変化するかをモデル化します。
これらすべての要素はモデル内である程度単純化されており、分析で焦点を当てている部分 (ミンター コードなど) はより詳細にモデル化されていますが、他の部分 (ビットコイン ネットワークなど) はあまり詳細にモデル化されていません。実際、TLA+ モデルは、システムの詳細な設計仕様に似ています。
直感的に、私たちが実装したい主な機能は、ckBTC が完全にサポートされていることを確認することです。言い換えれば、エンドユーザーは、入金した BTC を「二重支払い」して、入金した以上の ckBTC を取得することができるべきではありません。
しかし、そのような特性を分析するには、TLA+ 言語で形式的に表現することによって、この直感を非常に正確にする必要があります。私たちの正式な定義は、ckBTC の総供給量 (つまり、ckBTC 台帳に保存されているすべてのエンドユーザー ckBTC 残高の合計) が、鋳造コンテナによって管理されている BTC の総量 (つまり、すべてのビットコインの価値) を超えないということです。デポジットアドレスが所有する UTXO)。
問題を検出して解決する
モデルとプロパティを作成したら、TLA+ ツールキットでモデルを分析できます。分析を実行するには、まず分析を実行するための設定を定義します。たとえば、ckBTC のセットアップには 2 人の異なるエンド ユーザーと、ビットコインの総供給量のうちの少量 (例: 5 サトシ) のみが含まれています。
この設定は非常に限られていますが、実証研究によると、コンピューター システムの問題の大部分は少数のエンティティで発生する可能性があります。小規模なセットアップにより、分析では、モデルによって定義されたすべての可能なアクション シーケンスを系統的に調査し、そのようなシーケンスで所定のプロパティが保持されるかどうかを確認できます。
さらに、分析は完全に自動的に実行されます。つまり、人による入力は必要ありません。これらの特性が当てはまらない場合は、その特性に違反する操作の正確なシーケンスが提供されます。
たとえば、分析により、以下のようなシナリオでは「安全でない ckBTC なし」プロパティに違反する可能性があることが判明する可能性があります。
ここ：
エンドユーザーは以前と同様に BTC を入金します。
しかし、現在、エンドユーザーは ckBTC ミンターに残高を 2 回続けて更新するように指示しており、インターネット コンピューター上でこれらの更新を他のスマート コントラクトと同時に行うことができます。
同時に実行されている 2 つの更新は、エンド ユーザーによってデポジットされたすべての UTXO をビットコイン ネットワークに要求し、どちらも応答としてステップ 1 でデポジットされた同じ UTXO を受け取ります。UTXO はまだ「処理済み」リストに含まれていないため、両方の更新は UTXO が新しいと考えます。
どちらの更新も、ステップ 4 で対応する量の ckBTC を鋳造するように台帳に指示します。
したがって、ステップ 4 の終了時点では、ckBTC の供給量がデポジット アドレスの UTXO の合計の 2 倍になっている状態になり、これは「サポートされていない ckBTC がない」という特性に違反します。
このエラーは、エンドユーザー残高の更新が同時に実行されるためにのみ発生することに注意してください。実際には、DAO をダウンさせたエラーと同じ形式の再入可能エラーです。
この問題を解決する 1 つの方法は、残高更新が同じエンド ユーザーに対して並行して実行されないようにすることです。これを行うには、残高更新の開始時にミンターにエンド ユーザーを「ロックされた」ユーザー リストに保存させ、そこに保持させます。これを達成するには、更新リストの期間中。
エンド ユーザーが別の同時残高更新を開始しようとすると、更新はまずロックされたユーザー リスト内でこの特定のエンド ユーザーを確認して見つけ、その後中止されます。
ここでは攻撃を少し単純化していることに注意してください。ロックは実際には IC スマート コントラクトではかなり一般的なパターンであり、ckBTC ミンターは最初からそれを展開しています。ただし、ロックが不適切に実行されると、上記の攻撃への扉が開き、TLA+ はこれを検出できます。
さらに、「サポートされていない ckBTC なし」やその他の重要なプロパティに違反するいくつかのエッジ ケースが見つかり、すべての修正を適用すると、定義した設定にプロパティ違反がなくなったことを TLA+ が検証して確認できました。
スマート コントラクトに TLA+ を使用する必要がありますか?
絶対に！わかりました、わかりました。おそらく、私はより微妙な答えを提供する必要があるかもしれません。私たちの研究開発チームは、重要な同時実行が関係するときはいつでも、インターネット コンピューター上の重要なスマート コントラクトにこの答えを使用します。
たとえば、TLA+ 分析により、以前の手動セキュリティ レビューでは見逃され、重大な問題、ケース、ポイントにつながる可能性があった、インターネット コンピュータ ガバナンスと台帳コンテナの同時実行性の微妙なバグが発見されました。TLA+ は、そのような厄介な問題を明らかにするのに役立ちました。本当に素晴らしい結果でした。
もちろん、ノウハウの取得とモデルの構築という点では代償を払う必要がありますが、特にブロックチェーンセキュリティのリスクの高い性質を考慮すると、経験的にその代償は妥当なものです。
TLA+ 言語自体を怖がる必要はありませんが、名前は威圧的ですが、その強力な機能にアクセスするのは非常に簡単です。実際、ほぼすべての TLA+ 機能を説明する TLA+ チート シートは、およそ 1 ページに収まります。
mbt.informal.systems/docs/tla_basics_tutorials/tla+チートシート.html
さらに、モデルの構築に必要な労力は、標準的な手動によるセキュリティ レビューに匹敵します。例えばckBTCミンターの場合、設計を理解し、初期モデルを作成し、プロパティを作成するまでに1人で合計3週間程度かかります。
結果として得られる TLA+ モデルは、コードよりも単純であることと、TLA+ の高レベルな性質の両方により、実装よりもはるかに単純です。 ckBTC ミンターのモデルには、Rust 実装の数千行に比べて、約 250 行のコードが必要です。おそらく驚くべきことに、作業の面で最も難しい部分の 1 つは、直感的な仕様にはギャップが見つかることがよくあるため、必要なプロパティを指定することです。
モデルが完成すると、自動的に解析（モデルチェック）が完了します。分析の実行には長時間かかる場合があります。たとえば、ckBTC の場合、完了までに 20 時間以上かかりました。最後に、TLA のもう 1 つの利点は、コードが実装される前の設計フェーズでモデリングと分析を実行できることです。これにより、後の設計エラーによる大規模なリファクタリングを排除できます。
TLA+ が役に立たない場合
マイナス面としては、TLA+ は、同時実行プログラムとは対照的に、複雑な逐次プログラムにはあまり役に立ちません。また、より便利な他のツール (Tamarin など) がある複雑な暗号化プロトコルの処理も苦手です。
最後に、TLA+ モデルと実際の実装の同期を保つという問題があります。実装コードは時間の経過とともに進化するため、モデルに準拠しなくなる可能性があり、ツールのサポートがなければこれを把握するのは困難です。
実際、私たちの研究開発チームはこの問題の解決に取り組んでいます。近いうちにいくつかのツールを皆さんと共有できることを願っています。
この概要を読んで、ご自身の重要なスマート コントラクトに TLA+ を使用することに興味を持っていただければ幸いです。そうであれば、続報をお待ちください。スマート コントラクトに TLA+ を使用する方法に関するより詳細なチュートリアルを含むフォローアップ投稿が近々公開される予定です。添付は、当社の研究開発チームが開発した実際の TLA+ モデルです。
気になるICコンテンツ
テクノロジーの進歩 | 世界的なイベント
IC Binance チャネルを収集してフォローする
最新情報を常に入手してください