Fix uniqueSigner and createAndGetSignerEquivalence rules

safe-global · Jun 4, 2024 · 6a21c3f · 6a21c3f
1 parent 6ad4b5e
commit 6a21c3f
Show file tree

Hide file tree

Showing 5 changed files with 84 additions and 8 deletions.
diff --git a/certora/confs/WebAuthnBitVectorTheory.conf b/certora/confs/WebAuthnBitVectorTheory.conf
@@ -13,6 +13,7 @@
         "@account-abstraction=node_modules/@account-abstraction"
     ],
     "prover_args": ["-useBitVectorTheory"],
+    "rule": ["encodeClientDataJsonIntegrity", "uniqueMessagePerChallenge"],
     "solc": "solc8.23",
     "solc_via_ir": false,
     "optimistic_loop": true,

diff --git a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol
@@ -29,4 +29,21 @@ contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory {
         require(success);
         magicValue = abi.decode(result, (bytes4));
     }
+
+    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));
+    }
 }
diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec
@@ -2,7 +2,8 @@ using SafeWebAuthnSignerProxy as proxy;
 using SafeWebAuthnSignerSingleton as singleton;
 
 methods{
-    function getSigner(uint256, uint256, P256.Verifiers) external returns (address);
+    // function getSigner(uint256, uint256, P256.Verifiers) external returns (address);
+    // function getSigner(uint256 x, uint256 y, P256.Verifiers v) internal returns (address) => getSignerGhost(x, y, v);
     function createSigner(uint256, uint256, P256.Verifiers) external returns (address);
     function hasNoCode(address) external returns (bool) envfree;
 }
@@ -30,10 +31,51 @@ rule singletonNeverChanges()
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ getSigner is unique for every x,y and verifier combination    (Violated but low prob)                               │
+ 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)));
+    }                  
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-// consider adding the following munging after the creationcode to get a more clear dump 01234567891011121314152546
+
+// helper rule to justify the use of the munged 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;
@@ -42,23 +84,37 @@ rule uniqueSigner(){
     uint256 firstY;
     P256.Verifiers firstVerifier;
 
-    address firstSigner = getSigner(e, firstX, firstY, firstVerifier);
+    uint256 firstSignerValue = getSignerHarnessed(e, firstX, firstY, firstVerifier);
+    require firstSignerValue <= max_uint160;
+
+    address firstSigner = castToAddress(e, firstSignerValue);
 
     uint256 secondX;
     uint256 secondY;
     P256.Verifiers secondVerifier;
 
-    address secondSigner = getSigner(e, secondX, secondY, secondVerifier);
+    uint256 secondSignerValue = getSignerHarnessed(e, secondX, secondY, secondVerifier);
+    require secondSignerValue <= max_uint160;
+
+    address secondSigner = castToAddress(e, secondSignerValue);
+
 
     assert firstSigner == secondSigner <=> (firstX == secondX && firstY == secondY && firstVerifier == secondVerifier);
 }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ createSigner and getSigner always returns the same address   (Violated but low prob)                                │
+│ createSigner and getSigner always returns the same address   (Proved under assumption)                              │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 
+// Summary is correct only if the unique signer rule is proved !!! 
+ghost getSignerGhost(uint256, uint256, P256.Verifiers) returns address {
+    axiom forall uint256 x1. forall uint256 y1. forall P256.Verifiers v1.
+    forall uint256 x2. forall uint256 y2. forall P256.Verifiers v2.
+    (getSignerGhost(x1, y1, v1) == getSignerGhost(x2, y2, v2)) <=> (x1 == x2 && y1 == y2 && v1 == v2); 
+}
+
 rule createAndGetSignerEquivalence(){
     env e;
 

diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec
@@ -86,10 +86,11 @@ rule verifySignatureEq(){
     bool result1 = verifySignature@withrevert(e, challenge, bytesSignature, authenticatorFlags, x, y, verifiers);
     bool firstCallRevert = lastReverted;
 
-    bool result2 = verifySignature@withrevert(e, challenge, bytesSignature, authenticatorFlags, x, y, verifiers) at firstStorage;
+    bool result2 = verifySignature@withrevert(e, challenge, structSignature, authenticatorFlags, x, y, verifiers) at firstStorage;
     bool secondCallRevert = lastReverted;
 
-    assert (firstCallRevert == secondCallRevert) || (result1 == result2);
+    assert firstCallRevert == secondCallRevert;
+    assert (!firstCallRevert && !secondCallRevert) => result1 == result2;
 }
 
 /*

diff --git a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol
@@ -36,6 +36,7 @@ contract SafeWebAuthnSignerFactory is ISafeSignerFactory {
         bytes32 codeHash = keccak256(
             abi.encodePacked(
                 type(SafeWebAuthnSignerProxy).creationCode,
+                "01234567891011121314152546", // munged for word alignment workaround (32 bytes)
                 uint256(uint160(address(SINGLETON))),
                 x,
                 y,