Certora Prover setup and properties for the audit of Passkey module

certora/confs/GetConfigurationConf.conf

@@ -0,0 +1,25 @@
+{
+	"assert_autofinder_success": true,
+	"files": [
+		"certora/munged/SafeWebAuthnSignerSingleton.sol",
+		"certora/harnesses/GetConfigurationProxyHarness.sol",
+		"modules/passkey/contracts/SafeWebAuthnSignerFactory.sol"
+	],
+	"link": [
+		"GetConfigurationProxyHarness:_SINGLETON=SafeWebAuthnSignerSingleton"
+	],
+	"loop_iter": "6",
+	"optimistic_hashing": true,
+	"optimistic_loop": true,
+	"packages": [
+		"@safe-global=node_modules/@safe-global",
+		"@account-abstraction=node_modules/@account-abstraction"
+	],
+	"process": "emv",
+	"prover_args": [
+		" -split false"
+	],
+	"rule_sanity": "basic",
+	"solc": "solc8.23",
+	"verify": "GetConfigurationProxyHarness:certora/specs/GetConfigurationSpec.spec"
+}

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"
+    ],
+    "hashing_length_bound": "4694",
+    "link": [
+        "GetSignerHarness:SINGLETON=SafeWebAuthnSignerSingleton"
+    ],
+    "loop_iter": "144",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "process": "emv",
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "GetSignerHarness:certora/specs/GetSigner.spec"
+}

certora/confs/ProxySimulator.conf

@@ -0,0 +1,27 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "certora/harnesses/ProxySimulator.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
+        "modules/passkey/contracts/libraries/P256.sol",
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
+    ],
+    "hashing_length_bound": "2048",
+    "link": [
+        "ProxySimulator:_proxy=SafeWebAuthnSignerProxy",
+        "SafeWebAuthnSignerProxy:_VERIFIERS=P256",
+        "SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton"
+    ],
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "process": "emv",
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "ProxySimulator:certora/specs/ProxySimulator.spec"
+}

certora/confs/SafeWebAuthnSignerFactory.conf

@@ -0,0 +1,30 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "certora/harnesses/FactoryHarnessForSignerConsistency.sol",
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"
+    ],
+    "link": [
+        "FactoryHarnessForSignerConsistency:SINGLETON=SafeWebAuthnSignerSingleton"
+    ],
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "rule": [
+        "createAndGetSignerEquivalence",
+        "getSignerRevertingConditions",
+        "hasNoCodeIntegrity",
+        "isValidSignatureForSignerConsistency",
+        "singletonNeverChanges"
+    ],
+    "process": "emv",
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "FactoryHarnessForSignerConsistency:certora/specs/SafeWebAuthnSignerFactoryWithMunge.spec"
+}

certora/confs/SafeWebAuthnSignerProxy.conf

@@ -0,0 +1,23 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
+        "modules/passkey/contracts/libraries/P256.sol"
+    ],
+    "link": [
+        "SafeWebAuthnSignerProxy:_VERIFIERS=P256",
+        "SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton"
+    ],
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "process": "emv",
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "SafeWebAuthnSignerProxy:certora/specs/SafeWebAuthnSignerProxy.spec"
+}

certora/confs/SafeWebAuthnSignerSingleton.conf

@@ -0,0 +1,23 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
+        "modules/passkey/contracts/libraries/P256.sol",
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
+    ],
+    "link": [
+        "SafeWebAuthnSignerFactory:SINGLETON=SafeWebAuthnSignerSingleton"
+    ],
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "process": "emv",
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "SafeWebAuthnSignerSingleton:certora/specs/SafeWebAuthnSignerSingleton.spec"
+}

certora/confs/SignerCreationCantOverride.conf

@@ -0,0 +1,31 @@
+{
+    "assert_autofinder_success": true,
+    "exclude_rule": [
+        "createAndVerifyEQtoIsValidSignatureForSigner"
+    ],
+    "files": [
+        "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
+        "modules/passkey/contracts/libraries/P256.sol",
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
+    ],
+    "hashing_length_bound": "912",
+    "link": [
+        "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton"
+    ],
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "process": "emv",
+    "rule": [
+        "SignerCreationCantOverride"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactory.spec"
+}

certora/confs/SingletonIsValidSignatureRevertingConditions.conf

@@ -0,0 +1,23 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
+        "modules/passkey/contracts/libraries/P256.sol",
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
+    ],
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "process": "emv",
+    "rule": [
+        "isValidSignatureRevertingConditions"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "SafeWebAuthnSignerSingleton:certora/specs/SafeWebAuthnSignerSingleton.spec"
+}

certora/confs/ValidSignatureForSignerIntegrity.conf

@@ -0,0 +1,26 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol",
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"
+    ],
+    "link": [
+        "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton"
+    ],
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "process": "emv",
+    "rule": [
+        "isValidSignatureForSignerIntegrity"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactory.spec"
+}

certora/confs/VerifyEQtoIsValidSignatureForSigner.conf

@@ -0,0 +1,33 @@
+{
+    "assert_autofinder_success": true,
+    "dynamic_bound": "1",
+    "files": [
+        "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol",
+        "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
+        "certora/munged/SafeWebAuthnSignerProxy.sol",
+        "certora/munged/WebAuthn.sol",
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
+    ],
+    "hashing_length_bound": "906",
+    "link": [
+        "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton"
+    ],
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "process": "emv",
+    "prover_args": [
+        "-depth 12"
+    ],
+    "rule": [
+        "createAndVerifyEQtoIsValidSignatureForSigner"
+    ],
+    "rule_sanity": "basic",
+    "smt_timeout": "600",
+    "solc": "solc8.23",
+    "verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactoryWithMunge.spec"
+}

certora/confs/WebAuthn.conf

@@ -0,0 +1,17 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
+    ],
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "process": "emv",
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "WebAuthnHarnessWithMunge:certora/specs/WebAuthn.spec"
+}

certora/harnesses/FactoryHarnessForSignerConsistency.sol

@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+pragma solidity >=0.8.0;
+
+import {SafeWebAuthnSignerFactory} from "../munged/FactoryForSignerConsistency.sol";
+import {P256} from "../../modules/passkey/contracts/libraries/P256.sol";
+import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol";
+
+contract FactoryHarnessForSignerConsistency is SafeWebAuthnSignerFactory {
+
+    //Harness
+    function hasNoCode(address account) external view returns (bool result) {
+        // solhint-disable-next-line no-inline-assembly
+        return SafeWebAuthnSignerFactory._hasNoCode(account);
+    }
+
+    function createAndVerify(
+        bytes32 message,
+        bytes calldata signature,
+        uint256 x,
+        uint256 y,
+        P256.Verifiers verifiers
+    ) external returns (bytes4 magicValue) {
+        address signer = this.createSigner(x, y, verifiers);
+
+        bytes memory data = abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature);
+
+        // Use low-level call to invoke isValidSignature on the signer address
+        (bool success, bytes memory result) = signer.staticcall(data);
+        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;
+    }
+}