Add webAuth rules

safe-global · May 27, 2024 · bf0ff62 · bf0ff62
1 parent dca8c02
commit bf0ff62
Show file tree

Hide file tree

Showing 3 changed files with 79 additions and 4 deletions.
diff --git a/certora/confs/WebAuthn.conf b/certora/confs/WebAuthn.conf
@@ -1,9 +1,7 @@
 {
     "assert_autofinder_success": true,
     "files": [
-        "certora/harnesses/WebAuthnHarness.sol",
-        "certora/harnesses/ERC20Like/DummyWeth.sol",
-		"certora/harnesses/Utilities.sol",
+        "certora/harnesses/WebAuthnHarness.sol"
 	],
     "java_args": [
         " -ea -Dlevel.setup.helpers=info"

diff --git a/certora/harnesses/WebAuthnHarness.sol b/certora/harnesses/WebAuthnHarness.sol
@@ -21,6 +21,22 @@ contract WebAuthnHarness {
         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;
+        }
+
+        if (keccak256(abi.encodePacked(sig1.clientDataFields)) != keccak256(abi.encodePacked(sig2.clientDataFields))) {
+            return false;
+        }
+
+        if (keccak256(sig1.authenticatorData) != keccak256(sig2.authenticatorData)) {
+            return false;
+        }
+
+        return true;
+    }
+
     function castSignature(bytes calldata signature) external pure returns (bool isValid, WebAuthn.Signature calldata data){
         return WebAuthn.castSignature(signature);
     }

diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec
@@ -8,6 +8,7 @@ methods{
         encodeAxiomSummary(message, signature, result);
 
     //function encodeSigningMessage(bytes32,bytes calldata,string calldata) internal returns(bytes memory) => NONDET;
+    function castSignature(bytes calldata signature) external returns (bool, WebAuthn.Signature calldata);
 }
 
 function getEncodeClientDataJsonSummaryCVL(bytes32 message, string signature) returns string
@@ -75,7 +76,7 @@ rule uniqueMessagePerChallenge(){
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ verifySignature functions are equivalent                                                                            │
+│ verifySignature functions are equivalent (Vacuity check timeout cert-6290)                                          │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 rule verifySignatureEq(){
@@ -109,5 +110,65 @@ rule verifySignatureEq(){
     assert (firstCallRevert == secondCallRevert) || (result1 == result2);
 }
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ CastSignature Consistent (Once valid always valid, Once failed always failed, includes revert cases and middle call)|
+│   (Proved)                                                                                                          |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+rule castSignatureConsistent(){
+    env e;
+    method f;
+    calldataarg args;
+
+    bytes signature;
+
+    bool firstIsValid;
+    WebAuthn.Signature firstData;
+
+    bool secondIsValid;
+    WebAuthn.Signature secondData;
+
+    firstIsValid, firstData = castSignature@withrevert(e, signature);
+    bool firstRevert = lastReverted;
+
+    f(e, args);
+
+    secondIsValid, secondData = castSignature@withrevert(e, signature);
+    bool secondRevert = lastReverted;
+
+    if (!firstRevert && !secondRevert) {
+        assert compareSignatures(e, firstData, secondData) && firstIsValid == secondIsValid;
+    }
+
+    assert firstRevert == secondRevert;
+}
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ CastSignature uniqueness (violated)                                                                                 |
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+rule castSignatureUniqueness(){
+
+    env e;
+
+    bytes signature1;
+    bytes signature2;
+
+    bool firstIsValid;
+    WebAuthn.Signature firstData;
+
+    bool secondIsValid;
+    WebAuthn.Signature secondData;
+
+    firstIsValid, firstData = castSignature(e, signature1);
 
+    secondIsValid, secondData = castSignature(e, signature2);
 
+    assert (getSha256(e, signature1) != getSha256(e, signature2)) &&
+    ((firstIsValid && secondIsValid)) => !compareSignatures(e, firstData, secondData);
+}