`BinSub` & `Bits2Num` vulnerability

[alexbabits]

Preface

I checked GitHub repos that included both BinSub and Bits2Num in their circom files with GitHub's search: "BinSub" AND "Bits2Num" language:circom

I was surprised to find zero live projects affected. Because it appears no live projects are at risk, I'm publishing this bug report publicly.

Overview

BinSub template gracefully handles negative values obtained from subtraction by outputting it's binary out array in Twos Complement form.

For example, if we instantiate BinSub(4):

• Perform 0 - 15 = -15. Where "in": [[0, 0, 0, 0], [1, 1, 1, 1]] and out = [1, 0, 0, 0] = 0001 = {-15, 1}
• Perform 1 - 15 = -14. Where "in": [[1, 0, 0, 0], [1, 1, 1, 1]] and out = [0, 1, 0, 0] = 0010 = {-14, 2}
• Perform 2 - 15 = -13. Where "in": [[0, 1, 0, 0], [1, 1, 1, 1]] and out = [1, 1, 0, 0] = 0011 = {-13, 3}
• ...and so on

We see the out array represent the correct solution in Twos Complement, but also represents it's sister positive number.

Bits2Num template assumes incoming binary representations are always positive decimal numbers.

For example, if we instantiate Bits2Num(4):

• 15 in binary = 1111 = "in": [1, 1, 1, 1]. Outputs out=15
• 14 in binary = 1110 = "in": [0, 1, 1, 1]. Outputs out=14
• 8 in binary = 1000 = "in": [0, 0, 0, 1]. Outputs out=8
• ...and so on

We can see this is a problem anytime the developer wants a negative binary result from BinSub to be translated into it's negative decimal representation through Bits2Num.

Importantly, Bits2Num is silently outputting these incorrect positive numbers, rather than reverting.

Developer makes the incorrect natural assumption: "BinSub allows for negative outputs and handles stuff like 4-10 just fine. There is no negative-specific template for Bits2Num, so it'll handle all positive and negative results from BinSub fine too."

Notice there is already a Num2BitsNeg template which handles conversion of negative numbers into their binary representation. However, there is no Bits2NumNeg capable of handling Twos Complement negative binary values.

Tangential note: Num2BitsNeg seems to perform p - in, rather than outputting in Twos Complement? Not sure that's ideal/intended?

Proof of Concept

zkREPL

pragma circom 2.0.0;

template BinSub(n) {
    signal input in[2][n];
    signal output out[n];

    signal aux;

    var lin = 2**n;
    var lout = 0;

    var i;

    for (i=0; i<n; i++) {
        lin = lin + in[0][i]*(2**i);
        lin = lin - in[1][i]*(2**i);
    }

    for (i=0; i<n; i++) {
        out[i] <-- (lin >> i) & 1;

        // Ensure out is binary
        out[i] * (out[i] - 1) === 0;

        lout = lout + out[i]*(2**i);
    }

    aux <-- (lin >> n) & 1;
    aux*(aux-1) === 0;
    lout = lout + aux*(2**n);

    // Ensure the sum;
    lin === lout;
}


template Bits2Num(n) {
    signal input in[n];
    signal output out;
    var lc1=0;

    var e2 = 1;
    for (var i = 0; i<n; i++) {
        lc1 += in[i] * e2;
        e2 = e2 + e2;
    }

    lc1 ==> out;
}


template BadOutput(n) {
    signal input a[n]; // 6 in binary = 0110  = [0, 1, 1, 0]
    signal input b[n]; // 11 in binary = 1011 = [1, 1, 0, 1]
    signal output out;

    component binsub = BinSub(n); // 6 - 11 = -5
    binsub.in[0] <== a;
    binsub.in[1] <== b;

    component bits2num = Bits2Num(n);
    bits2num.in <== binsub.out; // -5 in twos complement binary

    out <== bits2num.out; // outputs 11 instead of -5
}

component main = BadOutput(4);

/* 
INPUT = {
    "a": [0, 1, 1, 0],
    "b": [1, 1, 0, 1]
}
*/

Recommended Fix

It probably doesn't make sense to stop BinSub from outputting negative results in Twos Complement.

You could add a bit flag attached to the output of BinSub. If b > a (negative result) then flag is 1, else flag is 0.

Then handle this flag accordingly in Bits2Num, allowing it to handle Twos Complement negative representations and normal positive representations.

The flag's Boolean state represents whether or not a binary array is a negative Twos Complement or not.

[alexbabits]

Ammendment: You can't output negative literals, so out restricted to mod p which is {0, p-1}, but the point still remains.

For example, if BinSub does 2 - 14 = -12, which outputs out = [0, 0, 1, 0] = 0100 = {4, -12}.

Using Bits2Num interprets this always as 4, but it should be interpretted as p - 12, when the subtraction produced a negative number.

[alrubio]

Many thanks for reporting your concerns.
Here we don't see any vulnerability in the library circuit, since the BinSub circuit does what is described the comment before the circom code:

(in[0][0]     * 2^0  +  in[0][1]     * 2^1  + ..... + in[0][n-1]    * 2^(n-1))  +
 +  2^n
 - (in[1][0]     * 2^0  +  in[1][1]     * 2^1  + ..... + in[1][n-1]    * 2^(n-1))
 ===
out[0] * 2^0  + out[1] * 2^1 +   + out[n-1] *2^(n-1) + aux

(Although, in fact it should end with + aux*2^n)

We understand some developers may not expect BinSub to use 2's complement representation of binary numbers, but on the other hand, assuming that both inputs are positive, one must be suspicious about how negative results are handled.

As you say, we cannot change this circuit now, as it is used in existing projects, and adding another output is not possible either, as it will change the way the template is used.

Since the behavior is clearly described, we believe that developers will check the specification before using it, and we will study adding a warning in the comments to emphasize this fact and adding other circuits with the sign flag (given by aux) or different implementations of binary subtraction.

[alexbabits]

I'm still concerned it appears to be silent bad footgun for devs, as there's currently no solution for handling Twos Complement outputs from BinSub template. The only natural and available conversion from binary to decimal is via Bits2Num template which outputs incorrect results.

For example, we see that 6 - 11 = 11 when going through BinSub --> Bits2Num flow, when it should be -5, which is p-5 instead. While p-5 is weird, it is correct. We know answer 11 is certainly wrong and silently succeeds dangerously. There's no way for the dev to rectify this atm.

If you find it worthwhile you could add something like these circuits which handle negative values, otherwise I understand if it doesn't make sense to make any changes.

These example circuits are completely separate and new, diff is just used to show difference from original circuits.

// https://github.com/iden3/circomlib/blob/35e54ea21da3e8762557234298dbb553c175ea8d/circuits/binsub.circom#L43-#L74
template BinSubNeg(n) {
    signal input in[2][n];
    signal output out[n];
+    signal output negFlag; // 0 if positive, 1 if negative (twos complement)

    signal aux;

    var lin = 2**n;
    var lout = 0;

    var i;

    for (i=0; i<n; i++) {
        lin = lin + in[0][i]*(2**i);
        lin = lin - in[1][i]*(2**i);
    }

    for (i=0; i<n; i++) {
        out[i] <-- (lin >> i) & 1;

        // Ensure out is binary
        out[i] * (out[i] - 1) === 0;

        lout = lout + out[i]*(2**i);
    }

    aux <-- (lin >> n) & 1;
    aux*(aux-1) === 0;
    lout = lout + aux*(2**n);

+    negFlag <== 1 - aux;

    // Ensure the sum;
    lin === lout;
}

// https://github.com/iden3/circomlib/blob/35e54ea21da3e8762557234298dbb553c175ea8d/circuits/bitify.circom#L55-#L67
// input = 0 should use negFlag = 0, else it outputs p - 2^n. Could also add constraints to force input 0 uses negFlag 0.
template Bits2NumNeg(n) {
    signal input in[n];
+    signal input negFlag; // 0 for positive, 1 for negative (Two's Complement)
    signal output out;
    
+    negFlag * (negFlag - 1) === 0;

+    // Normal
    var lc1 = 0;
    var e2 = 1;
    for (var i = 0; i < n; i++) {
        lc1 += in[i] * e2;
        e2 = e2 + e2;
    }
    
+    // Two's Complement
+    var lc2 = lc1 - (2**n);
    
+    signal negValue <== negFlag * lc2;

+    out <== negValue + (1 - negFlag) * lc1;
}

BinSubNeg(4) zkREPL outputs

// 12 - 5 = 7
in = [[0, 0, 1, 1],[1, 0, 1, 0]], negFlag=0, out=[1,1,1,0]

// 13 - 15 = -2
in = [[1, 0, 1, 1],[1, 1, 1, 1]], negFlag=1, out=[0,1,1,1]

// 5 - 5 = 0
in = [[1, 0, 1, 0],[1, 0, 1, 0]], negFalg=0, out=[0,0,0,0]

Bits2NumNeg(4) zkREPL outputs

// normal
in=[0,0,0,0], negFlag=0, out = 0
in=[1,0,0,0], negFlag=0, out = 1
in=[0,1,0,0], negFlag=0, out = 2
...
in=[1,1,1,1], negFlag=0, out = 15

// twos complement
in=[0,0,0,0], negFlag=1, out = p-16
in=[1,0,0,0], negFlag=1, out = p-15
in=[0,1,0,0], negFlag=1, out = p-14
...
in=[1,1,1,1], negFlag, out = p-1

Useful Info

https://www.omnicalculator.com/math/twos-complement
p = 21888242871839275222246405745257275088548364400416034343698204186575808495617
[0, 0, 0, 0]  // {0, 0}
[1, 0, 0, 0]  // {1, -15}
[0, 1, 0, 0]  // {2, -14}
[1, 1, 0, 0]  // {3, -13}
[0, 0, 1, 0]  // {4, -12}
[1, 0, 1, 0]  // {5, -11}
[0, 1, 1, 0]  // {6, -10}
[1, 1, 1, 0]  // {7, -9}
[0, 0, 0, 1]  // {8, -8}
[1, 0, 0, 1]  // {9, -7}
[0, 1, 0, 1]  // {10, -6}
[1, 1, 0, 1]  // {11, -5}
[0, 0, 1, 1]  // {12, -4}
[1, 0, 1, 1]  // {13, -3}
[0, 1, 1, 1]  // {14, -2}
[1, 1, 1, 1]  // {15, -1}