diff --git a/certora/confs/SafeWebAuthnSignerProxyHarness.conf b/certora/confs/GetSigner.conf similarity index 53% rename from certora/confs/SafeWebAuthnSignerProxyHarness.conf rename to certora/confs/GetSigner.conf index 88193a0dd..4484a3502 100644 --- a/certora/confs/SafeWebAuthnSignerProxyHarness.conf +++ b/certora/confs/GetSigner.conf @@ -1,23 +1,23 @@ { "assert_autofinder_success": true, "files": [ - "certora/harnesses/SafeWebAuthnSignerProxyHarness.sol", + "certora/harnesses/GetSignerHarness.sol", "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/libraries/P256.sol" + "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol" ], "link": [ - "SafeWebAuthnSignerProxyHarness:_VERIFIERS=P256", - "SafeWebAuthnSignerProxyHarness:_SINGLETON=SafeWebAuthnSignerSingleton" + "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, - "loop_iter": "6", "optimistic_hashing": true, - "rule_sanity": "basic", - "verify": "SafeWebAuthnSignerProxyHarness:certora/specs/SafeWebAuthnSignerProxyHarness.spec" + "hashing_length_bound": "4694", + "loop_iter": "144", + "verify": "GetSignerHarness:certora/specs/GetSigner.spec" } \ No newline at end of file diff --git a/certora/confs/ProxySimulator.conf b/certora/confs/ProxySimulator.conf deleted file mode 100644 index bc56bcf06..000000000 --- a/certora/confs/ProxySimulator.conf +++ /dev/null @@ -1,25 +0,0 @@ -{ - "assert_autofinder_success": true, - "files": [ - "certora/helpers/ProxySimulator.sol", - "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/libraries/P256.sol", - ], - "link": [ - "ProxySimulator:_proxy=SafeWebAuthnSignerProxy", - "SafeWebAuthnSignerProxy:_VERIFIERS=P256", - "SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton" - ], - "packages":[ - "@safe-global=node_modules/@safe-global", - "@account-abstraction=node_modules/@account-abstraction" - ], - "solc": "solc8.23", - "solc_via_ir": false, - "optimistic_loop": true, - "loop_iter": "6", - "optimistic_hashing": true, - "rule_sanity": "basic", - "verify": "ProxySimulator:certora/specs/ProxySimulator.spec" -} \ No newline at end of file diff --git a/certora/confs/SafeWebAuthnSignerFactory.conf b/certora/confs/SafeWebAuthnSignerFactory.conf index 6dfe5b5f5..ab76c81e4 100644 --- a/certora/confs/SafeWebAuthnSignerFactory.conf +++ b/certora/confs/SafeWebAuthnSignerFactory.conf @@ -4,17 +4,10 @@ "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" ], "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/SafeWebAuthnSignerSingleton.conf b/certora/confs/SafeWebAuthnSignerSingleton.conf index ec204d76b..8c830b7a1 100644 --- a/certora/confs/SafeWebAuthnSignerSingleton.conf +++ b/certora/confs/SafeWebAuthnSignerSingleton.conf @@ -20,7 +20,5 @@ "optimistic_loop": true, "loop_iter": "6", "optimistic_hashing": true, - "prover_version": "master", - "server": "production", "verify": "SafeWebAuthnSignerSingleton:certora/specs/SafeWebAuthnSignerSingleton.spec" } \ No newline at end of file diff --git a/certora/confs/WebAuthn.conf b/certora/confs/WebAuthn.conf index 06ce73680..c6134961c 100644 --- a/certora/confs/WebAuthn.conf +++ b/certora/confs/WebAuthn.conf @@ -3,11 +3,6 @@ "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" @@ -16,8 +11,6 @@ "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" diff --git a/certora/confs/WebAuthnBitVectorTheory.conf b/certora/confs/WebAuthnBitVectorTheory.conf deleted file mode 100644 index 285439bef..000000000 --- a/certora/confs/WebAuthnBitVectorTheory.conf +++ /dev/null @@ -1,25 +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"], - "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..f4df4ff78 --- /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 "../munged/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 8c9fd02f2..26ae793d7 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/harnesses/SafeWebAuthnSignerProxyHarness.sol b/certora/harnesses/SafeWebAuthnSignerProxyHarness.sol deleted file mode 100644 index 29f9500f9..000000000 --- a/certora/harnesses/SafeWebAuthnSignerProxyHarness.sol +++ /dev/null @@ -1,53 +0,0 @@ -// SPDX-License-Identifier: LGPL-3.0-only -/* solhint-disable no-complex-fallback */ -pragma solidity >=0.8.0; - -import {P256} from "../../modules/passkey/contracts/libraries/WebAuthn.sol"; -import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; - -/** - * @title Safe WebAuthn Signer Proxy Harness - * @dev This harness is written to be able to prove a certain property on the fallback function. - * The property we are proving using this harness is that no combination of x, y and verifiers can make the fallback revert - * due the problems with the untrivial data appanding. - * It adds another function `fallbackButNotDelegating which has the exact same functionality as the original fallback - * but it gets the x, y, and verifiers parameters instead of reading the immutable ones and does not make a delegatecall. - */ -contract SafeWebAuthnSignerProxyHarness is SafeWebAuthnSignerProxy { - /** - * @notice Creates a new WebAuthn Safe Signer Proxy. - * @param singleton The {SafeWebAuthnSignerSingleton} implementation to proxy to. - * @param x The x coordinate of the P-256 public key of the WebAuthn credential. - * @param y The y coordinate of the P-256 public key of the WebAuthn credential. - * @param verifiers The P-256 verifiers used for ECDSA signature verification. - */ - constructor(address singleton, uint256 x, uint256 y, P256.Verifiers verifiers) - SafeWebAuthnSignerProxy(singleton, x, y, verifiers) { } - - /** - * @dev Fallback function forwards all transactions and returns all received return data. - */ - function fallbackButNotDelegating(uint256 x, uint256 y, P256.Verifiers verifiers) external payable returns (bytes4) { - // solhint-disable-next-line no-inline-assembly - assembly { - // Forward the call to the singleton implementation. We append the configuration to the - // calldata instead of having the singleton implementation read it from storage. This is - // both more gas efficient and required for ERC-4337 compatibility. Note that we append - // the configuration fields in reverse order since the fields are packed, and this makes - // it so we don't need to mask any bits from the `verifiers` value. This computes `data` - // to be `abi.encodePacked(msg.data, x, y, verifiers)`. - let data := mload(0x40) - mstore(add(data, add(calldatasize(), 0x36)), verifiers) - mstore(add(data, add(calldatasize(), 0x20)), y) - mstore(add(data, calldatasize()), x) - calldatacopy(data, 0x00, calldatasize()) - - let success := true - returndatacopy(0, 0, returndatasize()) - if iszero(success) { - revert(0, returndatasize()) - } - return(0, returndatasize()) - } - } -} diff --git a/certora/harnesses/WebAuthnHarness.sol b/certora/harnesses/WebAuthnHarness.sol index 5b684bd6c..4ac43aab0 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 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)); + + 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/helpers/ProxySimulator.sol b/certora/helpers/ProxySimulator.sol deleted file mode 100644 index d9decc29f..000000000 --- a/certora/helpers/ProxySimulator.sol +++ /dev/null @@ -1,24 +0,0 @@ -// SPDX-License-Identifier: LGPL-3.0-only -/* solhint-disable no-complex-fallback */ -pragma solidity >=0.8.0; - -import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; - -contract ProxySimulator { - - address internal _proxy; - - constructor(address proxy) { - _proxy = proxy; - } - - function authenticate(bytes32 message, bytes calldata signature) external returns (bytes4) { - bytes memory data = abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature); - - (bool success, bytes memory result) = _proxy.call(data); - - require(success); - - return abi.decode(result, (bytes4)); - } -} \ No newline at end of file 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/GetSigner.spec b/certora/specs/GetSigner.spec new file mode 100644 index 000000000..4304f5d9e --- /dev/null +++ b/certora/specs/GetSigner.spec @@ -0,0 +1,89 @@ +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ + 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); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ 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/ProxySimulator.spec b/certora/specs/ProxySimulator.spec deleted file mode 100644 index a8405eeff..000000000 --- a/certora/specs/ProxySimulator.spec +++ /dev/null @@ -1,26 +0,0 @@ -using SafeWebAuthnSignerProxy as SafeWebAuthnSignerProxy; - -// This is the same MAGIC_VALUE constant used in ERC1271. -definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e); - -methods { - function authenticate(bytes32, bytes) external returns (bytes4) envfree; - function _._ external => DISPATCH [ - SafeWebAuthnSignerProxy._ - ] 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. -Rule stuck. -*/ -rule proxyReturnValue { - bytes32 message; - bytes signature; - - bytes4 ret = authenticate(message, signature); - - assert ret == MAGIC_VALUE(); -} diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 731f268c4..64f0158f6 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -2,11 +2,18 @@ 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 createSigner(uint256, uint256, P256.Verifiers) external returns (address); 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,36 +33,9 @@ rule singletonNeverChanges() assert currentSingleton == currentContract.SINGLETON; } - - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ getSigner is unique for every x,y and verifier combination (Violated but low prob) │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -// consider adding the following munging after the creationcode to get a more clear dump 01234567891011121314152546 - -rule uniqueSigner(){ - env e; - - uint256 firstX; - uint256 firstY; - P256.Verifiers firstVerifier; - - address firstSigner = getSigner(e, firstX, firstY, firstVerifier); - - uint256 secondX; - uint256 secondY; - P256.Verifiers secondVerifier; - - address secondSigner = getSigner(e, secondX, secondY, secondVerifier); - - 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) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ @@ -77,78 +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); -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Correctness of Signer Creation. (Cant called twice and override) (Bug CERT-6252) │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ - -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{ - 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; -} - -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) │ @@ -162,36 +70,17 @@ rule hasNoCodeIntegrity() /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ isValidSignatureForSigner equiv to first deploying the signer with the factory, and then | -| verifying the signature with it directly (CERT-6221) │ +│ isValidSignatureForSigner Consistency (Proved) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -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 │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ rule isValidSignatureForSignerConsistency() { env e; + env e1; + env e2; + require e1.msg.value == 0 && e2.msg.value == 0; + method f; calldataarg args; @@ -202,11 +91,27 @@ 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 firstRevert == secondRevert; + assert (!firstRevert && !secondRevert) => (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE()); +} - assert (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE()); -} \ No newline at end of file +rule getSignerRevertingConditions { + env e; + uint256 x; + uint256 y; + P256.Verifiers verifiers; + + bool triedTransferringEth = e.msg.value != 0; + + getSigner@withrevert(e, x, y, verifiers); + + assert lastReverted <=> triedTransferringEth; +} diff --git a/certora/specs/SafeWebAuthnSignerProxyHarness.spec b/certora/specs/SafeWebAuthnSignerProxyHarness.spec deleted file mode 100644 index 05f8b9302..000000000 --- a/certora/specs/SafeWebAuthnSignerProxyHarness.spec +++ /dev/null @@ -1,21 +0,0 @@ -methods { - function fallbackButNotDelegating(uint256,uint256,P256.Verifiers) external returns (bytes4); -} - -/* -Property 13. Proxy - Fallback data corruption does not revert the fallback (uses data appending that needed to be verified). -The fallback will only revert due to payable modifier. -Rule Verified. -*/ -rule fallbackDoesNotRevert { - env e; - uint256 x; - uint256 y; - P256.Verifiers verifiers; - - bool notEnoughEthSender = e.msg.value > nativeBalances[e.msg.sender]; - - fallbackButNotDelegating@withrevert(e, x, y, verifiers); - - assert lastReverted <=> notEnoughEthSender; -} \ No newline at end of file diff --git a/certora/specs/SafeWebAuthnSignerSingleton.spec b/certora/specs/SafeWebAuthnSignerSingleton.spec index 14a86fea2..bfdf7b3fd 100644 --- a/certora/specs/SafeWebAuthnSignerSingleton.spec +++ b/certora/specs/SafeWebAuthnSignerSingleton.spec @@ -125,3 +125,18 @@ rule verifyIsValidSignatureWillContinueToSucceed(){ satisfy (!firstReverted && firstVerified == to_bytes4(0x1626ba7e)); satisfy true; } + +rule isValidSignatureRevertingConditions { + env e; + bytes32 message; + + WebAuthn.Signature sigStruct; + bytes signature = WebAuthnHarness.encodeSignature(e, sigStruct); + + bool triedTransferringEth = e.msg.value != 0; + bool dataLengthInsufficient = sigStruct.authenticatorData.length <= 32; + + isValidSignature@withrevert(e, message, signature); + + assert lastReverted <=> (triedTransferringEth || dataLengthInsufficient); +} diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec index 753f977ee..f59e6818a 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); +} - string a1 = encodeClientDataJson(e, challenge1, clientDataFields); - string b1 = encodeClientDataJson(e, challenge2, clientDataFields); +function SencodeDataJsonCVL(bytes32 challenge, string clientDataFields) returns string +{ + env e; + return summaryEncodeDataJson(e, challenge, clientDataFields); +} + +ghost checkInjectiveSummary(bytes32, bytes32, bytes32) returns bool { + axiom forall bytes32 x1. forall bytes32 y1. forall bytes32 x2. forall bytes32 y2. forall bytes32 result. + (checkInjectiveSummary(x1, y1, result) && checkInjectiveSummary(x2, y2, result)) => (x1 == x2); +} - 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; } /* @@ -36,29 +44,9 @@ 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; - 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 (Vacuity check timeout cert-6290) │ +│ verifySignature functions are equivalent (Proved) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule verifySignatureEq(){ @@ -86,10 +74,45 @@ 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; + assert (!firstCallRevert && !secondCallRevert) => result1 == result2; +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ verifySignature consistent (Proved) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +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) || (result1 == result2); + assert firstCallRevert == secondCallRevert; + assert (!firstCallRevert && !secondCallRevert) => result1 == result2; } /* @@ -134,7 +157,7 @@ rule castSignatureConsistent(){ /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ CastSignature Canonical Deterministic Decoding | +│ CastSignature Canonical Deterministic Decoding (Proved) | └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ @@ -155,7 +178,7 @@ rule castSignatureDeterministicDecoding(){ /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ CastSignature Length Check Validity | +│ CastSignature Length Check Validity (Proved) | └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */