Underconstrained Comparison Can Be Exploited to Drain Funds
Description. We found a soundness issue in the low-level greater_than_zero() gadget, which leads to issues with many gadgets that directly or indirectly depend on it: greater_than_eq(), less_than(), constrain_less_than(), div_rem() and floor(). The unsoundness of floor() can be used to escape a critical check in the malleable-match circuit: that a user’s balance is sufficient to cover the trade being performed. We describe below how this might be exploited in an attack that drains the darkpool’s entire balance of any token.
This is the code of greater_than_eq_zero(), plus two of its subcomponents:
/// Evaluate the condition x >= 0; returns 1 if true, otherwise 0
pub fn greater_than_eq_zero(
x: Variable,
cs: &mut PlonkCircuit,
) -> Result<BoolVar, CircuitError> {
// Decompose and reconstruct the value in the given bitlength, if we can do so
// then the value is greater than zero
let reconstructed = ToBitsGadget::<D>::decompose_and_reconstruct(x, cs)?;
EqGadget::eq(&reconstructed, &x, cs)
}
/// Decompose and reconstruct a value to and from its bitwise representation
/// with a fixed bitlength
///
/// This is useful as a range check for a power of two, wherein the value
/// may only be represented in 2^D bits
pub fn decompose_and_reconstruct(
a: Variable,
cs: &mut PlonkCircuit,
) -> Result<Variable, CircuitError> {
let bits = Self::to_bits_unconstrained(a, cs)?;
Self::bit_reconstruct(&bits, cs)
}
/// [ZKSECURITY] ...
/// Converts a value to its bitwise representation without constraining the
/// value to be correct
fn to_bits_unconstrained(
/// [ZKSECURITY] ...
In summary, the gadget witnesses some value reconstructed which is known to be in the target bit range . As the code comment correctly points out, if the input x equals reconstructed, then we can conclude . So x must be greater or equal zero, using the common definition that negative numbers are those greater than half the field size.
The issue is that the converse is not true: Just because x does not equal reconstructed, we can’t conclude that x is negative. A malicious prover could simply tweak to_bits_unconstrained() to witness some arbitrary bits unrelated to the input. This causes greater_than_eq_zero() to always return false. In other words, we can’t rely on this gadget when it returns false.
The issue directly affects downstream gadgets:
greater_than_eq(a, b)just callsgreater_than_eq_zero()on the differencea - b, so it has the same issueless_than()logically negates the output ofgreater_than_eq(), so we can’t rely on it when it returnstrueconstrain_less_than()enforces the output ofless_than()to betrue, which is meaningless, and can be achieved by a malicious prover regardless of the inputdiv_rem(a, b)performs Euclidian division to produce a quotient and remainder such that . However, it usesconstrain_less_than()to check . By escaping this check, a prover can make the quotient smaller than it should be by adding multiples of to the remainder.
Finally, floor(x) is affected as follows: It takes as input a FixedPointVar, a fractional number that is represented as the field element , where M is the maximum length of the fractional part. It rounds that number down by doing an integer division by , so it returns . The division is done using div_rem(). By tweaking the quotient to be smaller, a malicious prover can change the floor() output to be any integer less than the input.
Impact. Of the gadgets identified as unsound, only floor() is directly used in protocol circuits. Furthermore, floor() is only used in the new malleable-match circuit. Circuits that were deployed prior to this audit are unaffected by this issue.
The impact to malleable-match proofs is severe and directly exploitable, as the following snippet shows:
// Compute the maximum amounts sent and received
let max_base = match_res.max_base_amount;
let max_quote_fp = match_res.price.mul_integer(max_base, cs)?;
let max_quote = FixedPointGadget::floor(max_quote_fp, cs)?;
// Select the appropriate amount based on the internal party's side
// order.side = 1 implies that the internal party sells the base asset
let max_send_recv = CondSelectVectorGadget::select(
&[max_base, max_quote], &[max_quote, max_base], order.side, cs)?;
let max_send = max_send_recv[0];
let max_recv = max_send_recv[1];
Self::validate_match_capitalized(max_send, send_bal, cs)?;
Note that floor() is used to calculate max_quote. If the internal party takes the “buy” side of the trade and sells the quote asset, max_quote is assigned to max_send. The last line in the snippet checks that there is enough balance in the wallet, by constraining send_bal.amount >= max_send.
Since an attacker can make max_send smaller than its actual value, by tweaking floor(), they can make the send_bal.amount >= max_send check succeed, regardless of the actual match result. Effectively, the attacker can trade funds that they don’t actually have in their wallet.
The underfunded trade is not prevented by any checks in the smart contract, since by design, user balances are not revealed onchain. Instead, the balance will be updated indirectly via an update to its public share, and will underflow and become a large number close to the field size when unblinded and combined with the private share.
The resulting wallet, which now has a huge quote balance, might no longer be usable for withdrawal, due to range checks in the update-wallet circuit. In particular, the base tokens received in the trade might not be accessible to the attacker. However, we believe an underfunded trade can still be exploited: note that we effectively print quote tokens to the external counter-party, and those are withdrawn immediately in the atomic swap. An attacker could take the role of the external party themselves. By setting an artificially high price for the base token, they can move an arbitrary amount of quote tokens out of the darkpool, in exchange for burning a tiny amount of base tokens.
The only quote token supported by the official relayer API is USDC. However, since running relayers is permissionless and the limitation to USDC is not enforced onchain, it appears to us that an attacker is free to choose which token balance to drain in a single swap.
Recommendation. To fix greater_than_eq_zero(), we can take inspiration from the classic LessThan gadget in circomlib. The following pseudo-code implements the gadget in a sound way:
/// input assumption: -2^D ≤ x < 2^D (necessary for completeness)
fn greater_than_eq_zero(D, x) {
// constrained D+1 bits decomposition of 2^D + x
let bits = to_bits(D + 1, (1 << D) + x);
// x ≥ 0 ↔ 2^D + x ≥ 2^D ↔ Dth bit is set
bits[D]
}
Client response. The issue was fixed in commit 0f2f9a7, following our recommendation.