From 6a21c3fb59d97c20a6be842913a5df2b1bb4c68f Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Tue, 4 Jun 2024 11:40:31 +0300 Subject: [PATCH 01/19] Fix uniqueSigner and createAndGetSignerEquivalence rules --- certora/confs/WebAuthnBitVectorTheory.conf | 1 + .../SafeWebAuthnSignerFactoryHarness.sol | 17 +++++ certora/specs/SafeWebAuthnSignerFactory.spec | 68 +++++++++++++++++-- certora/specs/WebAuthn.spec | 5 +- .../contracts/SafeWebAuthnSignerFactory.sol | 1 + 5 files changed, 84 insertions(+), 8 deletions(-) diff --git a/certora/confs/WebAuthnBitVectorTheory.conf b/certora/confs/WebAuthnBitVectorTheory.conf index 285439bef..7b928b6fa 100644 --- a/certora/confs/WebAuthnBitVectorTheory.conf +++ b/certora/confs/WebAuthnBitVectorTheory.conf @@ -13,6 +13,7 @@ "@account-abstraction=node_modules/@account-abstraction" ], "prover_args": ["-useBitVectorTheory"], + "rule": ["encodeClientDataJsonIntegrity", "uniqueMessagePerChallenge"], "solc": "solc8.23", "solc_via_ir": false, "optimistic_loop": true, diff --git a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol index 8c9fd02f2..0321274e4 100644 --- a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol +++ b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol @@ -29,4 +29,21 @@ contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory { require(success); magicValue = abi.decode(result, (bytes4)); } + + function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + "01234567891011121314152546", + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))); + } + function castToAddress(uint256 value) public pure returns (address addr){ + addr = address(uint160(value)); + } } diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 731f268c4..c0e6c7e72 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -2,7 +2,8 @@ using SafeWebAuthnSignerProxy as proxy; using SafeWebAuthnSignerSingleton as singleton; methods{ - function getSigner(uint256, uint256, P256.Verifiers) external returns (address); + // function getSigner(uint256, uint256, P256.Verifiers) external returns (address); + // function getSigner(uint256 x, uint256 y, P256.Verifiers v) internal returns (address) => getSignerGhost(x, y, v); function createSigner(uint256, uint256, P256.Verifiers) external returns (address); function hasNoCode(address) external returns (bool) envfree; } @@ -30,10 +31,51 @@ rule singletonNeverChanges() /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ getSigner is unique for every x,y and verifier combination (Violated but low prob) │ + getSigner is unique for every x,y and verifier combination, proved with assumptions: + 1.) value before cast to address <= max_uint160. + 2.) munging required to complete signer data to be constructed from full 32bytes size arrays + function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + "01234567891011121314152546", <--------------- HERE! + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))); + } └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -// consider adding the following munging after the creationcode to get a more clear dump 01234567891011121314152546 + +// helper rule to justify the use of the munged implementation (proved) +rule mungedEquivalence() +{ + env e1; + env e2; + + require e1.msg.value == 0 && e2.msg.value == 0; + uint256 x; + uint256 y; + P256.Verifiers verifier; + + storage s = lastStorage; + + uint256 harnessedSignerValue = getSignerHarnessed@withrevert(e1, x, y, verifier); + bool harnessedSignerRevert1 = lastReverted; + + address harnessedSigner = castToAddress@withrevert(e1, harnessedSignerValue); + bool harnessedSignerRevert2 = harnessedSignerRevert1 && lastReverted; + + address signer = getSigner@withrevert(e2, x, y, verifier) at s; + bool signerRevert = lastReverted; + + assert (harnessedSignerRevert2 == signerRevert); + assert (!harnessedSignerRevert2 && !signerRevert) => (harnessedSigner == signer); +} + rule uniqueSigner(){ env e; @@ -42,23 +84,37 @@ rule uniqueSigner(){ uint256 firstY; P256.Verifiers firstVerifier; - address firstSigner = getSigner(e, firstX, firstY, firstVerifier); + uint256 firstSignerValue = getSignerHarnessed(e, firstX, firstY, firstVerifier); + require firstSignerValue <= max_uint160; + + address firstSigner = castToAddress(e, firstSignerValue); uint256 secondX; uint256 secondY; P256.Verifiers secondVerifier; - address secondSigner = getSigner(e, secondX, secondY, secondVerifier); + uint256 secondSignerValue = getSignerHarnessed(e, secondX, secondY, secondVerifier); + require secondSignerValue <= max_uint160; + + address secondSigner = castToAddress(e, secondSignerValue); + assert firstSigner == secondSigner <=> (firstX == secondX && firstY == secondY && firstVerifier == secondVerifier); } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ createSigner and getSigner always returns the same address (Violated but low prob) │ +│ createSigner and getSigner always returns the same address (Proved under assumption) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ +// Summary is correct only if the unique signer rule is proved !!! +ghost getSignerGhost(uint256, uint256, P256.Verifiers) returns address { + axiom forall uint256 x1. forall uint256 y1. forall P256.Verifiers v1. + forall uint256 x2. forall uint256 y2. forall P256.Verifiers v2. + (getSignerGhost(x1, y1, v1) == getSignerGhost(x2, y2, v2)) <=> (x1 == x2 && y1 == y2 && v1 == v2); +} + rule createAndGetSignerEquivalence(){ env e; diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec index f3abcbc47..efc64ed45 100644 --- a/certora/specs/WebAuthn.spec +++ b/certora/specs/WebAuthn.spec @@ -86,10 +86,11 @@ rule verifySignatureEq(){ bool result1 = verifySignature@withrevert(e, challenge, bytesSignature, authenticatorFlags, x, y, verifiers); bool firstCallRevert = lastReverted; - bool result2 = verifySignature@withrevert(e, challenge, bytesSignature, authenticatorFlags, x, y, verifiers) at firstStorage; + bool result2 = verifySignature@withrevert(e, challenge, structSignature, authenticatorFlags, x, y, verifiers) at firstStorage; bool secondCallRevert = lastReverted; - assert (firstCallRevert == secondCallRevert) || (result1 == result2); + assert firstCallRevert == secondCallRevert; + assert (!firstCallRevert && !secondCallRevert) => result1 == result2; } /* diff --git a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol index 26d9f54c0..629fc574a 100644 --- a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol +++ b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol @@ -36,6 +36,7 @@ contract SafeWebAuthnSignerFactory is ISafeSignerFactory { bytes32 codeHash = keccak256( abi.encodePacked( type(SafeWebAuthnSignerProxy).creationCode, + "01234567891011121314152546", // munged for word alignment workaround (32 bytes) uint256(uint160(address(SINGLETON))), x, y, From 6ba67428a0541d9c215d56a4d847e35de039d6f6 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Tue, 4 Jun 2024 11:42:18 +0300 Subject: [PATCH 02/19] Add summary for getsiner --- certora/specs/SafeWebAuthnSignerFactory.spec | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index c0e6c7e72..e8972bc07 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -2,8 +2,7 @@ using SafeWebAuthnSignerProxy as proxy; using SafeWebAuthnSignerSingleton as singleton; methods{ - // function getSigner(uint256, uint256, P256.Verifiers) external returns (address); - // function getSigner(uint256 x, uint256 y, P256.Verifiers v) internal returns (address) => getSignerGhost(x, y, v); + function getSigner(uint256 x, uint256 y, P256.Verifiers v) internal returns (address) => getSignerGhost(x, y, v); function createSigner(uint256, uint256, P256.Verifiers) external returns (address); function hasNoCode(address) external returns (bool) envfree; } From 80a64da3adf36ae4da5ac0e0bf1498fc94181edb Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Tue, 4 Jun 2024 11:42:56 +0300 Subject: [PATCH 03/19] Add summary for getsiner --- certora/specs/SafeWebAuthnSignerFactory.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index e8972bc07..5c1088890 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -49,7 +49,7 @@ rule singletonNeverChanges() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -// helper rule to justify the use of the munged implementation (proved) +// helper rule to justify the use of the munged implementation (proved) need to drop getSigner summary before execution. rule mungedEquivalence() { env e1; From d668c4142c163c2f704a133c94cd8ec2ccf91143 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Tue, 4 Jun 2024 15:35:41 +0300 Subject: [PATCH 04/19] Add munging for hasNoCode --- certora/specs/SafeWebAuthnSignerFactory.spec | 17 --------------- .../contracts/SafeWebAuthnSignerFactory.sol | 21 ++++++++++++------- 2 files changed, 14 insertions(+), 24 deletions(-) diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 5c1088890..61964356e 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -159,11 +159,9 @@ rule deterministicSigner() ghost mathint numOfCreation; ghost mapping(address => uint) address_map; -ghost bool validValue; hook EXTCODESIZE(address addr) uint v{ require address_map[addr] == v; - validValue = addr <= max_uint160; } hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v{ @@ -189,21 +187,6 @@ rule SignerCreationCantOverride() assert numOfCreation < 2; } -rule ValidValue() -{ - env e; - require !validValue; - - uint x; - uint y; - P256.Verifiers verifier; - - createSigner(e, x, y, verifier); - createSigner@withrevert(e, x, y, verifier); - - satisfy validValue; -} - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Has no code integrity (Proved) │ diff --git a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol index 629fc574a..490704cd4 100644 --- a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol +++ b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol @@ -87,15 +87,22 @@ contract SafeWebAuthnSignerFactory is ISafeSignerFactory { } } + // /** + // * @dev Checks if the provided account has no code. + // * @param account The address of the account to check. + // * @return result True if the account has no code, false otherwise. + // */ + // function _hasNoCode(address account) internal view returns (bool result) { + // // solhint-disable-next-line no-inline-assembly + // assembly ("memory-safe") { + // result := iszero(extcodesize(account)) + // } + // } + /** - * @dev Checks if the provided account has no code. - * @param account The address of the account to check. - * @return result True if the account has no code, false otherwise. + Munged. */ function _hasNoCode(address account) internal view returns (bool result) { - // solhint-disable-next-line no-inline-assembly - assembly ("memory-safe") { - result := iszero(extcodesize(account)) - } + return account.code.length > 0; } } From a43568dc44df652404360cdc456aab780f5d8017 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 5 Jun 2024 12:02:28 +0300 Subject: [PATCH 05/19] Fix verifySignatureEq --- certora/harnesses/WebAuthnHarness.sol | 17 ++++++++++++ certora/specs/WebAuthn.spec | 39 ++++++++++++++++----------- 2 files changed, 41 insertions(+), 15 deletions(-) diff --git a/certora/harnesses/WebAuthnHarness.sol b/certora/harnesses/WebAuthnHarness.sol index e56c8430c..c7548c0a3 100644 --- a/certora/harnesses/WebAuthnHarness.sol +++ b/certora/harnesses/WebAuthnHarness.sol @@ -4,6 +4,23 @@ pragma solidity ^0.8.0; import {P256, WebAuthn} from "../../modules/passkey/contracts/libraries/WebAuthn.sol"; contract WebAuthnHarness { + + mapping (bytes32 => mapping (bytes32 => string)) symbolicClientDataJson; + + function SencodeDataJson(bytes32 challenge, string calldata clientDataFields) public returns (string memory){ + bytes32 hashClientDataFields = keccak256(abi.encodePacked(clientDataFields)); + string memory stringResult = symbolicClientDataJson[challenge][hashClientDataFields]; + bytes32 hashResult = keccak256(abi.encodePacked(stringResult)); + + require (checkInjective(challenge, hashClientDataFields, hashResult)); + + return stringResult; + } + + function checkInjective(bytes32 challenge, bytes32 clientDataFields, bytes32 result) internal view returns (bool){ + return true; + } + function compareSignatures(WebAuthn.Signature memory sig1, WebAuthn.Signature memory sig2) public pure returns (bool) { if (sig1.r != sig2.r || sig1.s != sig2.s) { return false; diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec index efc64ed45..028a8b1c0 100644 --- a/certora/specs/WebAuthn.spec +++ b/certora/specs/WebAuthn.spec @@ -1,22 +1,30 @@ -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ encodeClientDataJsonIntegrity 2 different challenges results in 2 different clientDataJson (Violated) │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule encodeClientDataJsonIntegrity(){ +methods { + function WebAuthn.encodeClientDataJson(bytes32 challenge, string calldata clientDataFields) internal returns (string memory) => + SencodeDataJsonCVL(challenge, clientDataFields); - env e; + function checkInjective(bytes32 challenge, bytes32 clientDataFields, bytes32 result) internal returns (bool) => + checkInjectiveSummary(challenge, clientDataFields, result); - bytes32 challenge1; - string clientDataFields; - bytes32 challenge2; + function P256.verifySignatureAllowMalleability(P256.Verifiers a, bytes32 b, uint256 c, uint256 d, uint256 e, uint256 f) internal returns bool => + verifySignatureAllowMalleabilityGhost(a, b, c, d, e, f); +} + +function SencodeDataJsonCVL(bytes32 challenge, string clientDataFields) returns string +{ + env e; + return SencodeDataJson(e, challenge, clientDataFields); +} - string a1 = encodeClientDataJson(e, challenge1, clientDataFields); - string b1 = encodeClientDataJson(e, challenge2, clientDataFields); +ghost checkInjectiveSummary(bytes32, bytes32, bytes32) returns bool { + axiom forall bytes32 x1. forall bytes32 y1. forall bytes32 x2. forall bytes32 y2. forall bytes32 result. + (x1 != x2) => !(checkInjectiveSummary(x1, y1, result) && checkInjectiveSummary(x2, y2, result)); +} - assert (challenge1 != challenge2) <=> !compareStrings(e, a1, b1); - satisfy true; +ghost verifySignatureAllowMalleabilityGhost(P256.Verifiers, bytes32, uint256, uint256, uint256, uint256) returns bool { + axiom forall P256.Verifiers a. forall bytes32 message1. forall bytes32 message2. forall uint256 c. forall uint256 d. forall uint256 e. forall uint256 f. + verifySignatureAllowMalleabilityGhost(a, message1, c, d, e, f) && + verifySignatureAllowMalleabilityGhost(a, message2, c, d, e, f) => message1 == message2; } /* @@ -48,6 +56,7 @@ rule uniqueMessagePerChallenge(){ bytes32 challenge1; bytes32 challenge2; bytes authenticatorData; + require authenticatorData.length % 32 == 0; string clientDataField; bytes message1 = encodeSigningMessage(e, challenge1, authenticatorData, clientDataField); @@ -58,7 +67,7 @@ rule uniqueMessagePerChallenge(){ /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ verifySignature functions are equivalent (Vacuity check timeout cert-6290) │ +│ verifySignature functions are equivalent (Proved) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule verifySignatureEq(){ From 6e49f8657e538cc0cb9a74e15fa972a2646c47dd Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 5 Jun 2024 12:44:14 +0300 Subject: [PATCH 06/19] Fix castSignatureDeterministicDecoding and castSignatureLengthCheckValidity --- certora/harnesses/WebAuthnHarness.sol | 2 +- certora/specs/WebAuthn.spec | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/harnesses/WebAuthnHarness.sol b/certora/harnesses/WebAuthnHarness.sol index c7548c0a3..20f0410ab 100644 --- a/certora/harnesses/WebAuthnHarness.sol +++ b/certora/harnesses/WebAuthnHarness.sol @@ -38,7 +38,7 @@ contract WebAuthnHarness { } function encodeSignature(WebAuthn.Signature calldata sig) external pure returns (bytes memory signature){ - signature = abi.encode(sig); + signature = abi.encode(sig.authenticatorData, sig.clientDataFields, sig.r, sig.s); } function castSignature(bytes calldata signature) external pure returns (bool isValid, WebAuthn.Signature calldata data){ diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec index 028a8b1c0..424662be2 100644 --- a/certora/specs/WebAuthn.spec +++ b/certora/specs/WebAuthn.spec @@ -144,7 +144,7 @@ rule castSignatureConsistent(){ /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ CastSignature Canonical Deterministic Decoding (Violated) | +│ CastSignature Canonical Deterministic Decoding (Proved) | └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ @@ -165,7 +165,7 @@ rule castSignatureDeterministicDecoding(){ /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ CastSignature Length Check Validity | +│ CastSignature Length Check Validity (Proved) | └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ From a346a51ca97f6de5bced9947304f9836439a2c0f Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 5 Jun 2024 14:31:02 +0300 Subject: [PATCH 07/19] Add verifySignatureConsistent --- certora/specs/WebAuthn.spec | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec index 424662be2..99f011d95 100644 --- a/certora/specs/WebAuthn.spec +++ b/certora/specs/WebAuthn.spec @@ -102,6 +102,40 @@ rule verifySignatureEq(){ assert (!firstCallRevert && !secondCallRevert) => result1 == result2; } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ verifySignature consistent │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule verifySignatureConsistent(){ + env e; + env e1; + env e2; + require e1.msg.value == 0 && e2.msg.value == 0; + method f; + calldataarg args; + + bytes32 challenge; + WebAuthn.AuthenticatorFlags authenticatorFlags; + uint256 x; + uint256 y; + P256.Verifiers verifiers; + bytes bytesSignature; + + + bool result1 = verifySignature@withrevert(e1, challenge, bytesSignature, authenticatorFlags, x, y, verifiers); + bool firstCallRevert = lastReverted; + + f(e, args); + + bool result2 = verifySignature@withrevert(e2, challenge, bytesSignature, authenticatorFlags, x, y, verifiers); + bool secondCallRevert = lastReverted; + + assert firstCallRevert == secondCallRevert; + assert (!firstCallRevert && !secondCallRevert) => result1 == result2; +} + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ CastSignature Consistent (Once valid always valid, Once failed always failed, includes revert cases and middle call)| From 10473cf2e2c5c08ddc6c60e37752c64493d30bf0 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 5 Jun 2024 14:31:16 +0300 Subject: [PATCH 08/19] . --- certora/specs/WebAuthn.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec index 99f011d95..e52f45415 100644 --- a/certora/specs/WebAuthn.spec +++ b/certora/specs/WebAuthn.spec @@ -105,7 +105,7 @@ rule verifySignatureEq(){ /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ verifySignature consistent │ +│ verifySignature consistent (Proved) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule verifySignatureConsistent(){ From d3e5471743bf81266487281e61037da0b87e93e9 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 5 Jun 2024 14:33:42 +0300 Subject: [PATCH 09/19] . --- .../contracts/SafeWebAuthnSignerFactory.sol | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol index 490704cd4..cb39fe9ed 100644 --- a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol +++ b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol @@ -87,22 +87,22 @@ contract SafeWebAuthnSignerFactory is ISafeSignerFactory { } } - // /** - // * @dev Checks if the provided account has no code. - // * @param account The address of the account to check. - // * @return result True if the account has no code, false otherwise. - // */ - // function _hasNoCode(address account) internal view returns (bool result) { - // // solhint-disable-next-line no-inline-assembly - // assembly ("memory-safe") { - // result := iszero(extcodesize(account)) - // } - // } - /** - Munged. + * @dev Checks if the provided account has no code. + * @param account The address of the account to check. + * @return result True if the account has no code, false otherwise. */ function _hasNoCode(address account) internal view returns (bool result) { - return account.code.length > 0; + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + result := iszero(extcodesize(account)) + } } + + // /** + // possible munge to pass the SignerCreationCantOverride rule, wait for concusion. + // */ + // function _hasNoCode(address account) internal view returns (bool result) { + // return account.code.length > 0; + // } } From 80ab0d5ebc8849dc1114c691fce56f625d83d144 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 5 Jun 2024 16:43:29 +0300 Subject: [PATCH 10/19] Organize files --- certora/confs/GetSigner.conf | 23 ++++ certora/confs/SafeWebAuthnSignerFactory.conf | 14 +-- certora/confs/WebAuthnBitVectorTheory.conf | 26 ----- certora/harnesses/GetSignerHarness.sol | 43 ++++++++ .../SafeWebAuthnSignerFactoryHarness.sol | 20 +--- certora/specs/GetSigner.spec | 70 ++++++++++++ certora/specs/SafeWebAuthnSignerFactory.spec | 104 +++--------------- .../contracts/SafeWebAuthnSignerFactory.sol | 14 +-- 8 files changed, 165 insertions(+), 149 deletions(-) create mode 100644 certora/confs/GetSigner.conf delete mode 100644 certora/confs/WebAuthnBitVectorTheory.conf create mode 100644 certora/harnesses/GetSignerHarness.sol create mode 100644 certora/specs/GetSigner.spec diff --git a/certora/confs/GetSigner.conf b/certora/confs/GetSigner.conf new file mode 100644 index 000000000..4484a3502 --- /dev/null +++ b/certora/confs/GetSigner.conf @@ -0,0 +1,23 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/GetSignerHarness.sol", + "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", + "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol" + ], + "link": [ + "GetSignerHarness:SINGLETON=SafeWebAuthnSignerSingleton" + ], + "packages":[ + "@safe-global=node_modules/@safe-global", + "@account-abstraction=node_modules/@account-abstraction" + ], + "rule_sanity": "basic", + "solc": "solc8.23", + "solc_via_ir": false, + "optimistic_loop": true, + "optimistic_hashing": true, + "hashing_length_bound": "4694", + "loop_iter": "144", + "verify": "GetSignerHarness:certora/specs/GetSigner.spec" +} \ No newline at end of file diff --git a/certora/confs/SafeWebAuthnSignerFactory.conf b/certora/confs/SafeWebAuthnSignerFactory.conf index 6dfe5b5f5..6e029af9d 100644 --- a/certora/confs/SafeWebAuthnSignerFactory.conf +++ b/certora/confs/SafeWebAuthnSignerFactory.conf @@ -3,18 +3,11 @@ "files": [ "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol", "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol", - "certora/harnesses/ERC20Like/DummyWeth.sol", - "certora/harnesses/Utilities.sol", - ], - "java_args": [ - " -ea -Dlevel.setup.helpers=info" + "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol" ], "link": [ "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton" ], - "msg": "sanity_with_all_default_summaries", - "process": "emv", "packages":[ "@safe-global=node_modules/@safe-global", "@account-abstraction=node_modules/@account-abstraction" @@ -24,9 +17,6 @@ "solc_via_ir": false, "optimistic_loop": true, "optimistic_hashing": true, - "hashing_length_bound": "4694", - "loop_iter": "144", - "prover_version": "master", - "server": "production", + "loop_iter": "6", "verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactory.spec" } \ No newline at end of file diff --git a/certora/confs/WebAuthnBitVectorTheory.conf b/certora/confs/WebAuthnBitVectorTheory.conf deleted file mode 100644 index 7b928b6fa..000000000 --- a/certora/confs/WebAuthnBitVectorTheory.conf +++ /dev/null @@ -1,26 +0,0 @@ -{ - "assert_autofinder_success": true, - "files": [ - "certora/harnesses/WebAuthnHarness.sol" - ], - "java_args": [ - " -ea -Dlevel.setup.helpers=info" - ], - "msg": "sanity_with_all_default_summaries", - "process": "emv", - "packages":[ - "@safe-global=node_modules/@safe-global", - "@account-abstraction=node_modules/@account-abstraction" - ], - "prover_args": ["-useBitVectorTheory"], - "rule": ["encodeClientDataJsonIntegrity", "uniqueMessagePerChallenge"], - "solc": "solc8.23", - "solc_via_ir": false, - "optimistic_loop": true, - "optimistic_hashing": true, - "prover_version": "master", - "server": "production", - "rule_sanity": "basic", - "loop_iter": "6", - "verify": "WebAuthnHarness:certora/specs/WebAuthn.spec" -} \ No newline at end of file diff --git a/certora/harnesses/GetSignerHarness.sol b/certora/harnesses/GetSignerHarness.sol new file mode 100644 index 000000000..940563550 --- /dev/null +++ b/certora/harnesses/GetSignerHarness.sol @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.8.0; + +import {SafeWebAuthnSignerFactory} from "../../modules/passkey/contracts/SafeWebAuthnSignerFactory.sol"; +import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; +import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; + +contract GetSignerHarness is SafeWebAuthnSignerFactory { + + function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + "01234567891011121314152546", + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))); + } + function castToAddress(uint256 value) public pure returns (address addr){ + addr = address(uint160(value)); + } + + /** + * munged getSigner + */ + function getSigner(uint256 x, uint256 y, P256.Verifiers verifiers) public view override returns (address signer) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + "01234567891011121314152546", // munged for word alignment workaround (32 bytes) + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + signer = address(uint160(uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))))); + } +} diff --git a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol index 0321274e4..a6dfb4101 100644 --- a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol +++ b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol @@ -30,20 +30,10 @@ contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory { magicValue = abi.decode(result, (bytes4)); } - function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) { - bytes32 codeHash = keccak256( - abi.encodePacked( - type(SafeWebAuthnSignerProxy).creationCode, - "01234567891011121314152546", - uint256(uint160(address(SINGLETON))), - x, - y, - uint256(P256.Verifiers.unwrap(verifiers)) - ) - ); - value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))); - } - function castToAddress(uint256 value) public pure returns (address addr){ - addr = address(uint160(value)); + /** + munge to pass the SignerCreationCantOverride rule. + */ + function _hasNoCode(address account) internal view override returns (bool result) { + return account.code.length > 0; } } diff --git a/certora/specs/GetSigner.spec b/certora/specs/GetSigner.spec new file mode 100644 index 000000000..35c4bfb9a --- /dev/null +++ b/certora/specs/GetSigner.spec @@ -0,0 +1,70 @@ +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ + getSigner is unique for every x,y and verifier combination, proved with assumptions: + 1.) value before cast to address <= max_uint160. + 2.) munging required to complete signer data to be constructed from full 32bytes size arrays + function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + "01234567891011121314152546", <--------------- HERE! + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))); + } +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +// helper rule to justify the use of the harnessed implementation (proved). +rule mungedEquivalence() +{ + env e1; + env e2; + + require e1.msg.value == 0 && e2.msg.value == 0; + uint256 x; + uint256 y; + P256.Verifiers verifier; + + storage s = lastStorage; + + uint256 harnessedSignerValue = getSignerHarnessed@withrevert(e1, x, y, verifier); + bool harnessedSignerRevert1 = lastReverted; + + address harnessedSigner = castToAddress@withrevert(e1, harnessedSignerValue); + bool harnessedSignerRevert2 = harnessedSignerRevert1 && lastReverted; + + address signer = getSigner@withrevert(e2, x, y, verifier) at s; + bool signerRevert = lastReverted; + + assert (harnessedSignerRevert2 == signerRevert); + assert (!harnessedSignerRevert2 && !signerRevert) => (harnessedSigner == signer); +} + +rule uniqueSigner(){ + env e; + + uint256 firstX; + uint256 firstY; + P256.Verifiers firstVerifier; + + uint256 firstSignerValue = getSignerHarnessed(e, firstX, firstY, firstVerifier); + require firstSignerValue <= max_uint160; // <=== needed assumption + + address firstSigner = castToAddress(e, firstSignerValue); + + uint256 secondX; + uint256 secondY; + P256.Verifiers secondVerifier; + + uint256 secondSignerValue = getSignerHarnessed(e, secondX, secondY, secondVerifier); + require secondSignerValue <= max_uint160; // <=== needed assumption + + address secondSigner = castToAddress(e, secondSignerValue); + + assert firstSigner == secondSigner <=> (firstX == secondX && firstY == secondY && firstVerifier == secondVerifier); +} \ No newline at end of file diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 61964356e..e4c403394 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -7,6 +7,13 @@ methods{ function hasNoCode(address) external returns (bool) envfree; } +// Summary is correct only if the unique signer rule is proved spec GetSigner +ghost getSignerGhost(uint256, uint256, P256.Verifiers) returns address { + axiom forall uint256 x1. forall uint256 y1. forall P256.Verifiers v1. + forall uint256 x2. forall uint256 y2. forall P256.Verifiers v2. + (getSignerGhost(x1, y1, v1) == getSignerGhost(x2, y2, v2)) <=> (x1 == x2 && y1 == y2 && v1 == v2); +} + definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e); /* @@ -26,94 +33,12 @@ rule singletonNeverChanges() assert currentSingleton == currentContract.SINGLETON; } - - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ - getSigner is unique for every x,y and verifier combination, proved with assumptions: - 1.) value before cast to address <= max_uint160. - 2.) munging required to complete signer data to be constructed from full 32bytes size arrays - function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) { - bytes32 codeHash = keccak256( - abi.encodePacked( - type(SafeWebAuthnSignerProxy).creationCode, - "01234567891011121314152546", <--------------- HERE! - uint256(uint160(address(SINGLETON))), - x, - y, - uint256(P256.Verifiers.unwrap(verifiers)) - ) - ); - value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))); - } -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ - -// helper rule to justify the use of the munged implementation (proved) need to drop getSigner summary before execution. -rule mungedEquivalence() -{ - env e1; - env e2; - - require e1.msg.value == 0 && e2.msg.value == 0; - uint256 x; - uint256 y; - P256.Verifiers verifier; - - storage s = lastStorage; - - uint256 harnessedSignerValue = getSignerHarnessed@withrevert(e1, x, y, verifier); - bool harnessedSignerRevert1 = lastReverted; - - address harnessedSigner = castToAddress@withrevert(e1, harnessedSignerValue); - bool harnessedSignerRevert2 = harnessedSignerRevert1 && lastReverted; - - address signer = getSigner@withrevert(e2, x, y, verifier) at s; - bool signerRevert = lastReverted; - - assert (harnessedSignerRevert2 == signerRevert); - assert (!harnessedSignerRevert2 && !signerRevert) => (harnessedSigner == signer); -} - - -rule uniqueSigner(){ - env e; - - uint256 firstX; - uint256 firstY; - P256.Verifiers firstVerifier; - - uint256 firstSignerValue = getSignerHarnessed(e, firstX, firstY, firstVerifier); - require firstSignerValue <= max_uint160; - - address firstSigner = castToAddress(e, firstSignerValue); - - uint256 secondX; - uint256 secondY; - P256.Verifiers secondVerifier; - - uint256 secondSignerValue = getSignerHarnessed(e, secondX, secondY, secondVerifier); - require secondSignerValue <= max_uint160; - - address secondSigner = castToAddress(e, secondSignerValue); - - - assert firstSigner == secondSigner <=> (firstX == secondX && firstY == secondY && firstVerifier == secondVerifier); -} - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ createSigner and getSigner always returns the same address (Proved under assumption) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -// Summary is correct only if the unique signer rule is proved !!! -ghost getSignerGhost(uint256, uint256, P256.Verifiers) returns address { - axiom forall uint256 x1. forall uint256 y1. forall P256.Verifiers v1. - forall uint256 x2. forall uint256 y2. forall P256.Verifiers v2. - (getSignerGhost(x1, y1, v1) == getSignerGhost(x2, y2, v2)) <=> (x1 == x2 && y1 == y2 && v1 == v2); -} - rule createAndGetSignerEquivalence(){ env e; @@ -224,12 +149,16 @@ rule createAndVerifyEQtoIsValidSignatureForSigner() /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ isValidSignatureForSigner Consistency │ +│ isValidSignatureForSigner Consistency Proved │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule isValidSignatureForSignerConsistency() { env e; + env e1; + env e2; + require e1.msg.value == 0 && e2.msg.value == 0; + method f; calldataarg args; @@ -240,11 +169,14 @@ rule isValidSignatureForSignerConsistency() bytes signature; bytes32 message; - bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier); + bytes4 magic1 = isValidSignatureForSigner@withrevert(e1, message, signature, x, y, verifier); + bool firstRevert = lastReverted; f(e, args); - bytes4 magic2 = isValidSignatureForSigner(e, message, signature, x, y, verifier); + bytes4 magic2 = isValidSignatureForSigner@withrevert(e2, message, signature, x, y, verifier); + bool secondRevert = lastReverted; - assert (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE()); + assert firstRevert == secondRevert; + assert (!firstRevert && !secondRevert) => (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE()); } \ No newline at end of file diff --git a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol index cb39fe9ed..8651a378f 100644 --- a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol +++ b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol @@ -32,11 +32,11 @@ contract SafeWebAuthnSignerFactory is ISafeSignerFactory { /** * @inheritdoc ISafeSignerFactory */ - function getSigner(uint256 x, uint256 y, P256.Verifiers verifiers) public view override returns (address signer) { + // funtion is not really virtual, Munged! + function getSigner(uint256 x, uint256 y, P256.Verifiers verifiers) public view virtual override returns (address signer) { bytes32 codeHash = keccak256( abi.encodePacked( type(SafeWebAuthnSignerProxy).creationCode, - "01234567891011121314152546", // munged for word alignment workaround (32 bytes) uint256(uint160(address(SINGLETON))), x, y, @@ -92,17 +92,11 @@ contract SafeWebAuthnSignerFactory is ISafeSignerFactory { * @param account The address of the account to check. * @return result True if the account has no code, false otherwise. */ - function _hasNoCode(address account) internal view returns (bool result) { + // funtion is not really virtual, munged! + function _hasNoCode(address account) internal view virtual returns (bool result) { // solhint-disable-next-line no-inline-assembly assembly ("memory-safe") { result := iszero(extcodesize(account)) } } - - // /** - // possible munge to pass the SignerCreationCantOverride rule, wait for concusion. - // */ - // function _hasNoCode(address account) internal view returns (bool result) { - // return account.code.length > 0; - // } } From 7d58f27f1055629b55c1ea5c93ebaa55a79699ab Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 5 Jun 2024 17:08:51 +0300 Subject: [PATCH 11/19] . --- certora/specs/SafeWebAuthnSignerFactory.spec | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index e4c403394..4b829c88d 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -149,9 +149,10 @@ rule createAndVerifyEQtoIsValidSignatureForSigner() /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ isValidSignatureForSigner Consistency Proved │ +│ isValidSignatureForSigner Consistency (Proved) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ + rule isValidSignatureForSignerConsistency() { env e; From a9e97ea8831d50166c7f76bffcfa82297b4e6552 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Thu, 6 Jun 2024 12:58:09 +0300 Subject: [PATCH 12/19] . --- certora/specs/SafeWebAuthnSignerFactory.spec | 22 ++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 4b829c88d..b9d5dc833 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -180,4 +180,26 @@ rule isValidSignatureForSignerConsistency() assert firstRevert == secondRevert; assert (!firstRevert && !secondRevert) => (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE()); +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ isValidSignatureForSigner Integrity (Violated) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule isValidSignatureForSignerIntegrity() +{ + env e; + + uint x; + uint y; + P256.Verifiers verifier; + bytes signature; + bytes32 message; + + bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier); + + satisfy magic1 == MAGIC_VALUE(); } \ No newline at end of file From 4d3d0f4030e0ef3454100b3739fc437bb2fd22f5 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Thu, 6 Jun 2024 13:23:21 +0300 Subject: [PATCH 13/19] . --- certora/harnesses/WebAuthnHarness.sol | 2 +- certora/specs/WebAuthn.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/harnesses/WebAuthnHarness.sol b/certora/harnesses/WebAuthnHarness.sol index 20f0410ab..68fbaf4ba 100644 --- a/certora/harnesses/WebAuthnHarness.sol +++ b/certora/harnesses/WebAuthnHarness.sol @@ -7,7 +7,7 @@ contract WebAuthnHarness { mapping (bytes32 => mapping (bytes32 => string)) symbolicClientDataJson; - function SencodeDataJson(bytes32 challenge, string calldata clientDataFields) public returns (string memory){ + function summaryEncodeDataJson(bytes32 challenge, string calldata clientDataFields) public returns (string memory){ bytes32 hashClientDataFields = keccak256(abi.encodePacked(clientDataFields)); string memory stringResult = symbolicClientDataJson[challenge][hashClientDataFields]; bytes32 hashResult = keccak256(abi.encodePacked(stringResult)); diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec index e52f45415..6c194a077 100644 --- a/certora/specs/WebAuthn.spec +++ b/certora/specs/WebAuthn.spec @@ -13,7 +13,7 @@ methods { function SencodeDataJsonCVL(bytes32 challenge, string clientDataFields) returns string { env e; - return SencodeDataJson(e, challenge, clientDataFields); + return summaryEncodeDataJson(e, challenge, clientDataFields); } ghost checkInjectiveSummary(bytes32, bytes32, bytes32) returns bool { From 34450e216e324f5da61b8f84b1f3182ae5443dfa Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Thu, 6 Jun 2024 13:32:17 +0300 Subject: [PATCH 14/19] Add munging remove changes from safe source code --- certora/harnesses/GetSignerHarness.sol | 2 +- .../SafeWebAuthnSignerFactoryHarness.sol | 2 +- certora/munged/SafeWebAuthnSignerFactory.sol | 102 ++++++++++++++++++ certora/specs/WebAuthn.spec | 2 +- .../contracts/SafeWebAuthnSignerFactory.sol | 6 +- 5 files changed, 107 insertions(+), 7 deletions(-) create mode 100644 certora/munged/SafeWebAuthnSignerFactory.sol diff --git a/certora/harnesses/GetSignerHarness.sol b/certora/harnesses/GetSignerHarness.sol index 940563550..f4df4ff78 100644 --- a/certora/harnesses/GetSignerHarness.sol +++ b/certora/harnesses/GetSignerHarness.sol @@ -1,7 +1,7 @@ // SPDX-License-Identifier: LGPL-3.0-only pragma solidity >=0.8.0; -import {SafeWebAuthnSignerFactory} from "../../modules/passkey/contracts/SafeWebAuthnSignerFactory.sol"; +import {SafeWebAuthnSignerFactory} from "../munged/SafeWebAuthnSignerFactory.sol"; import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; diff --git a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol index a6dfb4101..b14b24f23 100644 --- a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol +++ b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol @@ -1,7 +1,7 @@ // SPDX-License-Identifier: LGPL-3.0-only pragma solidity >=0.8.0; -import {SafeWebAuthnSignerFactory} from "../../modules/passkey/contracts/SafeWebAuthnSignerFactory.sol"; +import {SafeWebAuthnSignerFactory} from "../munged/SafeWebAuthnSignerFactory.sol"; import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; diff --git a/certora/munged/SafeWebAuthnSignerFactory.sol b/certora/munged/SafeWebAuthnSignerFactory.sol new file mode 100644 index 000000000..bc85d2cfe --- /dev/null +++ b/certora/munged/SafeWebAuthnSignerFactory.sol @@ -0,0 +1,102 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.8.0; + +import {ISafeSignerFactory} from "../../modules/passkey/contracts/interfaces/ISafeSignerFactory.sol"; +import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; +import {SafeWebAuthnSignerSingleton} from "../../modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol"; +import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; + +/** + * @title Safe WebAuthn Signer Factory + * @dev A factory contract for creating WebAuthn signers. Additionally, the factory supports + * signature verification without deploying a signer proxies. + * @custom:security-contact bounty@safe.global + */ +contract SafeWebAuthnSignerFactory is ISafeSignerFactory { + /** + * @notice The {SafeWebAuthnSignerSingleton} implementation to that is used for signature + * verification by this contract and any proxies it deploys. + */ + SafeWebAuthnSignerSingleton public immutable SINGLETON; + + /** + * @notice Creates a new WebAuthn Safe signer factory contract. + * @dev The {SafeWebAuthnSignerSingleton} singleton implementation is created with as part of + * this constructor. This ensures that the singleton contract is known, and lets us make certain + * assumptions about how it works. + */ + constructor() { + SINGLETON = new SafeWebAuthnSignerSingleton(); + } + + /** + * @inheritdoc ISafeSignerFactory + */ + // funtion is not really virtual, Munged! + function getSigner(uint256 x, uint256 y, P256.Verifiers verifiers) public view virtual override returns (address signer) { + bytes32 codeHash = keccak256( + abi.encodePacked( + type(SafeWebAuthnSignerProxy).creationCode, + uint256(uint160(address(SINGLETON))), + x, + y, + uint256(P256.Verifiers.unwrap(verifiers)) + ) + ); + signer = address(uint160(uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash))))); + } + + /** + * @inheritdoc ISafeSignerFactory + */ + function createSigner(uint256 x, uint256 y, P256.Verifiers verifiers) external returns (address signer) { + signer = getSigner(x, y, verifiers); + + if (_hasNoCode(signer)) { + SafeWebAuthnSignerProxy created = new SafeWebAuthnSignerProxy{salt: bytes32(0)}(address(SINGLETON), x, y, verifiers); + assert(address(created) == signer); + emit Created(signer, x, y, verifiers); + } + } + + /** + * @inheritdoc ISafeSignerFactory + */ + function isValidSignatureForSigner( + bytes32 message, + bytes calldata signature, + uint256 x, + uint256 y, + P256.Verifiers verifiers + ) external view override returns (bytes4 magicValue) { + address singleton = address(SINGLETON); + bytes memory data = abi.encodePacked( + abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature), + x, + y, + verifiers + ); + + // solhint-disable-next-line no-inline-assembly + assembly { + // staticcall to the singleton contract with return size given as 32 bytes. The + // singleton contract is known and immutable so it is safe to specify return size. + if staticcall(gas(), singleton, add(data, 0x20), mload(data), 0, 32) { + magicValue := mload(0) + } + } + } + + /** + * @dev Checks if the provided account has no code. + * @param account The address of the account to check. + * @return result True if the account has no code, false otherwise. + */ + // funtion is not really virtual, munged! + function _hasNoCode(address account) internal view virtual returns (bool result) { + // solhint-disable-next-line no-inline-assembly + assembly ("memory-safe") { + result := iszero(extcodesize(account)) + } + } +} diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec index 6c194a077..40a8734cb 100644 --- a/certora/specs/WebAuthn.spec +++ b/certora/specs/WebAuthn.spec @@ -18,7 +18,7 @@ function SencodeDataJsonCVL(bytes32 challenge, string clientDataFields) returns ghost checkInjectiveSummary(bytes32, bytes32, bytes32) returns bool { axiom forall bytes32 x1. forall bytes32 y1. forall bytes32 x2. forall bytes32 y2. forall bytes32 result. - (x1 != x2) => !(checkInjectiveSummary(x1, y1, result) && checkInjectiveSummary(x2, y2, result)); + (checkInjectiveSummary(x1, y1, result) && checkInjectiveSummary(x2, y2, result)) => (x1 == x2); } ghost verifySignatureAllowMalleabilityGhost(P256.Verifiers, bytes32, uint256, uint256, uint256, uint256) returns bool { diff --git a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol index 8651a378f..26d9f54c0 100644 --- a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol +++ b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol @@ -32,8 +32,7 @@ contract SafeWebAuthnSignerFactory is ISafeSignerFactory { /** * @inheritdoc ISafeSignerFactory */ - // funtion is not really virtual, Munged! - function getSigner(uint256 x, uint256 y, P256.Verifiers verifiers) public view virtual override returns (address signer) { + function getSigner(uint256 x, uint256 y, P256.Verifiers verifiers) public view override returns (address signer) { bytes32 codeHash = keccak256( abi.encodePacked( type(SafeWebAuthnSignerProxy).creationCode, @@ -92,8 +91,7 @@ contract SafeWebAuthnSignerFactory is ISafeSignerFactory { * @param account The address of the account to check. * @return result True if the account has no code, false otherwise. */ - // funtion is not really virtual, munged! - function _hasNoCode(address account) internal view virtual returns (bool result) { + function _hasNoCode(address account) internal view returns (bool result) { // solhint-disable-next-line no-inline-assembly assembly ("memory-safe") { result := iszero(extcodesize(account)) From dc899e6df1cf09b411ea723716e089e62d87e21c Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Thu, 6 Jun 2024 15:59:00 +0300 Subject: [PATCH 15/19] Clean --- certora/specs/SafeWebAuthnSignerFactory.spec | 46 -------------------- certora/specs/WebAuthn.spec | 21 --------- 2 files changed, 67 deletions(-) diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index b9d5dc833..24ee0b423 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -123,30 +123,6 @@ rule hasNoCodeIntegrity() assert (a == proxy) => !hasNoCode(a); } -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ isValidSignatureForSigner equiv to first deploying the signer with the factory, and then | -| verifying the signature with it directly (CERT-6221) │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule createAndVerifyEQtoIsValidSignatureForSigner() -{ - env e; - uint x; - uint y; - P256.Verifiers verifier; - bytes signature; - bytes32 message; - - storage s = lastStorage; - - bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier); - - bytes4 magic2 = createAndVerify(e, message, signature, x, y, verifier) at s; - - assert magic1 == magic2; -} - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ isValidSignatureForSigner Consistency (Proved) │ @@ -180,26 +156,4 @@ rule isValidSignatureForSignerConsistency() assert firstRevert == secondRevert; assert (!firstRevert && !secondRevert) => (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE()); -} - - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ isValidSignatureForSigner Integrity (Violated) │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ - -rule isValidSignatureForSignerIntegrity() -{ - env e; - - uint x; - uint y; - P256.Verifiers verifier; - bytes signature; - bytes32 message; - - bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier); - - satisfy magic1 == MAGIC_VALUE(); } \ No newline at end of file diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec index 4f394a3aa..f59e6818a 100644 --- a/certora/specs/WebAuthn.spec +++ b/certora/specs/WebAuthn.spec @@ -44,27 +44,6 @@ rule shaIntegrity(){ assert (keccak256(input1) != keccak256(input2)) <=> input1_sha != input2_sha; } - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ every 2 challenges results in unique message when using encodeSigningMessage (Timeout cert-6290) │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule uniqueMessagePerChallenge(){ - env e; - - bytes32 challenge1; - bytes32 challenge2; - bytes authenticatorData; - require authenticatorData.length % 32 == 0; - string clientDataField; - - bytes message1 = encodeSigningMessage(e, challenge1, authenticatorData, clientDataField); - bytes message2 = encodeSigningMessage(e, challenge2, authenticatorData, clientDataField); - - assert (challenge1 != challenge2) <=> (getSha256(e, message1) != getSha256(e, message2)); -} - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ verifySignature functions are equivalent (Proved) │ From 7cdc8ac22b2b860cfe31c3d23741a5126ba8b55a Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Thu, 6 Jun 2024 16:51:01 +0300 Subject: [PATCH 16/19] remove munging --- .../harnesses/SafeWebAuthnSignerFactoryHarness.sol | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol index b14b24f23..872879470 100644 --- a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol +++ b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol @@ -30,10 +30,10 @@ contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory { magicValue = abi.decode(result, (bytes4)); } - /** - munge to pass the SignerCreationCantOverride rule. - */ - function _hasNoCode(address account) internal view override returns (bool result) { - return account.code.length > 0; - } + // /** + // munge to pass the SignerCreationCantOverride rule. + // */ + // function _hasNoCode(address account) internal view override returns (bool result) { + // return account.code.length > 0; + // } } From 8a5a2c7700ab1a2d7ac4ddf16d833f5a706d2add Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Thu, 6 Jun 2024 17:15:16 +0300 Subject: [PATCH 17/19] move signer rules --- certora/specs/GetSigner.spec | 19 +++++++++++++++++++ certora/specs/SafeWebAuthnSignerFactory.spec | 18 ------------------ 2 files changed, 19 insertions(+), 18 deletions(-) diff --git a/certora/specs/GetSigner.spec b/certora/specs/GetSigner.spec index 35c4bfb9a..4304f5d9e 100644 --- a/certora/specs/GetSigner.spec +++ b/certora/specs/GetSigner.spec @@ -67,4 +67,23 @@ rule uniqueSigner(){ address secondSigner = castToAddress(e, secondSignerValue); assert firstSigner == secondSigner <=> (firstX == secondX && firstY == secondY && firstVerifier == secondVerifier); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Deterministic address in get signer (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule deterministicSigner() +{ + env e1; + env e2; + + uint x; + uint y; + P256.Verifiers verifier; + + address signer = getSigner(e1, x, y, verifier); + + assert signer == getSigner(e2, x, y, verifier); } \ No newline at end of file diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 24ee0b423..2e2232236 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -57,24 +57,6 @@ rule createAndGetSignerEquivalence(){ assert signer1 == signer2 <=> (createX == getX && createY == getY && createVerifier == getVerifier); } -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Deterministic address in get signer (Proved) │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule deterministicSigner() -{ - env e1; - env e2; - - uint x; - uint y; - P256.Verifiers verifier; - - address signer = getSigner(e1, x, y, verifier); - - assert signer == getSigner(e2, x, y, verifier); -} /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ From df3b264d834db0407ad5531ba7afe35b4e35bdb2 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Thu, 6 Jun 2024 17:23:34 +0300 Subject: [PATCH 18/19] . --- certora/specs/SafeWebAuthnSignerFactory.spec | 37 -------------------- 1 file changed, 37 deletions(-) diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 2e2232236..1444edcaf 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -57,43 +57,6 @@ rule createAndGetSignerEquivalence(){ assert signer1 == signer2 <=> (createX == getX && createY == getY && createVerifier == getVerifier); } - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Correctness of Signer Creation. (Cant called twice and override) (Bug CERT-6252) │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ - -ghost mathint numOfCreation; -ghost mapping(address => uint) address_map; - -hook EXTCODESIZE(address addr) uint v{ - require address_map[addr] == v; -} - -hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v{ - numOfCreation = numOfCreation + 1; - address_map[v] = length; -} - -rule SignerCreationCantOverride() -{ - env e; - require numOfCreation == 0; - - uint x; - uint y; - P256.Verifiers verifier; - - address a = getSigner(e, x, y, verifier); - require address_map[a] == 0; - - createSigner(e, x, y, verifier); - createSigner@withrevert(e, x, y, verifier); - - assert numOfCreation < 2; -} - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Has no code integrity (Proved) │ From 021d60d803f5a39c5f957fd4ce741cdc4f5c5e70 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Mon, 10 Jun 2024 17:27:30 +0300 Subject: [PATCH 19/19] Fix proxy return rule at least on john branch --- certora/confs/ProxySimulator.conf | 4 ++++ certora/specs/ProxySimulator.spec | 36 ++++++++++++++++++++++++++++--- 2 files changed, 37 insertions(+), 3 deletions(-) diff --git a/certora/confs/ProxySimulator.conf b/certora/confs/ProxySimulator.conf index bc56bcf06..1dddbee43 100644 --- a/certora/confs/ProxySimulator.conf +++ b/certora/confs/ProxySimulator.conf @@ -5,6 +5,9 @@ "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol", "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", "modules/passkey/contracts/libraries/P256.sol", + "modules/passkey/contracts/libraries/WebAuthn.sol", + "certora/harnesses/WebAuthnHarness.sol", + ], "link": [ "ProxySimulator:_proxy=SafeWebAuthnSignerProxy", @@ -20,6 +23,7 @@ "optimistic_loop": true, "loop_iter": "6", "optimistic_hashing": true, + "hashing_length_bound": "2048", "rule_sanity": "basic", "verify": "ProxySimulator:certora/specs/ProxySimulator.spec" } \ No newline at end of file diff --git a/certora/specs/ProxySimulator.spec b/certora/specs/ProxySimulator.spec index a8405eeff..43cf3a30d 100644 --- a/certora/specs/ProxySimulator.spec +++ b/certora/specs/ProxySimulator.spec @@ -1,4 +1,33 @@ using SafeWebAuthnSignerProxy as SafeWebAuthnSignerProxy; +using WebAuthnHarness as WebAuthnHarness; + +methods { + function P256.verifySignatureAllowMalleability(P256.Verifiers a, bytes32 b, uint256 c, uint256 d, uint256 e, uint256 f) internal returns (bool) => + verifySignatureAllowMalleabilityGhost(a, b, c, d, e, f); + + function WebAuthn.encodeSigningMessage(bytes32 challenge, bytes calldata authenticatorData, string calldata clientDataFields) internal returns (bytes memory) => + GETencodeSigningMessageCVL(challenge, authenticatorData, clientDataFields); + + function WebAuthnHarness.checkInjective(bytes32 challenge, bytes32 authenticatorData, bytes32 clientDataFields, bytes32 result) internal returns (bool) => + checkInjectiveSummary(challenge, authenticatorData, clientDataFields, result); +} + +function GETencodeSigningMessageCVL(bytes32 challenge, bytes authenticatorData, string clientDataFields) returns bytes +{ + env e; + return WebAuthnHarness.GETencodeSigningMessageSummary(e, challenge, authenticatorData, clientDataFields); +} + +ghost checkInjectiveSummary(bytes32, bytes32, bytes32, bytes32) returns bool { + axiom forall bytes32 x1. forall bytes32 y1. forall bytes32 z1. forall bytes32 x2. forall bytes32 y2. forall bytes32 z2. forall bytes32 result. + checkInjectiveSummary(x1, y1, z1, result) && checkInjectiveSummary(x2, y2, z2, result) => x1 == x2; +} + +ghost verifySignatureAllowMalleabilityGhost(P256.Verifiers, bytes32, uint256, uint256, uint256, uint256) returns bool { + axiom forall P256.Verifiers a. forall bytes32 message1. forall bytes32 message2. forall uint256 c. forall uint256 d. forall uint256 e. forall uint256 f. + verifySignatureAllowMalleabilityGhost(a, message1, c, d, e, f) && + verifySignatureAllowMalleabilityGhost(a, message2, c, d, e, f) => message1 == message2; +} // This is the same MAGIC_VALUE constant used in ERC1271. definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e); @@ -6,14 +35,15 @@ definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e); methods { function authenticate(bytes32, bytes) external returns (bytes4) envfree; function _._ external => DISPATCH [ - SafeWebAuthnSignerProxy._ + SafeWebAuthnSignerProxy._, + SafeWebAuthnSignerSingleton._ ] default NONDET; } /* Property 14. Proxy - verify return data from the fallback is only one of the magicNumbers Uses another contract that simulates interaction with the proxy. The reason is that the prover doesn't check all -possible calldata values so this simualtion will make the prover choose different values that will be passed on the calldata. +possible calldata values so this simulation will make the prover choose different values that will be passed on the calldata. Rule stuck. */ rule proxyReturnValue { @@ -22,5 +52,5 @@ rule proxyReturnValue { bytes4 ret = authenticate(message, signature); - assert ret == MAGIC_VALUE(); + satisfy ret == MAGIC_VALUE() || ret == to_bytes4(0); }