Merge branch 'certora' into yoav/Singleton

safe-global · Jun 23, 2024 · a05a177 · a05a177
2 parents e81f28b + e6f8e21
commit a05a177
Show file tree

Hide file tree

Showing 18 changed files with 371 additions and 370 deletions.
diff --git a/...confs/SafeWebAuthnSignerProxyHarness.conf → certora/confs/GetSigner.conf b/...confs/SafeWebAuthnSignerProxyHarness.conf → 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"
 }
diff --git a/certora/confs/ProxySimulator.conf b/certora/confs/ProxySimulator.conf
diff --git 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"
 }
diff --git 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"
 }
diff --git 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
diff --git a/certora/harnesses/GetSignerHarness.sol 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
@@ -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
diff --git 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