ゼロ知識証明の高度な形式化検証：2つのZK脆弱性の詳細分析

2024.05.30

共有先

TechFlow厳選深潮セレクト

ゼロ知識証明の高度な形式化検証：2つのZK脆弱性の詳細分析

本稿では、脆弱性を発見する観点に注目し、監査および検証プロセスで発見された具体的な脆弱性と、そこから得られた経験や教訓について分析する。

2024.05.30 - 08:47:42

Web3業界の深掘り報道に専念し潮流を洞察

執筆：CertiK

前回の記事では、ゼロ知識証明（ZKP）における高度な形式化検証、すなわちZK命令1つ1つをどう検証するかについて説明しました。zkWasmの各命令を形式的に検証することで、zkWasm回路全体の技術的セキュリティと正しさを完全に保証できます。本稿では、脆弱性発見の観点から、監査および検証プロセス中に発見された具体的な脆弱性とそこから得られた教訓について分析します。ゼロ知識証明ブロックチェーンに関する高度な形式化検証の一般的な議論については、「ゼロ知識証明ブロックチェーンの高度な形式化検証」をご参照ください。

ZKの脆弱性について議論する前に、まずCertiKがどのようにZKの形式化検証を行うかを理解しましょう。zk仮想マシン（zkVM）のような複雑なシステムにおいて、形式化検証（FV）の第一歩は、何を検証し、どのような性質を保証すべきかを明確にすることです。これには、ZKシステムの設計、コード実装、テスト設定に対する包括的なレビューが必要です。このプロセスは従来の監査と一部重なりますが、異なるのは、レビュー後に検証の目的と性質を明確に定めることです。CertiKではこれを「検証志向監査」と呼んでいます。監査と検証作業は通常一体のものであり、zkWasmの場合も、監査と形式化検証を同時に行いました。

ZK脆弱性とは何か？

ゼロ知識証明システムの核心的特徴は、オフラインまたはプライベートに実行された計算（例：ブロックチェーン取引）の短い暗号化証明を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バイト）のデータを読み出し、64ビットの値を作るためにゼロで前方埋め（prefix padding）を行います。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チェックを通過し、ブロックチェーン上で誤って正当な取引と認識されます。

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

この脆弱性は「コード脆弱性」と呼ばれるタイプに属しており、コードの記述に由来し、局所的な小さなコード修正で容易に修復できます。おそらくご同意いただけるでしょうが、こうした脆弱性は比較的発見しやすいものです。

設計脆弱性：偽返却攻撃

別の脆弱性を見てみましょう。今度はzkWasmの呼び出し（call）と返却（return）に関するものです。呼び出しと返却は基本的なVM命令で、ある実行コンテキスト（例：関数）が別の関数を呼び出し、呼び出された側の実行が終了後に元のコンテキストの実行を再開できるようにします。すべての呼び出しは、後ほど対応する返却が行われることが期待されます。zkWasmは呼び出しと返却のライフサイクルで追跡する動的データを「コールフレーム（call frame）」と呼びます。zkWasmは命令を順次実行するため、すべてのコールフレームは実行時間順に並べられます。以下は、zkWasm上で動作する呼び出し／返却コードの例です。

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

上図は、buy_token()がadd_token()を呼び出し、その後add_token()からbuy_token()へ戻る過程を示しています。トークンアカウントの残高が1増加しているのがわかります。E-Tableでは、各行が1つの実行ステップを占め、現在のコールフレーム番号、現在のコンテキスト関数名（ここでの説明用）、その関数内での現在の命令番号、および現在の命令（説明用）を含みます。J-Tableでは、各行が1つのコールフレームを表し、呼び出し元フレーム番号、呼び出し元関数名（説明用）、呼び出し元フレームの次の命令位置（返却先）を保持します。両テーブルとも、jops列があり、これは現在の命令が呼び出し／返却かどうか（E-Table）およびそのフレームでの呼び出し／返却命令の総数（J-Table）を追跡します。

予想される通り、各呼び出しには対応する返却が1回ずつあり、各フレームには呼び出しと返却がそれぞれ1回ずつあるべきです。上図では、J-Tableのフレーム1のjops値は2であり、E-Tableの行1と行3のjops値1と一致しています。現時点では正常に見えます。

しかし、実は問題があります。1回の呼び出しと1回の返却でjopsカウントが2になりますが、2回の呼び出し、あるいは2回の返却でもカウントは2になります。1つのフレームに2回の呼び出しや2回の返却があるというのは馬鹿げているように思えますが、ハッカーがまさにその「想定外」を達成しようとしていることを忘れてはいけません。

もう少し興奮してきたでしょうか。本当に問題を見つけたのでしょうか？

結論から言えば、2回の呼び出しは問題になりません。なぜなら、E-TableとJ-Tableの制約により、同じフレームに行に2つの呼び出しをエンコードできないからです。なぜなら、各呼び出しは新しいフレーム番号（現在の+1）を生成するためです。

しかし、2回の返却はそうではありません。返却時には新しいフレームは作成されないため、ハッカーは正当な実行シーケンスのE-TableとJ-Tableを取得し、偽の返却（および対応するフレーム）を注入できるのです。前述のbuy_token()がadd_token()を呼び出す例は、次のように改ざんできます。

ハッカーは、E-Tableの元の呼び出しと返却の間に2回の偽返却を挿入し、J-Tableに新しい偽フレームを追加します（元の返却以降のステップの行番号はE-Tableで+4される）。J-Tableの各行のjopsカウントがいずれも2であるため、制約は満たされ、zkWasm証明チェッカーはこの偽実行シーケンスの「証明」を受け入れます。図からわかるように、トークン残高は1回ではなく3回増加しています。つまり、ハッカーは1トークンの支払いで3トークンを手に入れることができます。

この問題を解決する方法はいくつかあります。明らかな方法の一つは、呼び出しと返却を別々に追跡し、各フレームに呼び出しと返却がそれぞれちょうど1回ずつあることを保証することです。

すでにお気づきかもしれませんが、この脆弱性に関しては、一行のコードも提示していません。主な理由は、どのコードにも問題がないからです。コードの実装はテーブルと制約の設計に完全に準拠しています。問題は設計自体にあり、修正も設計レベルで必要です。

この脆弱性は明らかだと感じるかもしれませんが、実際にはそうではありません。「2回の呼び出しや返却でjopsが2になる」と「実際に2回の返却が可能であること」の間にはギャップがあります。後者は、E-TableとJ-Tableに関連するすべての制約を詳細かつ完全に分析する必要があり、非形式的な推論では完全に把握するのは困難です。

2つの脆弱性の比較

「Load8データ注入脆弱性」と「偽返却脆弱性」は、いずれもハッカーがZK証明を操作し、偽取引を作成して証明チェッカーを騙し、窃取や乗っ取りを行うことを可能にします。しかし、その性質と発見方法は大きく異なります。

「Load8データ注入脆弱性」は、zkWasmの監査中に発見されました。これは決して簡単な作業ではなく、6,000行以上のRustコードと数百の制約を精査する必要がありました。それでも、この脆弱性は比較的発見・確認しやすいものでした。この脆弱性は形式化検証開始前に修正されたため、検証プロセスでは遭遇しませんでした。もし監査中に見逃されていた場合、Load8命令の検証中に発見できたでしょう。

一方、「偽返却脆弱性」は監査後の形式化検証中に発見されました。監査中に見つけられなかった理由の一つは、zkWasmにはjopsと非常によく似た「mops」という機構があることです。mopsは、実行中に各メモリユニットの履歴に対応するメモリアクセス命令を追跡します。mopsのカウント制約は正しく機能しています。なぜなら、mopsはメモリ書き込みという一種類の命令のみを追跡し、各メモリユニットの履歴データは不変で、一度しか書き込まれない（mopsカウント=1）からです。しかし、監査中にこの潜在的脆弱性に気付いていたとしても、すべての関連制約に対して厳密な形式的推論を行わなければ、あらゆる可能性を簡単に確認または排除することはできません。実際、コードのどこにも「誤った」行は存在しないからです。

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

ZK脆弱性発見のベストプラクティス

我々がzkVMおよび他のZK・非ZKチェーンの監査と形式化検証で得た経験に基づき、ZKシステムを最適に保護するための提言を以下に示します。

コードと設計の両方をチェックする

前述の通り、ZKのコードと設計の両方に脆弱性が存在する可能性があります。これら2種類の脆弱性はいずれもZKシステムを破綻させる可能性があるため、システム稼働前にそれらを排除する必要があります。非ZKシステムと比べ、ZKシステムの問題点は、攻撃がより露見・分析しにくいことにあると言えます。計算の詳細が公開されず、チェーン上にも保存されないため、ハッキングが発生したことはわかっていても、技術的にどのように起きたのかわからないことがあります。このため、ZK脆弱性のコストは非常に高くなります。その分、事前にZKシステムの安全性を確保する価値も非常に高いのです。

監査と形式化検証の両方を行う

ここで紹介した2つの脆弱性は、それぞれ監査と形式化検証によって発見されました。形式化検証を行えば監査は不要だと考える人もいるかもしれませんが、実際には両方を行うことをお勧めします。冒頭で説明した通り、高品質な形式化検証は、コードと設計の徹底的なレビュー、検査、非形式的推論から始まり、この作業自体が監査と重複します。また、監査中により単純な脆弱性を発見・排除しておくことで、形式化検証がよりシンプルかつ効率的になります。

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

すでにZKプロジェクトの監査を完了している場合（素晴らしい！）、あるいは複数回の監査を完了している場合（非常に素晴らしい！）、その結果を基に回路の形式化検証を行うことをお勧めします。zkVMおよび他のZK・非ZKプロジェクトにおける我々の経験から繰り返し明らかになっているのは、検証が監査で見逃されがちな脆弱性を捉えることが多いということです。ZKPの特性上、ZKシステムは非ZKソリューションよりも優れたブロックチェーンのセキュリティとスケーラビリティを提供すべきですが、そのシステム自体の安全性と正しさの重要度は、従来の非ZKシステムよりもはるかに高いと言えます。したがって、ZKシステムに対する高品質な形式化検証の価値も、非ZKシステムよりもはるかに高いのです。

回路とスマートコントラクトの両方の安全を確保する

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

我々のzkWasmの監査および形式化検証作業は、zkWasm回路に限定されていました。しかし、ZKアプリケーション全体のセキュリティの観点からは、スマートコントラクトに対する監査および形式化検証も極めて重要です。回路の安全性に多大な努力を注いだ後で、スマートコントラクトの面で油断してアプリが被害を受けるのは、非常に残念なことです。

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

以下に、形式化検証（FV）がZKシステムおよびその構成要素に与える影響を要約します。