AvaCloud Circuits Security Review Report

Status: Fixed

The Circom implementation of BabyJubjub curve operations does not validate that points lie on the curve before performing operations. In Circom (babyjub.circom), while a BabyCheck() template exists that can verify curve membership, it's not used in operations like BabyAdd(), BabyDbl(), or BabyPbk(), potentially allowing operations with invalid points.

template CheckValue() {
    signal input value;
    signal input privKey;
    signal input valueC1[2];
    signal input valueC2[2];
 
    // Verify the value is less than the base order
    assert(value < 2736030358979909402780800718157159386076813972158567259200215660948447373041);
 
    component checkValue = ElGamalDecrypt();
    checkValue.c1[0] <== valueC1[0];
    checkValue.c1[1] <== valueC1[1];
    checkValue.c2[0] <== valueC2[0];
    checkValue.c2[1] <== valueC2[1];
    checkValue.privKey <== privKey;
 
    component valueToPoint = BabyPbk();
    valueToPoint.in <== value;
 
    valueToPoint.Ax === checkValue.outx;
    valueToPoint.Ay === checkValue.outy;
}

template BabyCheck() {
    signal input x;
    signal input y;
 
    signal x2;
    signal y2;
 
    var a = 168700;
    var d = 168696;
 
    x2 <== x*x;
    y2 <== y*y;
 
    a*x2 + y2 === 1 + d*x2*y2;
}

Integrate curve validation in all BabyJubjub operations by adding BabyCheck() calls at the beginning of templates that handle curve points.

Less Than comparison circuits ensure values are below the BabyJubJub subgroup order and validate that spending does not exceed the sender's balance, preserving arithmetic integrity and transactional correctness. There can be applied some optimizations in the comparison:

    var baseOrder = 2736030358979909402780800718157159386076813972158567259200215660948447373041;
 
    component bitCheck1 = Num2Bits(252);
    bitCheck1.in <== random;
 
    component bitCheck2 = Num2Bits(252);
    bitCheck2.in <== baseOrder;
 
    component lt = LessThan(252);
    lt.in[0] <== random;
    lt.in[1] <== baseOrder;
    lt.out === 1;

Since baseOrder is a constant, the bitCheck2 operation is redundant because the constraints are already preserved.

    component bitCheck3 = Num2Bits(252);
    bitCheck3.in <== SenderBalance + 1;
 
    component checkValue = LessThan(252);
    checkValue.in[0] <== ValueToTransfer;
    checkValue.in[1] <== SenderBalance + 1;
    checkValue.out === 1;

In the value comparison section, the LessThan component can be replaced with LessEqThan, and SenderBalance + 1 should be updated to SenderBalance.

Apply the optimizations in PoseidonDecrypt, CheckPublicKey, CheckValue, CheckPCT, MintCircuit, TransferCircuit, WithdrawCircuit components.

Status: Fixed

CheckReceiverValue component validates receiver's encrypted amount equals to the actual receiving amount.

template CheckReceiverValue() {
    signal input receiverValue;
    signal input receiverPublicKey[2];
    signal input receiverRandom;
    signal input receiverValueC1[2];
    signal input receiverValueC2[2];
 
    component receiverValueToPoint = BabyPbk();
    receiverValueToPoint.in <== receiverValue;
 
    component receiverValueEncrypt = ElGamalEncrypt();
    receiverValueEncrypt.random <== receiverRandom;
    receiverValueEncrypt.pk[0] <== receiverPublicKey[0];
    receiverValueEncrypt.pk[1] <== receiverPublicKey[1];
    receiverValueEncrypt.msg[0] <== receiverValueToPoint.Ax;
    receiverValueEncrypt.msg[1] <== receiverValueToPoint.Ay;
 
    receiverValueEncrypt.encryptedC1X === receiverValueC1[0];
    receiverValueEncrypt.encryptedC1Y === receiverValueC1[1];
    receiverValueEncrypt.encryptedC2X === receiverValueC2[0];
    receiverValueEncrypt.encryptedC2Y === receiverValueC2[1];
}

The receiverRandom value misses the check to be less than the BabyJubJub subgroup order.

Validate the receiverRandom to be less than the curve's subgroup order.