Nurit CR

safe-global · May 27, 2024 · 76d0729 · 76d0729
1 parent ba92c5b
commit 76d0729
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 39 deletions.
diff --git a/certora/confs/ProxySimulator.conf b/certora/confs/ProxySimulator.conf
@@ -1,7 +1,7 @@
 {
     "assert_autofinder_success": true,
     "files": [
-        "modules/passkey/contracts/ProxySimulator.sol",
+        "certora/helpers/ProxySimulator.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
         "modules/passkey/contracts/libraries/P256.sol",
@@ -11,14 +11,6 @@
         "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,8 +20,6 @@
     "optimistic_loop": true,
     "loop_iter": "6",
     "optimistic_hashing": true,
-    "prover_version": "master",
-    "server": "production",
     "rule_sanity": "basic",
     "verify": "ProxySimulator:certora/specs/ProxySimulator.spec"
 }
diff --git a/certora/confs/SafeWebAuthnSignerProxy.conf b/certora/confs/SafeWebAuthnSignerProxy.conf
@@ -11,14 +11,6 @@
         "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,8 +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"
 }
diff --git a/certora/confs/SafeWebAuthnSignerProxyHarness.conf b/certora/confs/SafeWebAuthnSignerProxyHarness.conf
@@ -1,21 +1,14 @@
 {
     "assert_autofinder_success": true,
     "files": [
-        "modules/passkey/contracts/SafeWebAuthnSignerProxyHarness.sol",
+        "certora/harnesses/SafeWebAuthnSignerProxyHarness.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
-        //"certora/harnesses/ERC20Like/DummyWeth.sol",
-		//"certora/harnesses/Utilities.sol",
         "modules/passkey/contracts/libraries/P256.sol"
     ],
     "link": [
         "SafeWebAuthnSignerProxyHarness:_VERIFIERS=P256",
         "SafeWebAuthnSignerProxyHarness:_SINGLETON=SafeWebAuthnSignerSingleton"
     ],
-    "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"
@@ -25,8 +18,6 @@
     "optimistic_loop": true,
     "loop_iter": "6",
     "optimistic_hashing": true,
-    "prover_version": "master",
-    "server": "production",
     "rule_sanity": "basic",
     "verify": "SafeWebAuthnSignerProxyHarness:certora/specs/SafeWebAuthnSignerProxyHarness.spec"
 }
diff --git a/...tracts/SafeWebAuthnSignerProxyHarness.sol → ...nesses/SafeWebAuthnSignerProxyHarness.sol b/...tracts/SafeWebAuthnSignerProxyHarness.sol → ...nesses/SafeWebAuthnSignerProxyHarness.sol
@@ -2,15 +2,16 @@
 /* solhint-disable no-complex-fallback */
 pragma solidity >=0.8.0;
 
-import {P256} from "./libraries/WebAuthn.sol";
-import {SafeWebAuthnSignerProxy} from "./SafeWebAuthnSignerProxy.sol";
+import {P256} from "../../modules/passkey/contracts/libraries/WebAuthn.sol";
+import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol";
 
 /**
- * @title Safe WebAuthn Signer Proxy
- * @dev A specialized proxy to a {SafeWebAuthnSignerSingleton} signature validator implementation
- * for Safe accounts. Using a proxy pattern for the signature validator greatly reduces deployment
- * gas costs.
- * @custom:security-contact bounty@safe.global
+ * @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 { 
     /**

diff --git a/modules/passkey/contracts/ProxySimulator.sol → certora/helpers/ProxySimulator.sol b/modules/passkey/contracts/ProxySimulator.sol → certora/helpers/ProxySimulator.sol
@@ -2,7 +2,7 @@
 /* solhint-disable no-complex-fallback */
 pragma solidity >=0.8.0;
 
-import {SafeWebAuthnSignerProxy} from "./SafeWebAuthnSignerProxy.sol";
+import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol";
 
 contract ProxySimulator {
 

diff --git a/certora/specs/ProxySimulator.spec b/certora/specs/ProxySimulator.spec
@@ -1,5 +1,6 @@
 using SafeWebAuthnSignerProxy as SafeWebAuthnSignerProxy;
 
+// This is the same MAGIC_VALUE constant used in ERC1271.
 definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e);
 
 methods {