Security and optimizations (#116)

* Improve IN and other operators' calculation security

* Move safe calculation of signal with value one to separate template. Added empty assignments for unused signals to remove compiler warnings. Removed one unused template.

* Update comments with number of constraints

circuits/auth/authV2.circom

@@ -1,10 +1,11 @@
 pragma circom 2.1.1;
 
-include "../lib/idOwnership.circom";
-include "../lib/utils/idUtils.circom";
 include "../../node_modules/circomlib/circuits/mux1.circom";
 include "../../node_modules/circomlib/circuits/comparators.circom";
 include "../../node_modules/circomlib/circuits/eddsaposeidon.circom";
+include "../lib/idOwnership.circom";
+include "../lib/utils/idUtils.circom";
+include "../lib/utils/safeOne.circom";
 
 template AuthV2(IdOwnershipLevels, onChainLevels) {
     signal input genesisID;
@@ -48,17 +49,8 @@ template AuthV2(IdOwnershipLevels, onChainLevels) {
     // unless nonce == 0, in which case userID will be assigned with userGenesisID
     signal output userID;
 
-    /////////////////////////////////////////////////////////////////
-    // FIXME: `===` without multiplications gives 0 constraints!!!
-    // because compiler removes all linear constraints during optimization pass
-    // ForceEqualIfEnabled(1, [x, y]) gives 0 too, so we need to do a workaround:
-    // calculate signal with value 1 and pass it to ForceEqualIfEnabled as an enabled signal
-    /////////////////////////////////////////////////////////////////
-    signal tmp <== IsZero()(genesisID);
-    signal tmp2 <== NOT()(tmp);
-    signal zero <== IsEqual()([tmp, tmp2]);
-    signal one <== IsZero()(zero);
-    zero * one === 0;
+    // get safe zero and one values to be used in ForceEqualIfEnabled
+    signal one <== SafeOne()(genesisID);
 
     checkAuthV2(IdOwnershipLevels, onChainLevels)(
         one,

circuits/lib/query/comparators.circom

@@ -1,31 +1,27 @@
 pragma circom 2.1.1;
 
 include "../../../node_modules/circomlib/circuits/comparators.circom";
+include "../../../node_modules/circomlib/circuits/gates.circom";
 
 // nElements - number of value elements
-// Example nElements = 3, '1' v ['12', '1231', '9999'], 1 not in array of values
+// Example nElements = 3, '1' in ['12', '1231', '9999'], 1 not in array of values
 template IN (valueArraySize){
 
         signal input in;
         signal input value[valueArraySize];
         signal output out;
 
         component eq[valueArraySize];
-        signal count[valueArraySize+1];
-        count[0] <== 0;
+        signal isEq[valueArraySize+1];
+        isEq[0] <== 0;
         for (var i=0; i<valueArraySize; i++) {
             eq[i] = IsEqual();
             eq[i].in[0] <== in;
             eq[i].in[1] <== value[i];
-            count[i+1] <== count[i] + eq[i].out;
+            isEq[i+1] <== OR()(isEq[i], eq[i].out);
         }
 
-        // Greater than
-        component gt = GreaterThan(16);
-        gt.in[0] <== count[valueArraySize];
-        gt.in[1] <== 0;
-
-        out <== gt.out; // 1 - if in signal in the list, 0 - if it is not
+        out <== isEq[valueArraySize];
 }
 
 // As LessThan but for all possible numbers from field (not only 252-bit-max like LessThan)

circuits/lib/query/query.circom

@@ -35,23 +35,23 @@ template Query (valueArraySize) {
     signal eq <== IsEqual()([in, value[0]]);
 
     // LessThan
-    signal lt <== LessThan254()([in, value[0]]);
+    signal lt <== LessThan254()([in, value[0]]); // 767 constraints
+
+    // lte
+    signal lte <== OR()(lt, eq); // lte === lt || eq
 
     // GreaterThan
-    signal gt <== GreaterThan254()([in, value[0]]);
+    signal gt <== NOT()(lte); // gt === !lte
+
+    // gte
+    signal gte <== NOT()(lt); // gte === !lt
 
     // in
     signal inComp <== IN(valueArraySize)(in, value);
 
-    // lte
-    signal lte <== 1 - gt; // lte === !gt
-
-    // gte
-    signal gte <== 1 - lt; // gte === !lt
-
     // between (value[0] <= in <= value[1])
     signal gt2 <== GreaterThan254()([in, value[1]]);
-    signal lte2 <== 1 - gt2; // lte === !gt
+    signal lte2 <== NOT()(gt2); // lte === !gt
     signal between <== AND()(gte, lte2);
 
     signal opBits[5] <== Num2Bits(5)(operator); // values 0-15 are query operators, 16-31 - modifiers/computations
@@ -61,14 +61,15 @@ template Query (valueArraySize) {
     queryOpSatisfied.s <== [opBits[0], opBits[1], opBits[2], opBits[3]];
     // We don't use 5th bit (opBits[4]) here; which specifies whether operator is query or
     // modifier/computation operator. It's used in the final mux.
+    _ <== opBits[4];
 
     queryOpSatisfied.c[0] <== 1; // noop; skip execution
     queryOpSatisfied.c[1] <== eq;
     queryOpSatisfied.c[2] <== lt;
     queryOpSatisfied.c[3] <== gt;
     queryOpSatisfied.c[4] <== inComp; // in
-    queryOpSatisfied.c[5] <== 1-inComp; // nin
-    queryOpSatisfied.c[6] <== 1-eq; // neq
+    queryOpSatisfied.c[5] <== NOT()(inComp); // nin
+    queryOpSatisfied.c[6] <== NOT()(eq); // neq
     queryOpSatisfied.c[7] <== lte; // lte === !gt
     queryOpSatisfied.c[8] <== gte; // gte === !lt
     queryOpSatisfied.c[9] <== between; // between

circuits/lib/stateTransition.circom

@@ -7,6 +7,7 @@ include "../../node_modules/circomlib/circuits/poseidon.circom";
 include "../../node_modules/circomlib/circuits/bitify.circom";
 include "../../node_modules/circomlib/circuits/smt/smtverifier.circom";
 include "../../node_modules/circomlib/circuits/smt/smtprocessor.circom";
+include "utils/safeOne.circom";
 include "idOwnership.circom";
 
 template StateTransition(IdOwnershipLevels) {
@@ -36,9 +37,8 @@ template StateTransition(IdOwnershipLevels) {
     signal input newRevTreeRoot;
     signal input newRootsTreeRoot;
 
-    signal zero <== IsZero()(userID); // comparing to zero something that can't be zero to get zero as an output
-    signal one <== 1 - zero;
-    zero * one === 0;
+    // get safe one values to be used in ForceEqualIfEnabled
+    signal one <== SafeOne()(userID);
 
     signal cutId <== cutId()(userID);
 

circuits/lib/utils/claimUtils.circom

@@ -31,6 +31,11 @@ template getClaimSubjectOtherIden() {
     mux.c[3] <== claim[1*4 + 1];
 
     id <== mux.out;
+
+    // explicitly state that these signals are not used and it's ok
+    for (var i=0; i<8; i++) {
+        _ <== claim[i];
+    }
 }
 
 // getClaimMerkilizeFlag checks that a claim flag is set and return merklized slot.
@@ -65,6 +70,11 @@ template getClaimMerklizeRoot() {
     gt.in[0] <== merklizeLocation;
     gt.in[1] <== 0;
     flag <== gt.out;
+
+    // explicitly state that these signals are not used and it's ok
+    for (var i=0; i<8; i++) {
+        _ <== claim[i];
+    }
 }
 
 
@@ -89,6 +99,14 @@ template getClaimHeader() {
     for (var i=0; i<32; i++) {
         claimFlags[i] <== i0Bits.out[128 + i];
     }
+
+    // explicitly state that some of these signals are not used and it's ok
+    for (var i=1; i<8; i++) {
+        _ <== claim[i];
+    }
+    for (var i=160; i<254; i++) {
+        _ <== i0Bits.out[i];
+    }
 }
 
 // getClaimRevNonce gets the revocation nonce out of a claim outputing it as an integer.
@@ -105,6 +123,14 @@ template getClaimRevNonce() {
         claimRevNonce.in[i] <== v0Bits.out[i];
     }
     revNonce <== claimRevNonce.out;
+
+    // explicitly state that some of these signals are not used and it's ok
+    for (var i=0; i<8; i++) {
+        _ <== claim[i];
+    }
+    for (var i=0; i<254; i++) {
+        _ <== v0Bits.out[i];
+    }
 }
 
 //  getClaimHiHv calculates the hashes Hi and Hv of a claim (to be used as
@@ -225,6 +251,11 @@ template getPubKeyFromClaim() {
 
     Ax <== claim[2]; // Ax should be in indexSlotA
     Ay <== claim[3]; // Ay should be in indexSlotB
+
+    // explicitly state that these signals are not used and it's ok
+    for (var i=0; i<8; i++) {
+        _ <== claim[i];
+    }
 }
 
 // getValueByIndex select slot from claim by given index
@@ -281,6 +312,14 @@ template getClaimExpiration() {
         expirationBits.in[i] <== v0Bits.out[i+64];
     }
     expiration <== expirationBits.out;
+
+    // explicitly state that some of these signals are not used and it's ok
+    for (var i=0; i<8; i++) {
+        _ <== claim[i];
+    }
+    for (var i=0; i<254; i++) {
+        _ <== v0Bits.out[i];
+    }
 }
 
 // getSubjectLocation extract subject from claim flags.
@@ -295,6 +334,11 @@ template getSubjectLocation() {
     }
 
     out <== subjectBits.out;
+
+    // explicitly state that some of these signals are not used and it's ok
+    for (var i=0; i<32; i++) {
+        _ <== claimFlags[i];
+    }
 }
 
 // getMerklizeLocation extract merklize from claim flags.
@@ -310,6 +354,11 @@ template getMerklizeLocation() {
     }
 
     out <== mtBits.out;
+
+    // explicitly state that some of these signals are not used and it's ok
+    for (var i=0; i<32; i++) {
+        _ <== claimFlags[i];
+    }
 }
 
 // isExpirable return 1 if expiration flag is set otherwise 0.

circuits/lib/utils/idUtils.circom

@@ -16,6 +16,10 @@ template ProfileID(){
     genesisIdParts.id <== in;
 
     out <== NewID()(genesisIdParts.typ, genesis);
+
+    // explicitly state that these signals are not used and it's ok
+    _ <== genesisIdParts.genesis;
+    _ <== genesisIdParts.checksum;
 }
 
 // Split ID into type, genesys and checksum
@@ -46,6 +50,11 @@ template SplitID() {
         typBits.in[i] <== bs.out[i];
     }
     typ <== typBits.out;
+
+    // explicitly state that some of these signals are not used and it's ok
+    for (var i=0; i<254; i++) {
+        _ <== bs.out[i];
+    }
 }
 
 template NewID() {
@@ -101,6 +110,11 @@ template TakeNBits(n) {
         outBits.in[i] <== bits.out[i];
     }
     out <== outBits.out;
+
+    // explicitly state that these signals are not used and it's ok
+    for (var i=n; i<254; i++) {
+        _ <== bits.out[i];
+    }
 }
 
 template CalculateIdChecksum() {

circuits/lib/utils/safeOne.circom

@@ -0,0 +1,23 @@
+pragma circom 2.1.1;
+
+include "../../../node_modules/circomlib/circuits/comparators.circom";
+include "../../../node_modules/circomlib/circuits/gates.circom";
+
+/////////////////////////////////////////////////////////////////
+// SafeZeroOne calculates safe one signals from any signal coming from outside of circuit
+// It is needed because linear constraints are not giving real security guarantees and circom is
+// removing them during optimization pass.
+// Because of this `===` without multiplications gives 0 constraints!!!
+// ForceEqualIfEnabled(1, [x, y]) gives 0 too.
+// Only ForceEqualIfEnabled(enabled, [x, y]) with `enabled` from input signal or signal safely derived
+// from input signal generates constraints.
+// That's why we need to calculate safe zero and one signals from input signal.
+/////////////////////////////////////////////////////////////////
+template SafeOne() {
+    signal input inputSignal;
+    signal tmp <== IsZero()(inputSignal);
+    signal tmp2 <== NOT()(tmp);
+    signal zero <== IsEqual()([tmp, tmp2]);
+    signal output one <== IsZero()(zero);
+    zero * one === 0;
+}

circuits/lib/utils/treeUtils.circom

@@ -74,60 +74,6 @@ template checkIdenStateMatchesRoots() {
     );
 }
 
-// verifyClaimIssuanceNonRev verifies that claim is issued by the issuer and not revoked
-// TODO: review if we need both verifyClaimIssuanceNonRev and verifyClaimIssuance
-template verifyClaimIssuanceNonRev(IssuerLevels) {
-	signal input claim[8];
-	signal input claimHi;
-	signal input claimHv;
-	signal input claimIssuanceMtp[IssuerLevels];
-	signal input claimIssuanceClaimsTreeRoot;
-	signal input claimIssuanceRevTreeRoot;
-	signal input claimIssuanceRootsTreeRoot;
-	signal input claimIssuanceIdenState;
-
-	signal input enabledNonRevCheck;
-	signal input claimNonRevMtp[IssuerLevels];
-	signal input claimNonRevMtpNoAux;
-	signal input claimNonRevMtpAuxHi;
-	signal input claimNonRevMtpAuxHv;
-	signal input claimNonRevIssuerClaimsTreeRoot;
-	signal input claimNonRevIssuerRevTreeRoot;
-	signal input claimNonRevIssuerRootsTreeRoot;
-	signal input claimNonRevIssuerState;
-
-    verifyClaimIssuance(IssuerLevels)(
-        1, //tmp
-        claimHi,
-        claimHv,
-        claimIssuanceMtp,
-        claimIssuanceClaimsTreeRoot,
-        claimIssuanceRevTreeRoot,
-        claimIssuanceRootsTreeRoot,
-        claimIssuanceIdenState
-    );
-
-    // check non-revocation proof for claim
-    checkClaimNotRevoked(IssuerLevels)(
-        enabledNonRevCheck,
-        claim,
-        claimNonRevMtp,
-        claimIssuanceRevTreeRoot,
-        claimNonRevMtpNoAux,
-        claimNonRevMtpAuxHi,
-        claimNonRevMtpAuxHv
-    );
-
-    // check issuer state matches for non-revocation proof
-    checkIdenStateMatchesRoots()(
-        1, //tmp
-        claimNonRevIssuerClaimsTreeRoot,
-        claimNonRevIssuerRevTreeRoot,
-        claimNonRevIssuerRootsTreeRoot,
-        claimNonRevIssuerState
-    );
-}
-
 // verifyClaimIssuance verifies that claim is issued by the issuer
 template verifyClaimIssuance(IssuerLevels) {
     signal input enabled;
@@ -217,4 +163,9 @@ template VerifyAuthClaimAndSignature(nLevels) {
         challengeSignatureR8y,
         challenge
     );
+
+    // explicitly state that some of these signals are not used and it's ok
+    for (var i=0; i<32; i++) {
+        _ <== authClaimHeader.claimFlags[i];
+    }
 }