Skip to content

Commit

Permalink
Audit fixes (#131)
Browse files Browse the repository at this point in the history
* Fix Num2Bits usage

* Add check that signature r8x & r8y are on the curve. Small signal name fix

* Restrict input values for exists operator to 0 and 1

* Check checksum

* Small fixes

* Restrict Num2Bits to 248 bits in cutId
  • Loading branch information
OBrezhniev authored Apr 17, 2024
1 parent cdb8a59 commit a135e48
Show file tree
Hide file tree
Showing 9 changed files with 71 additions and 23 deletions.
18 changes: 14 additions & 4 deletions circuits/auth/authV2.circom
Original file line number Diff line number Diff line change
Expand Up @@ -136,18 +136,28 @@ template checkAuthV2(IdOwnershipLevels, onChainLevels) {
challengeSignatureS
);

/* Check on-chain SMT inclusion existence */
signal cutId <== cutId()(genesisID);
/* Check if state is genesis and if genesisId is valid */

signal cutState <== cutState()(state);

signal isStateGenesis <== IsEqual()([cutId, cutState]);
component genesisIdParts = SplitID();
genesisIdParts.id <== genesisID;

signal calculatedChecksum <== CalculateIdChecksum()(genesisIdParts.typ, genesisIdParts.genesis);
ForceEqualIfEnabled()(
enabled,
[genesisIdParts.checksum, calculatedChecksum]
);

signal isStateGenesis <== IsEqual()([genesisIdParts.genesis, cutState]);

/* Check on-chain SMT inclusion existence */

signal genesisIDHash <== Poseidon(1)([genesisID]);

SMTVerifier(onChainLevels)(
enabled <== enabled,
fnc <== isStateGenesis, // non-inclusion in case if genesis state, otherwise inclusion
fnc <== isStateGenesis, // non-inclusion in case of genesis state, otherwise inclusion
root <== gistRoot,
siblings <== gistMtp,
oldKey <== gistMtpAuxHi,
Expand Down
4 changes: 2 additions & 2 deletions circuits/lib/query/comparators.circom
Original file line number Diff line number Diff line change
Expand Up @@ -59,10 +59,10 @@ template LessThan254() {
signal input in[2];
signal output out;

component n0b = Num2Bits(254);
component n0b = Num2Bits_strict();
n0b.in <== in[0];

component n1b = Num2Bits(254);
component n1b = Num2Bits_strict();
n1b.in <== in[1];

// numbers for high 4 bits
Expand Down
12 changes: 10 additions & 2 deletions circuits/lib/query/processQueryWithModifiers.circom
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,11 @@ template ProcessQueryWithModifiers(claimLevels, maxValueArraySize){
signal isOpNoop <== IsZero()(operator);
signal merklizedAndEnabled <== AND()(enabled, merklized);

signal isOpExists <== IsEqual()([operator, 11]);

// if operator == exists and value[0] == 0 ($exists == false), then claimPathNotExists = 1 (check non-inclusion),
// otherwise claimPathNotExists = 0 (check inclusion)
signal claimPathNotExists <== AND()(IsEqual()([operator, 11]), IsZero()(value[0]));
signal claimPathNotExists <== AND()(isOpExists, IsZero()(value[0]));

// check path/in node exists in merkle tree specified by jsonldRoot
SMTVerifier(claimLevels)(
Expand All @@ -58,12 +60,18 @@ template ProcessQueryWithModifiers(claimLevels, maxValueArraySize){
);

// For non-merklized credentials exists / non-exist operators should always fail
signal isOpExists <== IsEqual()([operator, 11]);
ForceEqualIfEnabled()(
AND()(enabled, NOT()(merklized)),
[isOpExists, 0]
);

// Restrict exists operator input values to 0 and 1
ForceEqualIfEnabled()(
AND()(enabled, isOpExists),
[value[0] * (value[0] - 1), 0]
);


/////////////////////////////////////////////////////////////////
// Query Operator Processing
/////////////////////////////////////////////////////////////////
Expand Down
2 changes: 1 addition & 1 deletion circuits/lib/query/query.circom
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ include "comparators.circom";
8 - greater than or equal
9 - between (value[0] <= in <= value[1])
10 - not between
11 - exist (true / false)
11 - exists (true / false)
Modifier/computation operators:
16 - selective disclosure (16 = 10000 binary)
*/
Expand Down
4 changes: 2 additions & 2 deletions circuits/lib/stateTransition.circom
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@ template StateTransition(IdOwnershipLevels) {
ForceEqualIfEnabled()(one, [stateIsNotZero, 0]);

// old & new state checks
signal oldNewNotEqual <== IsEqual()([oldUserState, newUserState]);
ForceEqualIfEnabled()(one, [oldNewNotEqual, 0]);
signal oldNewEqual <== IsEqual()([oldUserState, newUserState]);
ForceEqualIfEnabled()(one, [oldNewEqual, 0]);

// check userID ownership by correct signature of a hash of old state and new state
signal challenge <== Poseidon(2)([oldUserState, newUserState]);
Expand Down
20 changes: 20 additions & 0 deletions circuits/lib/utils/babyjubjub.circom
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
pragma circom 2.1.5;

include "../../../node_modules/circomlib/circuits/comparators.circom";

template ForceBabyCheckIfEnabled() {
signal input {binary} enabled;
signal input x;
signal input y;

signal x2;
signal y2;

var a = 168700;
var d = 168696;

x2 <== x*x;
y2 <== y*y;

ForceEqualIfEnabled()(enabled, [a*x2 + y2, 1 + d*x2*y2]);
}
13 changes: 9 additions & 4 deletions circuits/lib/utils/claimUtils.circom
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ include "../../../node_modules/circomlib/circuits/mux3.circom";
include "../../../node_modules/circomlib/circuits/mux1.circom";
include "../../../node_modules/circomlib/circuits/mux2.circom";
include "./idUtils.circom";
include "./babyjubjub.circom";

// getClaimSubjectOtherIden checks that a claim Subject is OtherIden and outputs the identity within.
template getClaimSubjectOtherIden() {
Expand Down Expand Up @@ -89,7 +90,7 @@ template getClaimHeader() {
signal output schema;
signal output {binary} claimFlags[32];

component i0Bits = Num2Bits(254);
component i0Bits = Num2Bits_strict();
i0Bits.in <== claim[0];

component schemaNum = Bits2Num(128);
Expand Down Expand Up @@ -120,7 +121,7 @@ template getClaimRevNonce() {

component claimRevNonce = Bits2Num(64);

component v0Bits = Num2Bits(254);
component v0Bits = Num2Bits_strict();
v0Bits.in <== claim[4];
for (var i=0; i<64; i++) {
claimRevNonce.in[i] <== v0Bits.out[i];
Expand Down Expand Up @@ -213,6 +214,8 @@ template verifyClaimSignature() {
signal input pubKeyX;
signal input pubKeyY;

ForceBabyCheckIfEnabled()(enabled, sigR8x, sigR8y);

// signature verification
EdDSAPoseidonVerifier()(
enabled <== enabled,
Expand All @@ -236,6 +239,8 @@ template checkDataSignatureWithPubKeyInClaim() {
component getPubKey = getPubKeyFromClaim();
getPubKey.claim <== claim;

ForceBabyCheckIfEnabled()(enabled, signatureR8X, signatureR8Y);

EdDSAPoseidonVerifier()(
enabled <== enabled,
Ax <== getPubKey.Ax,
Expand Down Expand Up @@ -281,7 +286,7 @@ template getValueByIndex(){
value <== mux.out;
}

// verify that the claim has expiration time and it is less then timestamp
// verify that provided timestamp is less than claim expiration time
template verifyExpirationTime() {
signal input {binary} expirationFlag; // claimFlags[3] (expiration flag) is set
signal input claim[8];
Expand Down Expand Up @@ -311,7 +316,7 @@ template getClaimExpiration() {

component expirationBits = Bits2Num(64);

component v0Bits = Num2Bits(254);
component v0Bits = Num2Bits_strict();
v0Bits.in <== claim[4];
for (var i=0; i<64; i++) {
expirationBits.in[i] <== v0Bits.out[i+64];
Expand Down
20 changes: 13 additions & 7 deletions circuits/lib/utils/idUtils.circom
Original file line number Diff line number Diff line change
Expand Up @@ -102,8 +102,11 @@ template GatherID() {
template TakeNBits(n) {
signal input in;
signal output out;

assert(n <= 254);

// We take only n least significant bits from 254 bit number.
component bits = Num2Bits(254);
component bits = Num2Bits_strict();
bits.in <== in;

component outBits = Bits2Num(n);
Expand Down Expand Up @@ -178,10 +181,10 @@ template cutId() {
signal input in;
signal output out;

signal idBits[256] <== Num2Bits(256)(in);
signal idBits[248] <== Num2Bits(248)(in);

component cut = Bits2Num(256-16-16-8);
for (var i=16; i<256-16-8; i++) {
component cut = Bits2Num(216);
for (var i=16; i<248-16; i++) {
cut.in[i-16] <== idBits[i];
}
out <== cut.out;
Expand All @@ -191,12 +194,15 @@ template cutState() {
signal input in;
signal output out;

signal stateBits[256] <== Num2Bits(256)(in);
signal stateBits[254] <== Num2Bits_strict()(in);

component cut = Bits2Num(256-16-16-8);
for (var i=0; i<256-16-16-8; i++) {
component cut = Bits2Num(216);
// two most significant bits of 256-bit number are always 0, because we have 254-bit prime field
for (var i=0; i<216-2; i++) {
cut.in[i] <== stateBits[i+16+16+8];
}
cut.in[214] <== 0;
cut.in[215] <== 0;
out <== cut.out;
}

Expand Down
1 change: 0 additions & 1 deletion circuits/onchain/credentialAtomicQueryV3OnChain.circom
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ issuerLevels - Merkle tree depth level for claims issued by the issuer
claimLevels - Merkle tree depth level for claim JSON-LD document
maxValueArraySize - Number of elements in comparison array for in/notin operation if level = 3 number of values for
comparison ["1", "2", "3"]
idOwnershipLevels - Merkle tree depth level for personal claims
onChainLevels - Merkle tree depth level for Auth claim on-chain
*/
template credentialAtomicQueryV3OnChain(issuerLevels, claimLevels, maxValueArraySize, idOwnershipLevels, onChainLevels) {
Expand Down

0 comments on commit a135e48

Please sign in to comment.