Merge pull request #12 from Certora/niv/snapshot-to-certora

Niv/snapshot to certora

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

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

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

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";
 
@@ -29,4 +29,11 @@ contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory {
         require(success);
         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;
+    // }
 }

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;

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 [email protected]
+ */
+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))
+        }
+    }
+}

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