【テクニカル・上級編】 ZK-Rollupの回路設計における算術演算のオーバーフロー脆弱性 – IoT・OT（制御システム） & ブロックチェーンセキュリティ防御ガイド

ZK-Rollupの「算術の奈落」：回路設計におけるオーバーフローが招く証明の崩壊

SCADAシステムのラダーロジックを逆アセンブルして物理的なバルブ制御をハックしていた時代から、私たちは「境界値」という概念を物理的な電圧値と照らし合わせてきた。しかし、今の戦場はレイヤー2、それもZK-Rollupの回路（Circuit）という抽象的な数学空間だ。

現在、多くのエンジニアがZKの実装に飛び込んでいるが、彼らの大半は「算術回路は普通のプログラミングとは違う」という事実を軽視している。今日は、ZK-Rollupの心臓部である制約システム（Constraint System）における、数値オーバーフローという「静かなる爆弾」について深掘りしよう。

1. 算術回路における「オーバーフロー」の定義の変容

従来のCPUアーキテクチャでは、uint256のオーバーフローは単なるフラグの書き換えやラップアラウンドに過ぎない。しかし、ZK回路、特にR1CS（Rank-1 Constraint System）やPLONKishな制約系において、オーバーフローは「計算の不整合」ではなく「証明可能な偽」を生み出す種になる。

ZK回路は有限体（Finite Field）上で行われる。多くの証明系では素数 p を法として計算される。もし回路内で a + b を計算する際、その結果が p を超えてしまうと、剰余演算によって値が期待値から乖離する。これが単なるバグであれば「証明が失敗する」だけで済むが、攻撃者はこの「剰余によって値が小さくなる」性質を悪用し、残高の偽造や不正な状態遷移を引き起こす。

2. 脆弱性の解剖：制約が甘い回路の末路

以下は、ある仮想的なZK回路（Circom風の疑似コード）における、アンダーフローを許容してしまった脆弱なロジックの例だ。

// 脆弱な残高引き出し回路
template Withdraw() {
    signal input balance;
    signal input amount;
    signal output new_balance;

    // ここに range check がないことが致命的
    // amount > balance であれば、負の数が素数 p の補数として解釈される
    new_balance <== balance - amount; 
    
    // この制約が「値が正であること」を保証していない
    // 攻撃者は極めて大きな amount を指定することで、
    // new_balance を巨大な数値（アンダーフローした状態）に設定できる
}

このコードの根本原因は、new_balance が有効な範囲（例：0 から 2^64 - 1）に収まっていることを証明するRange Checkを怠っている点にある。

攻撃シナリオ：証明の錬金術

1. 攻撃者は balance が 100 の状態で、amount を 101 に設定する。
2. 回路内部では 100 - 101 が計算され、有限体の世界では p - 1 という極めて大きな数値にラップアラウンドする。
3. この「不正な巨大数値」を検証器（Verifier）が「有効な新残高」として受け入れてしまう。
4. 結果、攻撃者は実質的な負債を抱えるどころか、システム上の残高を最大値付近まで改ざんすることに成功する。

3. 防衛アーキテクチャ：堅牢な制約の設計

この脆弱性を封じるには、回路のすべての入力信号に対して「ビット幅の制約」を課す必要がある。circomlib 等の Num2Bits を活用し、値が期待される範囲内にあることを制約として記述しなければならない。

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

// 修正版：Range Check を組み込んだロジック
template SafeWithdraw(n) {
    signal input balance;
    signal input amount;
    signal output new_balance;

    // amount が n ビット以内であることを制約する
    component n2b = Num2Bits(n);
    n2b.in <== amount;

    // balance - amount が負にならないことを保証する制約
    // ここで比較演算子 (GreaterEqThan) を使用し、
    // 0 <= balance - amount を強制する
    component geq = GreaterEqThan(n);
    geq.a <== balance;
    geq.b <== amount;
    geq.out === 1; // 制約が満たされない場合、証明生成は失敗する

    new_balance <== balance - amount;
}

4. セキュリティリサーチャーの視点：監査の盲点

私が監査を行う際、必ず確認するのは「制約の数」ではなく「制約の漏れ」だ。特に以下のポイントを注視する。

入力の正規化: 外部から入力される信号が、有限体の最大値を超えていないか？（input < p は暗黙の了解だが、ロジック上での妥当性は別だ）
非決定論的な演算: 回路内で特定のビット操作を行う際、そのビットが期待する範囲外の入力を受け取った場合に、検証器がどのように振る舞うか？
耐量子暗号への移行期における検証コスト: 今後、STARKsベースのシステムへ移行する際、ハッシュ関数（Poseidon等）の制約が複雑化する。その際の「中間値のオーバーフロー」は、従来のECDSAベースとは異なる攻撃ベクトルを生むだろう。

結論：コードは数学である

ZK-Rollupのセキュリティは、もはや「コードのバグ」を探す仕事ではない。それは「制約の集合体が、いかに現実世界の整合性を維持しているか」を証明する数学的闘争だ。

スマートコントラクトの脆弱性が「金銭の流出」を招くなら、回路の脆弱性は「数学的真実の汚染」を招く。一度改ざんされた状態がブロックチェーンに刻まれれば、修正は不可能だ。我々アーキテクトは、常に「すべての値は、意図しない値になり得る」という前提に立ち、厳密なレンジチェックと制約の多重化を実装しなければならない。

次回の監査では、君の回路が「数学的に正しく、かつ悪意を許容しないか」を改めて問い直してほしい。泥臭い検証の積み重ねこそが、この不確実なWeb3の荒野を生き残る唯一の術なのだから。