🌳Dark Forest v0.3: Missing Bit Length Check

Book an audit with Zokyo

Summary

Related Vulnerabilities: 1. Under-constrained Circuits, 2. Nondeterministic Circuits, 3. Arithmetic Over/Under Flows, 4. Mismatching Bit Lengths

Identified By: Daira Hopwood

A RangeProof circuit was used to prevent overflows. However, it used the CircomLib LessThan circuit to ensure this, which expects a maximum number of bits for each input. The inputs did not have any constraints on the number of bits, so an attacker could use large numbers to achieve a successful RangeProof even though the number was out of range.

Background

Dark Forest,, had a missing bit length check from its early circuits. In order to prevent underflows their circuit included a RangeProof template to ensure that an input is within bounds to prevent an overflow.

// From darkforest-v0.3/circuits/range_proof/circuit.circom
template RangeProof(bits, max_abs_value) {
    signal input in;

    component lowerBound = LessThan(bits);
    component upperBound = LessThan(bits);

    lowerBound.in[0] <== max_abs_value + in;
    lowerBound.in[1] <== 0;
    lowerBound.out === 0

    upperBound.in[0] <== 2 * max_abs_value;
    upperBound.in[1] <== max_abs_value + in;
    upperBound.out === 0
}

The LessThan template compares two inputs, and outputs 1 if the first input is less than the second input. In the RangeProof circuit, the LessThan circuit is essentially used as a GreaterEqThan, requiring that the output is 0. The LessThan template takes in the max number of bits for both inputs as a parameter, but does not actually check this constraint.

// From circomlib/circuits/comparators.circom
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];
}

The Vulnerability

Therefore, in the RangeProof example the LessThan circuit is used with an expected maximum number of bits, but the inputs max_abs_value and in are never constrained to that number. An attacker could input max_abs_value and in values that contain more bits than the expected max. Since LessThan is expecting the two inputs to have a maximum number of bits, it may output an incorrect result. An attacker would be able to satisfy the RangeProof even though the input is out of range.

The Fix

In order to prevent this attack, a check was needed on the number of bits of max_abs_value and in. They must be constrained to *bits *****(the template input parameter) number of bits. The following is the implemented fix in production:

// From darkforest-eth/circuits/range_proof/circuit.circom

// NB: RangeProof is inclusive.
// input: field element, whose abs is claimed to be <= than max_abs_value
// output: none
// also checks that both max and abs(in) are expressible in `bits` bits
template RangeProof(bits) {
    signal input in;
    signal input max_abs_value;

    /* check that both max and abs(in) are expressible in `bits` bits  */
    component n2b1 = Num2Bits(bits+1);
    n2b1.in <== in + (1 << bits);
    component n2b2 = Num2Bits(bits);
    n2b2.in <== max_abs_value;

    /* check that in + max is between 0 and 2*max */
    component lowerBound = LessThan(bits+1);
    component upperBound = LessThan(bits+1);

    lowerBound.in[0] <== max_abs_value + in;
    lowerBound.in[1] <== 0;
    lowerBound.out === 0

    upperBound.in[0] <== 2 * max_abs_value;
    upperBound.in[1] <== max_abs_value + in;
    upperBound.out === 0
}

Conclusion

1. The Problem with RangeProof:

   • The RangeProof circuit's goal is to ensure that a given input number (let's call it in) doesn't exceed a certain maximum absolute value (max_abs_value).

   • To achieve this, the RangeProof circuit utilized a module named LessThan from the CircomLib library.

   • The problem arose because LessThan was designed to work with numbers of a certain bit length, but the RangeProof didn't ensure that the numbers it received respected that bit length. This means that, with clever input, a malicious actor could make the LessThan function return an incorrect result, which would then allow an out-of-range number to be mistakenly approved by the RangeProof.

2. The Specifics of LessThan:

   • The LessThan module is pretty straightforward. It compares two numbers and outputs 1 if the first number is smaller than the second.

   • Here’s the trick: LessThan is designed to work with numbers of a certain maximum bit length (specified as n). If the numbers have more bits than that, the function will not behave correctly.

3. How This Can Be Exploited:

   • Without constraints on the inputs' bit lengths, an attacker can input numbers for max_abs_value and in that have more bits than the LessThan function expects.

   • This can cause the LessThan function to return an incorrect result, allowing the attacker to satisfy the RangeProof even if the number is actually out of range.

4. The Fix:

   • To address this vulnerability, the developers added constraints on the bit lengths of the inputs (max_abs_value and in). They ensured that these inputs have a bit length that aligns with what the LessThan function expects.

The described vulnerability has to do with a weakness in the constraint system of a zero-knowledge proof, specifically related to the RangeProof that ensures an input number is within a certain range. Let's unpack the implications and potential attacks:

1. The Purpose of RangeProof: The primary purpose of a RangeProof is to prove that a particular number lies within a certain range without revealing the exact number. In this context, it's crucial to ensure that the proof is bulletproof, because if an attacker can convince a verifier that a number lies within a range when it actually doesn't, it can break the integrity of the whole system.

2. Potential Attack: If an attacker can feed the LessThan function with numbers that have more bits than expected, they might get the function to output an incorrect result. This could potentially allow an attacker to submit an out-of-range number while still producing a valid RangeProof—effectively lying about the number being within the range.

3. Implications: Let's use an analogy. Imagine a secured gate that only allows cars of a certain size to pass through. If someone found a way to trick the gate's sensor into allowing larger vehicles, they could potentially smuggle unauthorized or dangerous items. Similarly, if the RangeProof is not robust, it could lead to unauthorized or malicious transactions, a breach of privacy, or other unwanted outcomes, depending on the application.

4. Why It's a Big Issue:

   • Trust: In cryptographic systems, especially ones like zero-knowledge proofs, trust is paramount. If there's a vulnerability that allows someone to produce a misleading proof, it undermines the whole system.

   • Financial Implications: Many zero-knowledge systems, including zk-SNARKs, are used in financial systems like certain blockchain implementations. If an attacker can misrepresent a transaction, they might be able to steal or double-spend funds.

   • Privacy Breach: ZK systems often handle sensitive data. A vulnerability could lead to a breach of privacy or unauthorized data access.

   • Integrity of Computation: In some systems, ensuring a value is within a certain range might be critical for other computations. If an out-of-bounds value is introduced, it could lead to unexpected behaviors or errors elsewhere in the system.

References:

1. ZKPs for Engineers: A look at the Dark Forest ZKPs (See the “Bonus 1: Range Proofs” section)

2. Commit of the Fix