WebAuthnHarness to WebAuthnHarnessWithMunge fix

safe-global · Sep 12, 2024 · a1eab8a · a1eab8a
1 parent 0862df2
commit a1eab8a
Show file tree

Hide file tree

Showing 10 changed files with 12 additions and 16 deletions.
diff --git a/certora/confs/ProxySimulator.conf b/certora/confs/ProxySimulator.conf
@@ -5,8 +5,7 @@
         "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
         "modules/passkey/contracts/libraries/P256.sol",
-        "modules/passkey/contracts/libraries/WebAuthn.sol",
-        "certora/harnesses/WebAuthnHarness.sol"
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
     ],
     "hashing_length_bound": "2048",
     "link": [

diff --git a/certora/confs/SafeWebAuthnSignerSingleton.conf b/certora/confs/SafeWebAuthnSignerSingleton.conf
@@ -3,9 +3,8 @@
     "files": [
         "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
-        "modules/passkey/contracts/libraries/WebAuthn.sol",
         "modules/passkey/contracts/libraries/P256.sol",
-        "certora/harnesses/WebAuthnHarness.sol"
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
     ],
     "link": [
         "SafeWebAuthnSignerFactory:SINGLETON=SafeWebAuthnSignerSingleton"

diff --git a/certora/confs/SignerCreationCantOverride.conf b/certora/confs/SignerCreationCantOverride.conf
@@ -7,9 +7,8 @@
         "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
-        "modules/passkey/contracts/libraries/WebAuthn.sol",
         "modules/passkey/contracts/libraries/P256.sol",
-        "certora/harnesses/WebAuthnHarness.sol"
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
     ],
     "hashing_length_bound": "912",
     "link": [

diff --git a/certora/confs/SingletonIsValidSignatureRevertingConditions.conf b/certora/confs/SingletonIsValidSignatureRevertingConditions.conf
@@ -3,9 +3,8 @@
     "files": [
         "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
-        "modules/passkey/contracts/libraries/WebAuthn.sol",
         "modules/passkey/contracts/libraries/P256.sol",
-        "certora/harnesses/WebAuthnHarness.sol"
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
     ],
     "loop_iter": "6",
     "optimistic_hashing": true,

diff --git a/certora/confs/ValidSignatureForSignerIntegrity.conf b/certora/confs/ValidSignatureForSignerIntegrity.conf
@@ -2,7 +2,7 @@
     "assert_autofinder_success": true,
     "files": [
         "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol",
-        "certora/harnesses/WebAuthnHarness.sol",
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"
     ],

diff --git a/certora/confs/WebAuthn.conf b/certora/confs/WebAuthn.conf
@@ -1,7 +1,7 @@
 {
     "assert_autofinder_success": true,
     "files": [
-        "certora/harnesses/WebAuthnHarness.sol"
+        "certora/harnesses/WebAuthnHarnessWithMunge.sol"
     ],
     "loop_iter": "6",
     "optimistic_hashing": true,
@@ -13,5 +13,5 @@
     "process": "emv",
     "rule_sanity": "basic",
     "solc": "solc8.23",
-    "verify": "WebAuthnHarness:certora/specs/WebAuthn.spec"
+    "verify": "WebAuthnHarnessWithMunge:certora/specs/WebAuthn.spec"
 }
diff --git a/certora/specs/ProxySimulator.spec b/certora/specs/ProxySimulator.spec
@@ -1,5 +1,5 @@
 using SafeWebAuthnSignerProxy as SafeWebAuthnSignerProxy;
-using WebAuthnHarness as WebAuthnHarness;
+using WebAuthnHarnessWithMunge as WebAuthnHarness;
 
 methods {
     function P256.verifySignatureAllowMalleability(P256.Verifiers a, bytes32 b, uint256 c, uint256 d, uint256 e, uint256 f) internal returns (bool) => 

diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec
@@ -1,6 +1,6 @@
 using SafeWebAuthnSignerProxy as proxy;
 using SafeWebAuthnSignerSingleton as singleton;
-using WebAuthnHarness as WebAuthnHarness;
+using WebAuthnHarnessWithMunge as WebAuthnHarness;
 
 
 methods{

diff --git a/certora/specs/SafeWebAuthnSignerSingleton.spec b/certora/specs/SafeWebAuthnSignerSingleton.spec
@@ -1,4 +1,4 @@
-using WebAuthnHarness as WebAuthnHarness;
+using WebAuthnHarnessWithMunge as WebAuthnHarness;
 
 methods {
     function P256.verifySignatureAllowMalleability(P256.Verifiers a, bytes32 b, uint256 c, uint256 d, uint256 e, uint256 f) internal returns (bool) => 

diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec
@@ -198,7 +198,7 @@ rule castSignatureDeterministicDecoding(){
 │ CastSignature Length Check Validity (Proved)                                                                        |
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-
+/*  note: the rule requires specific features still not available on a stable certora-cli
 rule castSignatureLengthCheckValidity(){
     env e;
 
@@ -213,7 +213,7 @@ rule castSignatureLengthCheckValidity(){
 
     assert isValid <=> length_is_correct;
 }
-
+*/
 /*
 ┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ castSignature Reverting Conditions                                                                                                       |