Merge pull request #15 from Certora/liav/more-reverting-conditions

Liav/more reverting conditions
safe-global · Jun 10, 2024 · 08594cc · 08594cc
2 parents 021d60d + dba6d97
commit 08594cc
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 2 deletions.
diff --git a/certora/confs/SafeWebAuthnSignerFactory.conf b/certora/confs/SafeWebAuthnSignerFactory.conf
@@ -3,7 +3,7 @@
     "files": [
         "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
-        "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"
+        "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
     ],
     "link": [
         "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton"

diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec
@@ -101,4 +101,17 @@ rule isValidSignatureForSignerConsistency()
 
     assert firstRevert == secondRevert;
     assert (!firstRevert && !secondRevert) => (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE());
-}
+}
+
+rule getSignerRevertingConditions {
+    env e;
+    uint256 x;
+    uint256 y;
+    P256.Verifiers verifiers;
+
+    bool triedTransferringEth = e.msg.value != 0;
+
+    getSigner@withrevert(e, x, y, verifiers);
+
+    assert lastReverted <=> triedTransferringEth;
+}
diff --git a/certora/specs/SafeWebAuthnSignerSingleton.spec b/certora/specs/SafeWebAuthnSignerSingleton.spec
@@ -121,3 +121,18 @@ rule verifyIsValidSignatureWillContinueToSucceed(){
     assert (!firstReverted && !secondRevert) => (firstVerified == secondVerify);
     satisfy true;
 }
+
+rule isValidSignatureRevertingConditions {
+    env e;
+    bytes32 message;
+
+    WebAuthn.Signature sigStruct;
+    bytes signature = WebAuthnHarness.encodeSignature(e, sigStruct);
+
+    bool triedTransferringEth = e.msg.value != 0;
+    bool dataLengthInsufficient = sigStruct.authenticatorData.length <= 32;
+
+    isValidSignature@withrevert(e, message, signature);
+
+    assert lastReverted <=> (triedTransferringEth || dataLengthInsufficient);
+}