Exploiting Under-Constrained ZK Circuits

Zero-Knowledge (ZK) Circuits allow:

• Provers to make claims without revealing the private information they use to make those claims

• Verifiers to verify claims made by a Prover without having to trust the Prover or know any of the private information the Prover used to make their claims

ZK Properties

ZK systems have 3 important properties:

1. Completeness - given valid inputs, the Prover is able to generate valid Proofs which are accepted by the Verifier

2. Soundness - a malicious Prover is unable (in practice has a very low probability) to generate invalid / forged Proofs which will be accepted by the Verifier

3. Zero Knowledge - Private Inputs known by the Prover are not leaked and can’t be reverse engineered from the Proof or Public Inputs provided to the Verifier

ZK Vulnerabilities

Many vulnerabilities in ZK Circuits involve breaking one or more of these important properties; most circuit vulnerabilities can be categorized into 3 general categories:

1. Over-Constrained - a Prover is able to create a valid Proof but the Verifier is unable to verify it as the Circuit contains too many Constraints, breaking the "Completeness" property

2. Under-Constrained - a malicious Prover can create an invalid Proof which the Verifier subsequently verifies as the Circuit contains too few Constraints, breaking the "Soundness" property

3. Non-Zero Knowledge - the Private Inputs used by the Prover leak out or are able to be reverse-engineered by the Verifier or other observers, breaking the "Zero Knowledge" property

Vulnerable Circuit - "Is Not Prime"

Let's start off by creating a Circuit to prove that a number is not a prime number. To setup the repository use one of the Circom “starter” repositories which integrate Hardhat [1,2] for easier compilation & testing workflow. For this example we'll use the second link then:

• copy the 2-hardhat-integration into a new folder to be our project folder

• change the URL for ptau in hardhat.config.js to be ptau: "<https://hermez.s3-eu-west-1.amazonaws.com/powersOfTau28_hez_final_15.ptau>"

For simplicity we won’t create new files but simply edit already existing files; start by putting our example Circuit code inside circuits/multiplier.circom:

pragma circom 2.1.4;

// Prover uses Circuit `IsNotPrime` to prove that `val` is not 
// a prime number without revealing the private factors
// which the Prover knows and uses to prove this
template IsNotPrime() {
    signal input factorOne;
    signal input factorTwo;
    signal input val;

    // constraint: factors multipled result in val
    // will fail for prime numbers
    val === factorOne * factorTwo;
}

// `val` is public, factors are private
component main {public [val]} = IsNotPrime();

This Circuit:

• takes 1 Public Input val which is the number the Prover claims is not prime

• takes 2 Private Inputs factorOne and factorTwo which are secret inputs the Prover uses to assert their claim; these should never be leaked or otherwise disclosed to the Verifier or other observers

• contains 1 Constraint (using the === operator) which enforces that the multiplication of factorOne and factorTwo results in val - if this is true then val should not be prime

Next put the inputs inside circuits/multiplier.json:

{
    "val": 21,
    "factorOne": 3,
    "factorTwo": 7
}

Then put the test inside test/multiplier.test.js:

const hre = require("hardhat");
const { assert } = require("chai");

describe("multiplier circuit", () => {
  let circuit;

  const sampleInput = {
    val: "21",
    factorOne: "7",
    factorTwo: "3"
  };
  const sanityCheck = true;

  before(async () => {
    circuit = await hre.circuitTest.setup("multiplier");
  });

  it("produces a witness with valid constraints", async () => {
    const witness = await circuit.calculateWitness(sampleInput, sanityCheck);
    await circuit.checkConstraints(witness);
  });

  it("has expected witness values", async () => {
    const witness = await circuit.calculateLabeledWitness(
      sampleInput,
      sanityCheck
    );
    assert.propertyVal(witness, "main.val", sampleInput.val);
    assert.propertyVal(witness, "main.factorOne", sampleInput.factorOne);
    assert.propertyVal(witness, "main.factorTwo", sampleInput.factorTwo);
  });
});

Compile with yarn circom:dev and run the test with yarn test - everything passes and our Circuit appears to be working correctly!

Exploiting Under-Constrained Factors

Recall that the Circuit has only 1 Constraint: the product of both factors must equal the value being proved:

// constraint: factors multipled result in val
// will fail for prime numbers
val === factorOne * factorTwo;

However there are no Constraints on the possible values of factorOne and factorTwo; the Prover can set these to whatever they like. Could a malicious Prover abuse this to create a false Proof? It turns out the answer is yes.

A Prime Number is an unsigned integer which:

• is greater than 1

• cannot be written as a product of two smaller numbers which are themselves also greater than 1

Change sampleInput in test/multiplier.test.js to multiply the number being proved by 1:

  const sampleInput = {
    val: "7",
    factorOne: "1",
    factorTwo: "7"
  };

Then re-run the test suite using yarn test and everything passes - a malicious Prover was able to exploit the under-constraining of factorOne and factorTwo to create a false Proof which successfully verified the number 7 is not a prime number, which of course is incorrect as 7 is a prime number!

Constraining The Factors

As the Circuit is Under-Constrained we'll need to add additional Constraints to prevent factorOne and factorTwo from being equal to 1. In Solidity this would be relatively simple:

require(factorOne != 1 && factorTwo != 1);

However Circom Constraints must be Quadratic Equations so they can be easily used with the Rank One Constraint System (R1CS). Hence we must use some mathematical tricks to express require(x != 1) in a compatible form. To do this we will modify one math trick already in the circomlib library; put the new expanded Circuit into circuits/multiplier.circom:

pragma circom 2.1.4;

// slightly modified from
// https://github.com/iden3/circomlib/blob/master/circuits/comparators.circom#L24-L34
// math hack to implement `require(input != 1)`
// doesn't gracefully handle case where input == 0
// but that isn't required for this circuit
// as factors of 0 couldn't be used to create
// false proofs
template IsOne() {
    signal input in;
    signal output out;

    // intermediate signal
    signal inv;

    // store into `inv` intermediate signal:
    //   if input != 1 -> inv = 1/in
    // else input == 1 -> inv = 0
    inv <-- in != 1 ? 1/in : 0;

    // store and constrain `out` using a math trick that
    // will make the constraint at the end fail for input == 1
    //
    // case a) if input was 1 then inv = 0
    //         out <== -1 * 0 + 1
    //         out <== 1 (will make constraint at end fail)
    // case b) if input was 2 then inv = 1/2
    //         out <== -2*1/2 + 1
    //         out <== -1 + 1
    //         out <== 0
    out <== -in*inv + 1;

    // constraint prevents factors of 1
    // case a) if input was 1 then in = 1 and out = 1
    //         in*out = 1*1 = 1 -> constraint fails
    // case b) if input was 2 then in = 2 and out = 0
    //         in*out = 2*0 = 0 -> constraint passes
    in*out === 0;
}

// Prover uses Circuit `IsNotPrime` to prove that `val` is not 
// a prime number without revealing the private factors
// which the Prover knows and uses to prove this
template IsNotPrime() {
    signal input factorOne;
    signal input factorTwo;
    signal input val;

    // constraint: factors multiplied result in val
    // will fail for prime numbers
    val === factorOne * factorTwo;

    // prevent factorOne == 1
    component f1Check = IsOne();
    f1Check.in <== factorOne;

    // prevent factorTwo == 1
    component f2Check = IsOne();
    f2Check.in <== factorTwo;
}

// `val` is public, factors are private
component main {public [val]} = IsNotPrime();

After compiling again with yarn circom:dev, change the test sampleInputs inside test/multiplier.test.js to use different values for different runs to verify that the Prover can no longer create a false Proof by multiplying val by 1:

  // fails as factorOne == 1
  const sampleInput = {
    val: "21",
    factorOne: "1",
    factorTwo: "21"
  };

  // fails as factorTwo == 1
  const sampleInput = {
    val: "21",
    factorOne: "21",
    factorTwo: "1"
  };

  // succeeds as factorOne != 1 and
  //             factorTwo != 1 and
  //             factorOne * factorTwo == val
  const sampleInput = {
    val: "21",
    factorOne: "7",
    factorTwo: "3"
  };

  // fails as factorOne * factorTwo != val
  const sampleInput = {
    val: "21",
    factorOne: "7",
    factorTwo: "4"
  };

Our 2 additional Constraints and expanded test suite appears to have resolved the issue; a malicious Prover can no longer exploit the Circuit by having a prime number multiply itself by 1 to falsely prove it is not prime. However there is a much more subtle vulnerability still present..

Exploiting Modular Arithmetic Overflow In Finite Fields

ZK Circuits operate using Modular Arithmetic in a Finite Field Fp with a default value of p = 21888242871839275222246405745257275088548364400416034343698204186575808495617 though the value of p can be changed using the -p compilation option.

Due to Modular Arithmetic numbers wrap around; for simplicity consider p = 11 for a Finite Field F11. A Prover could then pass the following inputs to our "fixed" Circuit:

  const sampleInput = {
    val: "7",
    factorOne: "6",
    factorTwo: "3"
  };

When the Circuit executes, 6 * 3 = 18 wraps to 7 since 11 wraps to 0 due to Modular Arithmetic in F11 with p = 11 . A malicious Prover could exploit this overflow to create a false Proof that 7 is not a prime number! Hence the "fixed" Circuit still contains a critical and more subtle "Under-Constrained" vulnerability because there is no constraint on the range of inputs which operate using Modular Arithmetic within a Finite Field.

Range Constraints To Prevent Overflow

To handle the multiplication overflow from factorOne * factorTwo we'll need to constrain both factors such that their product is smaller than p of the Finite Field Fp. To achieve this we constrain each factor x in range 2 <= x < sqrt(p) ; in practice for Circom's default p we can use 2 <= x < 2 ** 100 but auditors must always be aware of which p value the Circuit they are auditing uses and the consequences this has for range constraints & overflow due to Modular Arithmetic.

For our updated solution we'll write a new InRange template to perform the range check leveraging some more math tricks from circomlib. This allows us to delete the previous Constraints enforcing factor != 1 as this is now handled by the range checks. Put the new complete code in circuits/multiplier.circom :

pragma circom 2.1.4;

// helpers taken from circomlib
template Num2Bits(n) {
    signal input in;
    signal output out[n];
    var lc1=0;

    var e2=1;
    for (var i = 0; i<n; i++) {
        out[i] <-- (in >> i) & 1;
        out[i] * (out[i] -1 ) === 0;
        lc1 += out[i] * e2;
        e2 = e2+e2;
    }

    lc1 === in;
}

template LessThan(n) {
    assert(n <= 252);
    signal input in[2];
    signal output out;

    component n2b = Num2Bits(n+1);

    n2b.in <== in[0]+ (1<<n) - in[1];

    out <== 1-n2b.out[n];
}

template LessEqThan(n) {
    signal input in[2];
    signal output out;

    component lt = LessThan(n);

    lt.in[0] <== in[0];
    lt.in[1] <== in[1]+1;
    lt.out ==> out;
}

template GreaterEqThan(n) {
    signal input in[2];
    signal output out;

    component lt = LessThan(n);

    lt.in[0] <== in[1];
    lt.in[1] <== in[0]+1;
    lt.out ==> out;
}

// written using circomlib helpers
// to enforce range constraints preventing
// overflow due to modular arithmetic
template InRange() {
    signal input a;
    signal input lowerbound;
    signal input upperbound;
    signal output out;

    // if lowerbound <= a <= upperbound return 1 else 0
    component lteCheck = LessEqThan(124);
    lteCheck.in[0] <== a;
    lteCheck.in[1] <== upperbound;

    component gteCheck = GreaterEqThan(124);
    gteCheck.in[0] <== a;
    gteCheck.in[1] <== lowerbound;

    out <== lteCheck.out * gteCheck.out;
}


// Prover uses Circuit `IsNotPrime` to prove that `val` is not 
// a prime number without revealing the private factors
// which the Prover knows and uses to prove this
template IsNotPrime() {
    signal input factorOne;
    signal input factorTwo;
    signal input val;

    // constraint: factors multiplied result in val
    // will fail for prime numbers
    val === factorOne * factorTwo;

    // Circom circuits: 
    // * operate in a Finite Field Fp where p is one of 
    //   several potential primes
    // * use Modular Arithmetic (mod p) such that
    //   p wraps back around to 0
    //
    // Consider simple case F11 so 11 wraps to 0, a Prover
    // could call this circuit with:
    // factorOne = 6
    // factorTwo = 3
    //       val = 7
    //
    // 6 * 3 = 18 which wraps to 7 due to mod 11
    // Hence the Prover could use this Circuit to
    // create a false proof that 7 is not prime
    // by exploiting overflow due to Modular Arithmetic
    //
    // To prevent overflow implement range check
    // constraints on the factors

    // {0, 1} not valid factors
    var MIN_RANGE = 2; 

    // must be below sqrt(p) for Fp, 2**100 works for default p
    // https://docs.circom.io/circom-language/basic-operators/#field-elements
    var MAX_RANGE = 2 ** 100;

    component f1RangeCheck = InRange();
    f1RangeCheck.a <== factorOne;
    f1RangeCheck.lowerbound <== MIN_RANGE;
    f1RangeCheck.upperbound <== MAX_RANGE;

    component f2RangeCheck = InRange();
    f2RangeCheck.a <== factorTwo;
    f2RangeCheck.lowerbound <== MIN_RANGE;
    f2RangeCheck.upperbound <== MAX_RANGE;

    // constraint to enforce factor range constraints
    1 === f1RangeCheck.out * f2RangeCheck.out;
}

// `val` is public, factors are private
component main {public [val]} = IsNotPrime();

While the factor range check Constraints prevent the overflow exploit, one necessary consequence to be aware of is that they also limit the range of numbers for which the Circuit can be used to prove a number is not a prime.

Additional Resources

Special thanks to rkm0959 and cergyk1337 for invaluable ZK insights and cyfrin.io for providing me with research time between audits to study and explore. Some helpful additional resources include:

• Taxonomy of ZK Vulns

• ZK Security Explained

• ZK Bug Tracker