Merge pull request #6 from Certora/liav/property

Proxy properties

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"
+}

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"
 }

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"
+}

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())
+        }
+    }
+}

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));
+    }
+}

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();
+}

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;

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;
+}