前回の記事では、ゼロ知識証明(ZKP)システムの高度な形式検証、つまりZK命令を検証する方法について説明しました。各zkWasm命令を正式に検証することにより、zkWasm回路全体の技術的なセキュリティと正確性を完全に保証できます。この記事では、脆弱性発見の視点に焦点を当て、監査および検証プロセス中に特定された特定の脆弱性を分析し、そこから学んだ教訓について説明します。ZKPブロックチェーンの高度な形式検証に関する一般的な議論については、ZKPブロックチェーンの高度な形式検証に関する記事を参照してください。

ZKの脆弱性について説明する前に、まずCertiKがZKの正式な検証を実行する方法を理解しましょう。ZK仮想マシン(zkVM)のような複雑なシステムの場合、形式検証(FV)の最初のステップは、検証する必要がある内容とその特性を明確に定義することです。これには、ZKシステムの設計、コード実装、およびテストセットアップの包括的なレビューが必要です。このプロセスは通常の監査と重複しますが、レビュー後に検証目標とプロパティを確立する必要があるという点で異なります。CertiKでは、これを監査指向の検証と呼んでいます。通常、監査と検証の作業は統合されています。zkWasmでは、監査と形式検証の両方を同時に実施しました。

ZKの脆弱性とは?

ゼロ知識証明(ZKP)システムの中核的な特徴は、オフラインまたはプライベート(ブロックチェーントランザクションなど)で実行された計算の簡単な暗号化された証明をZKP検証機に転送できることです。検証者は、計算が主張どおりに行われたことを確認するために、証明をチェックして確認します。この文脈では、ZKの脆弱性により、ハッカーは偽のトランザクションのために偽造されたZKプルーフを提出し、ZKP検証者に受け入れられる可能性があります。

zkVM証明者の場合、ZK証明プロセスには、プログラムを実行し、各ステップの実行記録を生成し、これらの実行記録を一連の数値表に変換することが含まれます(「算術化」と呼ばれるプロセス)。これらの数値は、特定のテーブル セル間の関係、固定定数、テーブル間のデータベース ルックアップ制約、および隣接するテーブル行の各ペアが満たさなければならない多項式 (または「ゲート」) を含む一連の制約 (「回路」) を満たす必要があります。オンチェーン検証では、テーブル内の特定の番号を明らかにすることなく、すべての制約を満たすテーブルの存在を確認できます。

zkWasmの算術化表

各制約の精度は非常に重要です。制約にエラーがあると、それが弱すぎたり、欠落していたりして、ハッカーが誤解を招く証拠を提出する可能性があります。これらのテーブルは、スマートコントラクトの有効な実行を表しているように見えるかもしれませんが、実際にはそうではありません。従来のVMと比較すると、zkVMトランザクションの不透明性はこれらの脆弱性を増幅します。ZK以外のチェーンでは、トランザクション計算の詳細がブロックチェーンに公開されます。ただし、zkVMはこれらの詳細をオンチェーンに保存しません。この透明性の欠如により、攻撃の詳細や、攻撃が発生したかどうかさえ判断することが困難になります。

zkVM命令の実行ルールを強制するZK回路は、非常に複雑です。zkWasm の場合、ZK 回路の実装には 6,000 行を超える Rust コードと数百の制約が含まれます。この複雑さは、多くの場合、発見されるのを待っている複数の脆弱性が存在する可能性があることを意味します。

zkWasm 回路アーキテクチャ

実際、zkWasmの監査と正式な検証を通じて、そのような脆弱性がいくつか発見されました。以下では、代表的な2つの例を取り上げ、それらの違いについて検討します。

コードの脆弱性: Load8 データ インジェクション攻撃

1 つ目の脆弱性は、zkWasm の Load8 命令に関係します。zkWasm では、ヒープ メモリの読み取りは、一連の LoadN 命令を使用して実行されます (N はロードするデータのサイズです)。たとえば、Load64 は zkWasm メモリ アドレスから 64 ビット データを読み取る必要があります。Load8 は、メモリから 8 ビット データ (つまり、1 バイト) を読み取り、それを 0 で埋めて 64 ビット値を作成する必要があります。内部的には、zkWasm はメモリを 64 ビット バイトの配列として表すため、メモリ配列の一部を "選択" する必要があります。これは、4 つの中間変数 (u16_cells) を使用して行われ、これらが組み合わさって完全な 64 ビット負荷値を形成します。

これらのLoadN命令の制約は、次のように定義されます。

この拘束は、Load32、Load16、Load8 の 3 つのケースに分かれています。Load64 には、メモリ単位が正確に 64 ビットであるため、制約はありません。Load32 の場合、このコードでは、メモリ ユニットの上位 4 バイト (32 ビット) が 0 でなければならないことが確認されます。

Load16 の場合、このコードでは、メモリ ユニットの上位 6 バイト (48 ビット) が 0 でなければならないことが確認されます。

Load8 の場合、メモリ ユニットの上位 7 バイト (56 ビット) を 0 にする必要があります。残念ながら、これはコードには当てはまりません。

ご覧のとおり、上位 9 ビットから 16 ビットのみが 0 に制限されています。他の上位 48 ビットは任意の値にすることができ、"メモリからの読み取り" として渡されます。

この脆弱性を悪用すると、ハッカーは正当な実行シーケンスのZKプルーフを改ざんし、Load8命令にこれらの予期しないバイトをロードさせ、データ破損を引き起こす可能性があります。さらに、周囲のコードやデータを慎重に配置することで、誤った実行や転送を引き起こし、データや資産の盗難につながる可能性があります。これらの偽造されたトランザクションは、zkWasmチェッカーのチェックに合格し、ブロックチェーンによって正当なトランザクションとして誤って認識される可能性があります。

この脆弱性の修正は、実際には非常に簡単です。

この脆弱性は、コードの実装に起因し、ローカルのコードを少し変更することで簡単に修正できるため、「コードの脆弱性」と呼ばれるZKの脆弱性のクラスを表しています。ご想像のとおり、これらの脆弱性は比較的簡単に特定できます。

設計上の脆弱性 : 偽造リターン攻撃

別の脆弱性、今回はzkWasmの呼び出しと戻りに関する脆弱性を見てみましょう。呼び出しと戻りは、1つの実行中のコンテキスト(関数など)が別のコンテキストを呼び出し、呼び出し先が実行を完了した後に呼び出し元のコンテキストの実行を再開できるようにする基本的なVM命令です。各呼び出しは、後で戻ることを期待します。呼び出しと戻りのライフサイクル中に zkWasm によって追跡される動的データは、"呼び出しフレーム" と呼ばれます。zkWasm は命令を順番に実行するため、すべての呼び出しフレームは、実行時に発生する順序に基づいて順序付けできます。以下は、zkWasm で実行される呼び出し/戻りコードの例です。

ユーザーはbuy_token()関数を呼び出してトークンを購入できます(おそらく支払いまたは他の貴重なアイテムの転送によって)。その中核となるステップの1つは、add_token()関数を呼び出してトークンアカウントの残高を1増やすことです。ZK証明機自体はコールフレームのデータ構造をサポートしていないため、これらのコールフレームの完全な履歴を記録および追跡するには、実行テーブル(E-Table)とジャンプテーブル(J-Table)が必要です。

上の図は、buy_token()がadd_token()を呼び出し、add_token()からbuy_token()に戻るプロセスを示しています。トークンアカウントの残高が1つ増えていることがわかります。実行テーブルでは、各実行ステップが 1 行を占め、実行中の現在の呼び出しフレーム番号、現在のコンテキスト関数名 (説明のみ)、関数内で現在実行中の命令の番号、およびテーブルに格納されている現在の命令 (説明のみを目的としています) が含まれます。ジャンプ テーブルでは、各呼び出しフレームが 1 行を占め、呼び出し元フレームの番号、呼び出し元関数のコンテキスト名 (説明のみを目的として)、呼び出し元フレームの次の命令位置 (フレームが戻ることができるように) が格納されます。どちらのテーブルにも、現在の命令が呼び出し/戻りであるかどうか (実行テーブル内) と、そのフレームの呼び出し/戻り命令の合計数 (ジャンプ テーブル内) を追跡する "jops" 列があります。

予想どおり、各呼び出しには対応するリターンがあり、各フレームには 1 つの呼び出しと 1 つのリターンのみが必要です。上の図に示すように、ジャンプ テーブルの最初のフレームの "jops" 値は 2 で、実行テーブルの 1 行目と 3 行目の "jops" 値が 1 に相当します。現時点では、すべてが正常に見えます。

ただし、ここには問題があります: 1 回の呼び出しと 1 回のリターンではフレームの "jops" カウントが 2 に増えますが、2 回の呼び出しまたは 2 回のリターンでもカウントは 2 になります。フレームごとに 2 つの呼び出しや 2 つのリターンがあるのはばかげているように思えるかもしれませんが、これはまさにハッカーが期待を裏切ることによって行おうとすることだということを覚えておくことが重要です。

あなたは今興奮しているかもしれませんが、私たちは本当に問題を見つけましたか?

実行テーブルとジャンプテーブルの制約により、2つの呼び出しがフレームの同じ行にエンコードされないため、2つの呼び出しは新しいフレーム番号、つまり現在の呼び出しフレーム番号に1を加えたものが生成されるため、2つの呼び出しは問題になりません。

しかし、この状況は 2 つのリターンにとってそれほど幸運ではありません: リターン時に新しいフレームは作成されないため、ハッカーは正当な実行シーケンスの実行テーブルとジャンプテーブルを取得し、偽造されたリターン (および対応するフレーム) を注入する可能性があります。たとえば、buy_token() が add_token() を呼び出す前の実行テーブルとジャンプ テーブルの例は、ハッカーによって改ざんされて次のシナリオになる可能性があります。

ハッカーは、元の呼び出しと実行テーブルのリターンの間に2つの偽造されたリターンを挿入し、ジャンプテーブルに新しい偽造フレーム行を追加しました(実行テーブルの元のリターンとその後の命令実行ステップは4ずつインクリメントする必要があります)。ジャンプ テーブルの各行の "jops" カウントは 2 であるため、制約は満たされ、zkWasm プルーフ チェッカーは、この偽造された実行シーケンスの "プルーフ" を受け入れます。図からわかるように、トークンアカウントの残高は1倍ではなく3倍に増えます。したがって、ハッカーは1の価格で3つのトークンを取得できます。

この問題に対処するには、さまざまな方法があります。明白なアプローチの 1 つは、呼び出しと戻りを別々に追跡し、各フレームに 1 つの呼び出しと 1 つの戻りがあることを確認することです。

お気づきかもしれませんが、これまでのところ、この脆弱性に対するコードは 1 行も示されていません。主な理由は、問題のあるコード行がないことです。コードの実装は、テーブルと制約の設計と完全に一致しています。問題はデザイン自体にあり、修正も同様です。

この脆弱性は明らかなはずだと思うかもしれませんが、実際にはそうではありません。これは、「2 回の呼び出しまたは 2 回のリターンでも 2 の 'jops' カウントになる」と「2 回のリターンが実際に可能である」の間にギャップがあるためです。後者では、実行テーブルとジャンプテーブルのさまざまな制約を詳細かつ包括的に分析する必要があるため、完全な非公式推論を実行することは困難です。

2 つの脆弱性の比較

「Load8 データインジェクションの脆弱性」と「偽造リターンの脆弱性」はどちらも、ハッカーが ZK プルーフを操作し、偽のトランザクションを作成し、プルーフチェッカーを欺き、盗難やハイジャックを行う可能性があります。しかし、その性質や発見の仕方は大きく異なります。

「Load8 Data Injection Vulnerability」は、zkWasmの監査中に発見されました。これは簡単な作業ではなく、6,000 行を超える Rust コードと数十の zkWasm 命令で何百もの制約を確認する必要がありました。それにもかかわらず、脆弱性の検出と確認は比較的簡単でした。この脆弱性は正式な検証が始まる前に修正されたため、検証プロセス中には発生しませんでした。この脆弱性が監査中に発見されなかった場合は、Load8命令の検証中に発見されることが予想されます。

「偽造返品の脆弱性」は、監査後の正式な検証中に発見されました。監査中に検出できなかった理由の 1 つは、zkWasm には "mops" と呼ばれる "jops" に似たメカニズムがあり、zkWasm の実行中に各メモリ ユニットの履歴データに対応するメモリ アクセス命令を追跡していることです。モップ数の制約は、メモリ書き込みという 1 種類のメモリ命令のみを追跡し、各メモリ ユニットの履歴データは不変で 1 回だけ書き込まれる (モップ カウントは 1) ため、確かに正しいです。しかし、監査中にこの潜在的な脆弱性に気付いたとしても、実際には間違ったコード行は存在しないため、関連するすべての制約に関する厳密な形式的推論がなければ、考えられるすべてのシナリオを簡単に確認または除外することはできませんでした。

要約すると、これら2つの脆弱性は、それぞれ「コードの脆弱性」と「設計の脆弱性」のカテゴリに属します。コードの脆弱性は比較的単純で、発見しやすく (コードに欠陥がある)、推論や確認も容易です。設計の脆弱性は、非常に微妙で、発見が難しく(「欠陥のある」コードがない)、推論や確認が難しい場合があります。

ZKの脆弱性を発見するためのベストプラクティス

zkVMやその他のZKチェーンと非ZKチェーンを監査し、正式に検証した経験に基づいて、ZKシステムを保護する最善の方法についていくつかの提案を以下に示します。

コードと設計の確認

前述したように、ZKのコードとデザインの両方に脆弱性が含まれている可能性があります。どちらのタイプの脆弱性もZKシステムの整合性を損なう可能性があるため、システムを運用する前に対処する必要があります。ZKシステムの問題の1つは、非ZKシステムと比較して、計算の詳細が公開されていないか、チェーン上に保持されていないため、攻撃の検出と分析が困難であることです。その結果、ハッカー攻撃が発生したことは認識していても、それがどのように発生したかの技術的な詳細はわからない場合があります。これにより、ZKの脆弱性のコストが非常に高くなります。したがって、ZKシステムのセキュリティを事前に確保することの価値も非常に高いです。

監査と正式な検証の実施

ここで説明した2つの脆弱性は、監査と正式な検証によって発見されました。すべての脆弱性は正式な検証によって検出されるため、正式な検証だけでは監査の必要がなくなると考える人もいるかもしれません。ただし、両方を実行することをお勧めします。この記事の冒頭で説明したように、高品質のフォーマル検証作業は、コードと設計に関する徹底的なレビュー、検査、および非公式の推論から始まりますが、これは監査と重複します。さらに、監査中に単純な脆弱性を見つけて解決することで、正式な検証プロセスを簡素化および合理化できます。

ZKシステムの監査と形式検証の両方を実施する場合、最適なアプローチは両方を同時に実行することです。これにより、監査人とフォーマル検証エンジニアが効率的に連携できるようになり、フォーマル検証には高品質の監査入力が必要になるため、より多くの脆弱性を発見できる可能性があります。

ZKプロジェクトがすでに監査(称賛)または複数の監査(大きな称賛)を受けている場合は、以前の監査結果に基づいて回路で正式な検証を行うことをお勧めします。zkVMなどのプロジェクト(ZKと非ZKの両方)での監査と形式検証の経験から、形式検証では監査中に見落とされた脆弱性を捉えることが多いことが繰り返し示されています。ZKPの性質を考えると、ZKシステムは非ZKソリューションよりも優れたブロックチェーンセキュリティとスケーラビリティを提供するはずですが、そのセキュリティと正確性の重要度は、従来の非ZKシステムよりもはるかに高くなります。したがって、ZKシステムの高品質な形式検証の価値は、非ZKシステムの価値をはるかに上回ります。

回線とスマートコントラクトのセキュリティを確保

ZKアプリケーションは通常、回路とスマートコントラクトの2つのコンポーネントで構成されています。zkVMに基づくアプリケーションには、ユニバーサルzkVM回線とスマートコントラクトアプリケーションがあります。zkVMに基づかないアプリケーションの場合、アプリケーション固有のZK回線と、対応するスマートコントラクトがL1チェーンまたはブリッジのもう一方の端にデプロイされています。

zkWasm の監査および形式検証の取り組みには、zkWasm 回路のみが含まれます。しかし、ZKアプリケーションの全体的なセキュリティの観点からは、スマートコントラクトを監査し、正式に検証することも重要です。結局のところ、回路のセキュリティを確保するために多大な労力を費やした後、スマートコントラクトの精査の甘さがアプリケーションの侵害につながったとしたら、それは残念なことです。

特に注目に値するスマートコントラクトは2種類あります。最初のタイプは、ZKプルーフを直接処理します。規模は大きくないかもしれませんが、リスクは非常に高いです。2つ目のタイプは、zkVM上で実行される中規模から大規模のスマートコントラクトで構成されています。これらの契約は非常に複雑になることがあり、特にその実行の詳細がオンチェーンで表示されないため、最も価値のある契約は監査と検証を受ける必要があることを私たちは知っています。幸いなことに、何年にもわたる開発を経て、スマートコントラクトの正式な検証は現在実用的であり、適切な価値の高いターゲットに備えています。

形式検証(FV)がZKシステムとそのコンポーネントに与える影響を、以下の点でまとめてみましょう。

陳述：

1. この記事は[panewslab]から転載されており、著作権は原作者[CertiK]に帰属しますので、転載に異議がある場合は、Gate Learnチームに連絡していただければ、チームは関連する手順に従ってできるだけ早く処理します。

2. 免責事項:この記事で表明された見解や意見は、著者の個人的な見解を表しているにすぎず、投資アドバイスを構成するものではありません。

3. 記事の他の言語バージョンはGate Learnチームによって翻訳されており、 Gate.io で言及されていない場合、翻訳された記事を複製、配布、または盗用することはできません。