【テクニカル・上級編】 ZK-Rollupにおける回路(Circuit)のバグと健全性証明の偽造 – IoT・OT（制御システム） & ブロックチェーンセキュリティ防御ガイド

ZK-Rollup回路の暗号学的盲点：健全性証明偽造のメカニズムと形式検証による防衛網の構築

世の中の多くのブロックチェーンエンジニアは、ZK-Rollupを「数学的に絶対に破られない魔法の圧縮装置」だと勘違いしている。CZ（Changpeng Zhao）やVitalikがどれほどSNARKsの美しさを説こうとも、現実のコード――つまり、R1CS（Rank-1 Constraint Systems）やPlonkのカスタムゲートに落とし込まれた回路（Circuit）を記述するのは、生身の人間である。人間が書く以上、そこには必ずバグが宿る。

OT（制御システム）のPLCラダーロジックで安全インターロックをバイパスする配線を一本間違えればボイラーが爆発するように、ZK回路の制約（Constraints）を1つ書き損じれば、存在しない残高を無限に生み出す「論理的なショート」が起きる。L2のスマートコントラクト監査で表面上のSolidityコードだけを眺めているホワイトハッカーは、すでに周回遅れだ。今の最前線は、CircomやNoirのコード、そしてその先に広がる深淵なる多項式制約のバグとの戦いである。

今回は、ZK-Rollupの心臓部である「回路の論理欠陥」が生む健全性証明（Soundness）の偽造と、それに立ち向かうための形式検証（Formal Verification）のリアルな実装アプローチを解き明かしていく。

—

1. なぜZK回路は破られるのか：低レイヤの制約漏れとアンダークラシフィケーション

ZK-Rollupの根幹を支えるのは、「計算の正当性を短い証明（Proof）で検証する」というパラダイムだ。しかし、この「計算」を暗号学的な回路にマッピングする際、開発者は従来のプログラミング言語とは全く異なる思考を強いられる。

最大の罠が 「アンダークラシフィケーション（Under-constrained）」 である。

通常のプログラムでは、変数を宣言すれば勝手にメモリ領域が確保され、値が代入される。だが、Circomなどの回路言語において、明示的な制約（=== や制約演算子）をかけない限り、その変数は「何でも入れられる自由変数（Witnessの任意性）」として扱われる。攻撃者は、プルーフ生成時にこの自由変数に都合の良い値をねじ込むことで、不当な状態遷移を通る偽の証明を作り出す。

脆弱なCircom回路の典型例（パッと見で見抜けるか？）

以下のコードは、あるZK-Rollupのレイヤーで「指定された残高が、送金額以上であること」を検証しようとしたカスタムゲートの断片だ。

pragma circom 2.1.6;

include "../node_modules/circomlib/circuits/comparators.circom";

template CheckBalance() {
    // 入力信号
    signal input balance;
    signal input transferAmount;
    
    // 出力信号
    signal output isValid;

    // 内部シグナル（ここに罠がある）
    signal diff;

    // 残高から送金額を引く
    diff <== balance - transferAmount;

    // 比較器を使って、diffが非負（0以上）であることを確認しようとする
    // 注意: レンジプルーフが不完全な場合、diffが有限体の負の値（ラップアラウンド）になり得る
    component ge = GreaterEqThan(252);
    ge.in[0] <== balance;
    ge.in[1] <== transferAmount;

    isValid <== ge.out;
}

このコードのどこが致命的だろうか？
diff というシグナルは定義されているが、回路内で diff が正しく計算されていること（balance - transferAmount === diff）を強制する制約が抜けている（あるいは、有限体のフィールド演算におけるオーバーフローの考慮が漏れている）。悪意あるプロベータは、diff に全く無関係な魔術的な値を代入しつつ、Verifierを欺く証明を生成することが可能になる。これが健全性（Soundness）の崩壊、すなわち証明の偽造である。

—

2. 状態遷移の論理欠陥がもたらす致命的インシデント

実戦の現場では、このような回路のバグがL2全体の資金枯渇に直結する。よくある脆弱性のパターンを分類すると、以下の3つに集約される。

1. ゼロ知識の剥離（Over-constrainedによるDoS）: 必要以上に厳しい制約を課した結果、正当なトランザクションすら通らなくなる。
2. 非活性なビットの悪用（Unconstrained Bits）: 署名検証やMerkle木証明において、パディング領域や未使用のビットに対する制約が欠落しており、任意の不正データが「有効」と判定される。
3. Merkleパスのルート検証漏れ: ツリーの深さ（Depth）の検証や、リーフノードのインデックスが範囲内（Out-of-Bounds）であることのチェックが抜けているため、存在しない口座から資金を引き出せる。

特に恐ろしいのは、これらのバグがコンパイルエラーを1つも吐き出さない点だ。RustやSolidityのコンパイラとは異なり、ZKのコンパイラは「数学的に記述された通りの制約」を愚直にR1CSへ変換するだけである。ロジックの破綻は、コンパイル時には検知できない。

—

3. 防衛の要：形式検証（Formal Verification）による数学的担保

手動のコードレビューや単体テスト（WitnessTesterを用いたテストなど）だけでは、無限にある入力空間のパターンのうち、ごく一部しか検証できない。ここで登場するのが 形式検証（Formal Verification） である。

回路が「いかなる入力に対しても、意図しない状態遷移を許可しない」ことを数学的に証明するためには、SMT（Satisfiability Modulo Theories）ソルバーや、専用の検証ツールチェーンを導入する必要がある。

ここでは、HalmosやSymmetricなアプローチ、あるいはCircom向けの抽象解釈ツールを用いた検証の概念コードを示そう。Pythonなどのホスト言語から、Z3などのSMTソルバーを叩いて回路の健全性を検証するスクリプトのイメージだ。

from z3 import *

def verify_zk_circuit_logic():
    """
    Z3 SMTソルバーを用いて、ZK回路のカスタム制約に
    アンダークラシフィケーション（抜け穴）が存在しないかを検証するモックコード
    """
    # 有限体の素数フィールド（例: BN254のスカラーフィールドの簡易表現）
    FieldPrime = 21888242871839275222246405745257275088548364400416034343698204186575808495617

    # シンボリック変数として入力と内部シグナルを定義
    balance = Int('balance')
    transferAmount = Int('transferAmount')
    diff = Int('diff')

    s = Solver()

    # 1. 範囲制約の付与（フィールドのモジュロ演算を模倣）
    s.add(balance >= 0, balance < FieldPrime)
    s.add(transferAmount >= 0, transferAmount < FieldPrime)
    s.add(diff >= 0, diff < FieldPrime)

    # 2. 回路が本来満たすべき制約（但し、バグが含まれている状態を仮定）
    # バグ: diffの整合性を強制する制約 (balance - transferAmount == diff) がコメントアウトされているとする
    # したがって、s.add(balance - transferAmount == diff) はあえて追加しない。

    # 3. 攻撃者の目標: 「残高より多い金額を送金している（balance < transferAmount）」にもかかわらず、
    # isValid が True (1) と判定されるような入力の組み合わせ（バグの証拠）が存在するか？
    isValid = Bool('isValid')
    
    # 簡易的に、送金が成立してしまう条件を記述
    s.add(balance < transferAmount)
    
    # もし不整合な状態（健全性の破壊）が「充足可能（Satisfiable）」であれば、脆弱性が存在する
    if s.check() == sat:
        m = s.model()
        print("[!] 脆弱性を検出: 健全性証明が偽造可能です。")
        print(f"    -> 攻撃時の balance: {m[balance]}")
        print(f"    -> 攻撃時の transferAmount: {m[transferAmount]}")
        print(f"    -> 攻撃時の 自由変数 diff: {m[diff]}")
    else:
        print("[+] 回路の制約は健全です（脆弱性は検出されませんでした）。")

if __name__ == "__main__":
    verify_zk_circuit_logic()

このようなシンボリック実行（Symbolic Execution）やSMTソルバーを活用したアプローチにより、人間の認知限界を超えたエッジケースのバグを機械的に炙り出すことができる。

—

4. チーフホワイトハッカーが実践するZK-Rollup監査のチェックリスト

現場のテックリードやセキュリティアーキテクトが、L2/ZKプロジェクトのコードベースをレビューする際、真っ先に確認すべき核心的ポイントを以下に挙げる。

1. カスタムゲートとPlonk制約のオーバーフロー対策

  • ビット幅の検証（Range Checks）がすべての入力に対して完全に行われているか？ 特にカスタムガジェット（SHA-256やPoseidonハッシュ関数など）の内部で、オーバーフローが無視されていないか確認する。

2. 非ゼロチェック（Non-Zero Checks）の厳密性

  • 除算や逆元（Inverse）を計算する際、分母が 0 になるケースを完全に排除しているか。暗号学的プリミティブにおいて、ゼロ除算のハンドリングミスはそのままプルーフ生成のクラッシュ、あるいは偽造へと繋がる。

3. Public Inputs と Private Inputs のバウンダリー

  • 検証者（Verifierスマートコントラクト）側で受け取る Public Inputs が、回路内で改ざん不可能な形でコミットされているか。特に、L1からの入金キュー（Deposit Queue）やブリッジの状態を示すルートハッシュが、外部からの介入に対して強固に保護されているかを精査する。

4. アップグレードメカニズムとタイムロック

  • ZK-Rollupの検証用スマートコントラクト（Verifier Contract）が、マルチシグや単一のEOAによって勝手に差し替えられないガバナンス構造になっているか。回路自体をアップデートする際、古い証明と新しい証明の互換性で状態が矛盾しないかを確認する。

—

結びに代えて

ZK-Rollupのセキュリティは、ブロックチェーンのコンセンサス層を守る最後の砦だ。スマートコントラクトのハッキングが「資産の強奪」で済むのに対し、ZK回路の破綻は「システム全体の数学的信頼の崩壊」を意味する。

コードを書くときは、常に「この変数に最悪の数値をブッ込んだらどうなるか」という悪意ある視点を忘れてはならない。綺麗に動くコードではなく、数学的に裏切らないコードだけが、次の世代のWeb3インフラを生き残る。

スポンサーリンク

コメント

タイトルとURLをコピーしました