In your storage: exploring ethereum, solidity & smart contract security

Exploiting Under-Constrained ZK Circuits

Under-constrained Zero-Knowledge Circuits are ripe for exploitation..

PublishedJuly 1, 2024

•11 min read•View as Markdown

Dacian

trust nothing, verify everything

Part of seriesDeep Dives

Comments (1)

Join the discussion

Juliana Cox2y ago

In March 2024, I found myself facing a bad scenario that many in the cryptocurrency space dread – falling victim to a phishing scam and losing a substantial amount of Bitcoin, totaling around $300,000. It was a devastating blow, one that left me feeling helpless and betrayed by the very technology I had come to trust. However, amidst the despair, a glimmer of hope emerged in the form of Digital Hack Recovery. In the attack, I was determined to learn from my mistake and take proactive measures to prevent such incidents from happening again. I delved into the world of cryptocurrency security, absorbing every piece of information I could find to arm myself against future threats. It was during this research phase that I came across Digital Hack Recovery, a name that would soon become synonymous with salvation. What struck me initially about Digital Hack Recovery was their emphasis on education and awareness. They understood that ignorance was often the greatest vulnerability in the crypto space and sought to empower their clients with the knowledge to mitigate risks effectively. Their website was a treasure trove of resources, offering comprehensive guides on security best practices, common scams to watch out for, and steps to take in the event of a breach. It was evident that they were not just a recovery service but a beacon of guidance in a sea of uncertainty. Upon reaching out to Digital Hack Recovery, I was met with a level of expertise that immediately put me at ease. Unlike other recovery platforms I had encountered, they took the time to assess my case thoroughly before committing to any action. Their transparency was refreshing – they made it clear from the outset what the likelihood of success was and what steps would be involved in the recovery process. This level of honesty instilled confidence in their capabilities and gave me hope that all was not lost. Throughout the recovery journey, Digital Hack Recovery maintained clear and open communication, providing regular updates on their progress and patiently answering any questions or concerns I had along the way. Their dedication to customer satisfaction was evident in every interaction, and it was clear that they genuinely cared about restoring not just my funds but also my peace of mind. In the end, Digital Hack Recovery delivered on its promise, managing to recover approximately 80% of the funds I had lost to the scam. While the financial aspect was certainly significant, it was the sense of closure and justice that proved to be the most valuable takeaway. Thanks to their expertise and perseverance, I was able to reclaim a portion of what was rightfully mine and move forward with renewed confidence in the crypto landscape. I cannot recommend Digital Hack Recovery highly enough to anyone who finds themselves in a similar predicament. Their commitment to education, transparency, and customer satisfaction sets them apart as a beacon of hope in an otherwise tumultuous industry. While the scars of my ordeal may never fully heal, knowing that there are professionals like Digital Hack Recovery standing ready to assist brings a sense of comfort and reassurance that is truly priceless. Trusting them with my recovery was undoubtedly one of the best decisions I have ever made, and I am eternally grateful for their unwavering support. Their contact;

WhatsApp +19152151930

Email; digital hack recovery @ techie . com

Deep Dives

Part 7 of 20

Deep dives on vulnerability classes exploited in real-world smart contract attacks

Up next

Solidity Inline Assembly Vulnerabilities

Using assembly to save gas can introduce memory corruption and other subtle vulnerabilities..

More from this blog

Using Claude To Evolve Specialist AI Smart Contract Auditors

In recent times a number of web3 security companies have begun offering paid “AI Smart Contract Auditor” services. These services commonly require clients to upload code to a website and after paying a fee, receive an AI-generated audit report. A muc...

Jul 4, 20257 min read

The Yieldoor Gas Optimizoor

Learn to write gas-efficient Solidity code using a real-world example!

Mar 17, 202515 min read

DeFi Liquidation Vulnerabilities

Liquidation code can contain subtle bugs and vulnerabilities..

Jan 23, 202528 min read

Find Highs Before External Auditors Using Certora Formal Verification

At DeFi Security Summit 2024 I presented a workshop on how smart contract developers can use invariant fuzz testing to find high severity issues prior to external audit, based on my real-world experience doing private audits with Cyfrin. Since fuzz t...

Nov 29, 202426 min read

Find Highs Before External Auditors Using Invariant Fuzz Testing

Many high severity findings found during private audits by external auditors could have been found by the protocol developers themselves using invariant fuzz testing prior to engaging external auditors. While this doesn’t require developing an “attac...

Nov 10, 202414 min read

In your storage: exploring ethereum, solidity & smart contract security

24 posts

deep diving smart contract security

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:

Completeness - given valid inputs, the Prover is able to generate valid Proofs which are accepted by the Verifier
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
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:

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
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
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:

Command Palette