Dark Forest v0.3: Missing Bit Length Check
Dark Forest v0.3: Missing Bit Length Check
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, a fully decentralized and real time strategy game, 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
}
Sources
https://github.com/0xPARC/zk-bug-tracker#dark-forest-1
ZKPs for Engineers: A look at the Dark Forest ZKPs (See the “Bonus 1: Range Proofs” section)
See also
Related Vulnerabilities:
Under-Constrained Circuits vulnerability
Nondeterministic Circuits vulnerability