diff --git a/certora/confs/ProxySimulator.conf b/certora/confs/ProxySimulator.conf new file mode 100644 index 000000000..bc56bcf06 --- /dev/null +++ b/certora/confs/ProxySimulator.conf @@ -0,0 +1,25 @@ +{ + "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/SafeWebAuthnSignerProxy.conf b/certora/confs/SafeWebAuthnSignerProxy.conf index 80b4979ff..4ac4342b6 100644 --- a/certora/confs/SafeWebAuthnSignerProxy.conf +++ b/certora/confs/SafeWebAuthnSignerProxy.conf @@ -3,22 +3,14 @@ "files": [ "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol", "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "certora/harnesses/ERC20Like/DummyWeth.sol", - "certora/harnesses/Utilities.sol", + //"certora/harnesses/ERC20Like/DummyWeth.sol", + //"certora/harnesses/Utilities.sol", "modules/passkey/contracts/libraries/P256.sol" ], "link": [ "SafeWebAuthnSignerProxy:_VERIFIERS=P256", "SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton" ], - "java_args": [ - " -ea -Dlevel.setup.helpers=info" - ], - "msg": "sanity_with_all_default_summaries", - "process": "emv", - "prover_args": [ - " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on" - ], "packages":[ "@safe-global=node_modules/@safe-global", "@account-abstraction=node_modules/@account-abstraction" @@ -28,7 +20,6 @@ "optimistic_loop": true, "loop_iter": "6", "optimistic_hashing": true, - "prover_version": "master", - "server": "production", + "rule_sanity": "basic", "verify": "SafeWebAuthnSignerProxy:certora/specs/SafeWebAuthnSignerProxy.spec" } \ No newline at end of file diff --git a/certora/confs/SafeWebAuthnSignerProxyHarness.conf b/certora/confs/SafeWebAuthnSignerProxyHarness.conf new file mode 100644 index 000000000..88193a0dd --- /dev/null +++ b/certora/confs/SafeWebAuthnSignerProxyHarness.conf @@ -0,0 +1,23 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/SafeWebAuthnSignerProxyHarness.sol", + "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", + "modules/passkey/contracts/libraries/P256.sol" + ], + "link": [ + "SafeWebAuthnSignerProxyHarness:_VERIFIERS=P256", + "SafeWebAuthnSignerProxyHarness:_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": "SafeWebAuthnSignerProxyHarness:certora/specs/SafeWebAuthnSignerProxyHarness.spec" +} \ No newline at end of file diff --git a/certora/harnesses/SafeWebAuthnSignerProxyHarness.sol b/certora/harnesses/SafeWebAuthnSignerProxyHarness.sol new file mode 100644 index 000000000..29f9500f9 --- /dev/null +++ b/certora/harnesses/SafeWebAuthnSignerProxyHarness.sol @@ -0,0 +1,53 @@ +// 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/helpers/ProxySimulator.sol b/certora/helpers/ProxySimulator.sol new file mode 100644 index 000000000..d9decc29f --- /dev/null +++ b/certora/helpers/ProxySimulator.sol @@ -0,0 +1,24 @@ +// 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/specs/ProxySimulator.spec b/certora/specs/ProxySimulator.spec new file mode 100644 index 000000000..a8405eeff --- /dev/null +++ b/certora/specs/ProxySimulator.spec @@ -0,0 +1,26 @@ +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/SafeWebAuthnSignerProxy.spec b/certora/specs/SafeWebAuthnSignerProxy.spec index 3e33ea015..0f665b620 100644 --- a/certora/specs/SafeWebAuthnSignerProxy.spec +++ b/certora/specs/SafeWebAuthnSignerProxy.spec @@ -1,3 +1,4 @@ +/* Setup Artifacts import "ERC20/erc20cvl.spec"; import "ERC20/WETHcvl.spec"; import "ERC721/erc721.spec"; @@ -21,10 +22,35 @@ use rule timeoutChecker filtered { f -> f.contract == currentContract } use rule simpleFrontRunning filtered { f -> f.contract == currentContract } use rule noRevert filtered { f -> f.contract == currentContract } use rule alwaysRevert filtered { f -> f.contract == currentContract } +*/ +using SafeWebAuthnSignerSingleton as SafeWebAuthnSignerSingleton; + +hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + // DELEGATECALL is used in this contract, but it only ever calls into the singleton. + assert (executingContract != currentContract || addr == SafeWebAuthnSignerSingleton, + "we should only `delegatecall` into the singleton." + ); +} + +/* +Property 12. Proxy - Delegate Call Integrity (calls the Singleton) +Hooking on delegate calls will make sure we'll get a violation if the singleton isn't the contract called. +Rule verified. +*/ +rule delegateCallsOnlyToSingleton { + env e; + method f; + calldataarg args; + f(e, args); + + assert true; +} /* -Rule: Proxy Configuration Paramateres Never Change -- Passed +Property 11. Proxy - Immutability of Configuration Parameters (x, y, Singleton, verifier) +x, y, singleton and verifiers never changes after any function call. +Rule verified. */ rule configParametersImmutability { env e; diff --git a/certora/specs/SafeWebAuthnSignerProxyHarness.spec b/certora/specs/SafeWebAuthnSignerProxyHarness.spec new file mode 100644 index 000000000..05f8b9302 --- /dev/null +++ b/certora/specs/SafeWebAuthnSignerProxyHarness.spec @@ -0,0 +1,21 @@ +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