二つのZK脆弱性を深く分析する

著者：CertiK

以前の記事では、ゼロ知識証明の先進的な形式的検証について、ZK命令をどのように検証するかを議論しました。各zkWasm命令を形式的に検証することで、私たちはzkWasm回路全体の技術的安全性と正確性を完全に検証することができます。本稿では、脆弱性を発見する視点に焦点を当て、監査と検証の過程で発見された具体的な脆弱性を分析し、そこから得られた経験と教訓を考察します。ゼロ知識証明（ZKP）ブロックチェーンの先進的な形式的検証に関する一般的な議論については、ゼロ知識証明ブロックチェーンの先進的な形式的検証に関する記事を参照してください。

ZKの脆弱性について議論する前に、CertiKがどのようにZKの形式的検証を行っているかを理解しましょう。ZK仮想マシン（zkVM）のような複雑なシステムに対して、形式的検証（FV）の最初のステップは、検証する内容とその性質を明確にすることです。これには、ZKシステムの設計、コード実装、テスト設定に対する包括的なレビューが必要です。このプロセスは通常の監査と重なる部分がありますが、異なる点は、レビュー後に検証の目標と性質を確立する必要があることです。CertiKでは、これを「検証指向の監査」と呼んでいます。監査と検証の作業は通常一体となっています。zkWasmに対しては、同時に監査と形式的検証を行いました。

ZKの脆弱性とは？

ゼロ知識証明システムの核心的な特徴は、オフラインまたはプライベートに実行された計算（例えばブロックチェーン取引）の短い暗号証明をゼロ知識証明検証者に渡し、それをチェックして確認することにより、その計算が宣言された通りに実行されたことを確信できることです。この点において、ZKの脆弱性は、ハッカーが虚偽の取引を証明するための偽造ZK証明を提出し、ZK証明検査者がそれを受け入れることを可能にします。

zkVMの証明器にとって、ZK証明プロセスはプログラムを実行し、各ステップの実行記録を生成し、その実行記録のデータを一連の数値表に変換すること（このプロセスは「算術化」と呼ばれます）を含みます。これらの数値は、一連の制約（すなわち「回路」）を満たさなければならず、その中には具体的な表のセル間の関連方程式、固定された定数、表間のデータベース検索制約、そして隣接する表行間で満たす必要のある多項式方程式（すなわち「ゲート」）が含まれています。オンチェーン検証は、すべての制約を満たす表が確かに存在することを確認でき、その具体的な数値を見ることはありません。

zkWasm算術化表

各制約の正確性は非常に重要です。制約のいずれかに誤りがあれば、たとえそれが弱すぎるものであっても、ハッカーが誤解を招く証明を提出できる可能性があり、これらの表は一見するとスマートコントラクトの有効な実行を表しているように見えますが、実際にはそうではありません。従来のVMと比較して、zkVM取引の不透明性はこれらの脆弱性を拡大します。非ZKチェーンでは、取引の計算の詳細はブロック上に公開されて記録されていますが、zkVMはこれらの詳細をチェーン上に保存しません。透明性の欠如は、攻撃の具体的な状況を特定することを難しくし、攻撃が発生したかどうかさえも判断が難しくなります。

zkVM命令規則を実行するZK回路は非常に複雑です。zkWasmの場合、そのZK回路の実装は6,000行以上のRustコードと数百の制約を含んでいます。この複雑さは、通常、複数の脆弱性が発見されるのを待っていることを意味します。

zkWasm回路アーキテクチャ

実際、私たちはzkWasmの監査と形式的検証を通じて、複数のそのような脆弱性を発見しました。以下では、2つの代表的な例について議論し、それらの違いについて考察します。

コード脆弱性：Load8データ注入攻撃

最初の脆弱性は、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ビット）がゼロであることを保証しています。

Load16の場合、メモリセルの上位6バイト（48ビット）がゼロである必要があります。

Load8の場合、メモリセルの上位7バイト（56ビット）がゼロであることが求められます。残念ながら、コードではそうなっていません。

ご覧の通り、上位9ビットから16ビットのみがゼロに制限されています。他の上位48ビットは任意の値でありながら、「メモリから読み取った」ように偽装することができます。

この脆弱性を利用することで、ハッカーは合法的な実行シーケンスのZK証明を改ざんし、Load8命令の実行がこれらの予期しないバイトを読み込むようにし、データの破損を引き起こすことができます。また、周囲のコードとデータを巧妙に配置することで、虚偽の実行と転送を引き起こし、データと資産を盗む可能性があります。この偽造された取引はzkWasm検査器の検査を通過し、ブロックチェーンによって誤って実際の取引として認識されることになります。

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

この脆弱性は「コード脆弱性」と呼ばれる一類のZK脆弱性を代表しています。なぜなら、これらはコードの記述に起因し、比較的小さな局所的なコード修正によって簡単に修正できるからです。あなたが同意するかもしれないように、これらの脆弱性は比較的見つけやすいです。

設計脆弱性：偽造戻り攻撃

次に、zkWasmの呼び出しと戻りに関する別の脆弱性を見てみましょう。呼び出しと戻りは基本的なVM命令であり、実行中のコンテキスト（例えば関数）が別のコンテキストを呼び出し、呼び出された側が実行を完了した後に呼び出し元のコンテキストの実行を復元することを可能にします。各呼び出しは、後で戻ることが期待されます。zkWasmで呼び出しと戻りのライフサイクル中に追跡される動的データは「呼び出しフレーム（call frame）」と呼ばれます。zkWasmは命令を順次実行するため、すべての呼び出しフレームは実行中の発生時間に基づいて並べ替えることができます。以下は、zkWasm上で実行される呼び出し/戻りコードの例です。

ユーザーはbuytoken()関数を呼び出してトークンを購入できます（おそらく支払いまたは他の価値のあるものを移転することによって）。その核心的なステップの1つは、addtoken()関数を呼び出すことによって、実際にトークンアカウントの残高を1増やすことです。ZK証明器自体は呼び出しフレームデータ構造をサポートしていないため、実行表（E-Table）とジャンプ表（J-Table）を使用して、これらの呼び出しフレームの完全な履歴を記録し追跡する必要があります。

上の図は、buytoken()がaddtoken()を呼び出す実行プロセスと、addtoken()からbuytoken()に戻るプロセスを示しています。トークンアカウントの残高が1増加したことがわかります。実行表では、各実行ステップが1行を占め、その中には現在の実行中の呼び出しフレーム番号、現在のコンテキスト関数名（ここでは説明のためのみ）、その関数内の現在の実行命令の番号、および表に保存されている現在の命令（ここでは説明のためのみ）が含まれています。ジャンプ表では、各呼び出しフレームが1行を占め、その中には呼び出し元フレームの番号、呼び出し元関数のコンテキスト名（ここでは説明のためのみ）、呼び出し元フレームの次の命令位置（そのフレームが戻ることができるように）があります。この2つの表には、現在の命令が呼び出し/戻りであるかどうかを追跡するjops列があり（実行表内）、そのフレームで発生した呼び出し/戻り命令の総数が記録されています（ジャンプ表内）。

人々が予想するように、各呼び出しには対応する戻りが必要であり、各フレームには1回の呼び出しと1回の戻りしかないはずです。上の図のように、ジャンプ表の第1フレームのjops値は2で、実行表の第1行と第3行に対応し、そこではjops値が1です。現時点ではすべてが正常に見えます。

しかし、実際には問題があります。1回の呼び出しと1回の戻りがフレームのjopsカウントを2にする一方で、2回の呼び出しまたは2回の戻りもカウントを2にする可能性があります。各フレームに2回の呼び出しまたは2回の戻りがあるのは奇妙に聞こえるかもしれませんが、ハッカーが期待を破るために正にそれを試みようとしていることを忘れないでください。

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

結果として、2回の呼び出しは問題ではありません。なぜなら、実行表と呼び出し表の制約により、2つの呼び出しを同じフレームの行にエンコードすることはできないからです。なぜなら、各呼び出しは新しいフレーム番号を生成し、つまり現在の呼び出しフレーム番号に1を加えたものになるからです。

しかし、2回の戻りのケースはそうはいきません。戻り時に新しいフレームが作成されないため、ハッカーは合法的な実行シーケンスの実行表と呼び出し表を取得し、偽造された戻り（およびそれに対応するフレーム）を注入することが可能です。例えば、以前の実行表と呼び出し表でbuytoken()がaddtoken()を呼び出す例は、ハッカーによって次のように改ざんされる可能性があります：

ハッカーは、実行表の元の呼び出しと戻りの間に2回の偽造された戻りを注入し、呼び出し表に新しい偽造されたフレーム行を追加しました（元の戻りとその後の命令の実行ステップ番号は実行表で4を加える必要があります）。呼び出し表の各行のjopsカウントが2であるため、制約条件を満たし、zkWasm証明検査器はこの偽造された実行シーケンスの「証明」を受け入れます。図からわかるように、トークンアカウントの残高が1回ではなく3回増加しました。したがって、ハッカーは1トークンの価格で3トークンを取得できるのです。

この問題を解決する方法はいくつかあります。明らかな方法は、呼び出しと戻りをそれぞれ個別に追跡し、各フレームに正確に1回の呼び出しと1回の戻りがあることを確認することです。

あなたはおそらく、これまでのところこの脆弱性のコードの行を一行も示していないことに気づいているでしょう。主な理由は、問題のある行がないためで、コード実装は表と制約の設計に完全に従っています。問題は設計自体にあり、修正方法も同様です。

あなたはこの脆弱性が明白であるべきだと思うかもしれませんが、実際にはそうではありません。なぜなら、「2回の呼び出しまたは2回の戻りもjopsカウントを2にする」ということと「実際に2回の戻りが可能である」ということの間にはギャップがあるからです。後者は、実行表と呼び出し表に関連するさまざまな制約を詳細かつ完全に分析する必要があり、完全な非形式的推論を行うのは難しいのです。

2つの脆弱性の比較

「Load8データ注入脆弱性」と「偽造戻り脆弱性」について、どちらもハッカーがZK証明を操作し、虚偽の取引を作成し、証明検査器を欺き、盗難や占有を行う可能性があります。しかし、それらの性質と発見の方法はまったく異なります。

「Load8データ注入脆弱性」は、zkWasmの監査中に発見されました。これは決して簡単なことではなく、6,000行以上のRustコードと数百のzkWasm命令の制約をレビューしなければならなかったからです。それにもかかわらず、この脆弱性は比較的容易に発見され、確認されました。この脆弱性は形式的検証が始まる前に修正されていたため、検証プロセス中には遭遇しませんでした。監査中にこの脆弱性が発見されなかった場合、Load8命令の検証中にそれを発見することが期待されます。

「偽造戻り脆弱性」は、監査後の形式的検証中に発見されました。監査中にそれを発見できなかった部分的な理由は、zkWasmにはjopsに非常に似たメカニズムである「mops」があり、zkWasmの実行中に各メモリセルの履歴データに対応するメモリアクセス命令を追跡します。mopsのカウント制約は正しいものであり、なぜならそれはメモリ書き込みという1種類のメモリ命令のみを追跡するからです。また、各メモリセルの履歴データは不変であり、一度だけ書き込まれます（mopsカウントは1）。しかし、監査中にこの潜在的な脆弱性に気づいても、すべての関連する制約に対して厳密な形式的推論を行わなければ、各種の可能性を容易に確認または排除することはできません。なぜなら、実際には問題のある行がないからです。

要約すると、これら2つの脆弱性はそれぞれ「コード脆弱性」と「設計脆弱性」に分類されます。コード脆弱性は比較的明白で、発見が容易（誤ったコード）であり、推論と確認が容易です。一方、設計脆弱性は非常に隠れやすく、発見が難しい（「誤った」コードがない）ため、推論と確認が難しいです。

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

私たちがzkVMおよび他のZKおよび非ZKチェーンの監査と形式的検証で得た経験に基づいて、ZKシステムを最もよく保護する方法についてのいくつかの提案を以下に示します：

コードと設計を確認する

前述のように、ZKのコードと設計には脆弱性が存在する可能性があります。この2種類の脆弱性は、ZKシステムが破壊される原因となる可能性があるため、システムが稼働する前に排除する必要があります。非ZKシステムと比較して、ZKシステムの問題の1つは、攻撃が公開されず、チェーン上に保持されないため、攻撃の詳細を明らかにし分析することが難しいことです。したがって、人々はハッキングが発生したことを知っているかもしれませんが、技術的にどのように発生したのかを知ることはできません。これにより、ZK脆弱性のコストが非常に高くなります。それに応じて、ZKシステムの安全性を事前に確保する価値も非常に高くなります。

監査と形式的検証を行う

ここで紹介した2つの脆弱性は、それぞれ監査と形式的検証を通じて発見されました。形式的検証を使用すれば監査は不要だと考える人もいるかもしれませんが、すべての脆弱性が形式的検証で発見されるわけではありません。実際、私たちの提案は両方を行うことです。本文の冒頭で説明したように、高品質の形式的検証作業は、コードと設計の徹底的なレビュー、チェック、および非公式な推論から始まります。この作業自体は監査と重なります。さらに、監査中により簡単な脆弱性を発見し排除することで、形式的検証がより簡単かつ効率的になります。

ZKシステムに対して監査と形式的検証の両方を行う場合、最適なタイミングはこの2つの作業を同時に行うことです。これにより、監査者と形式的検証エンジニアが効率的に協力でき（より多くの脆弱性を発見する可能性があります）、形式的検証の対象と目標には高品質の監査入力が必要です。

もしあなたのZKプロジェクトが監査を受けた（素晴らしい）または複数回監査を受けた（素晴らしい）場合、私たちの提案は、以前の監査結果に基づいて回路を形式的に検証することです。私たちのzkVMおよび他のZKおよび非ZKプロジェクトの監査と形式的検証の経験は、検証が監査中に見逃されがちな脆弱性を捕捉することが多いことを再三示しています。ZKPの特性により、ZKシステムは非ZKソリューションよりも優れたブロックチェーンの安全性とスケーラビリティを提供するべきですが、その安全性と正確性の重要性は従来の非ZKシステムよりもはるかに高いです。したがって、ZKシステムに対する高品質の形式的検証の価値は、非ZKシステムよりもはるかに高いのです。

回路およびスマートコントラクトの安全性を確保する

ZKアプリケーションは通常、回路とスマートコントラクトの2つの部分で構成されています。zkVMベースのアプリケーションには、一般的なzkVM回路とスマートコントラクトアプリケーションがあります。非zkVMベースのアプリケーションには、アプリケーション固有のZK回路と、L1チェーンまたはブリッジの反対側にデプロイされたスマートコントラクトがあります。

私たちのzkWasmの監査と形式的検証作業は、zkWasm回路にのみ関与しています。ZKアプリケーションの全体的な安全性の観点から、スマートコントラクトの監査と形式的検証も非常に重要です。結局のところ、回路の安全性を確保するために多くの努力を注いだ後、スマートコントラクトの面で警戒を緩め、アプリケーションが最終的に損害を受けることは非常に残念です。

特に注意すべき2種類のスマートコントラクトがあります。1つ目は、ZK証明を直接処理するスマートコントラクトです。これらは規模が小さいかもしれませんが、リスクは非常に高いです。2つ目は、zkVM上で実行される中規模から大規模のスマートコントラクトです。これらは時に非常に複雑であり、その中で最も価値のあるものは監査と検証を受けるべきです。特に、実行の詳細をチェーン上で見ることができないためです。幸いなことに、数年の発展を経て、スマートコントラクトの形式的検証は実用的になり、適切な高価値のターゲットに対して準備が整っています。

以下の説明を通じて、形式的検証（FV）がZKシステムおよびそのコンポーネントに与える影響をまとめましょう。