Added all properties.

getConfiguration Integrity not done yet.
safe-global · May 20, 2024 · 4714c04 · 4714c04
1 parent 64a6083
commit 4714c04
Show file tree

Hide file tree

Showing 2 changed files with 138 additions and 27 deletions.
diff --git a/certora/confs/SafeWebAuthnSignerSingleton.conf b/certora/confs/SafeWebAuthnSignerSingleton.conf
@@ -1,14 +1,14 @@
 {
     "assert_autofinder_success": true,
     "files": [
+        "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
-        "certora/harnesses/ERC20Like/DummyWeth.sol",
-		"certora/harnesses/Utilities.sol",
+        "certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol",
     ],
     "java_args": [
         " -ea -Dlevel.setup.helpers=info"
     ],
-    "msg": "sanity_with_all_default_summaries",
+    "msg": "",
     "process": "emv",
     "prover_args": [
         " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on"
@@ -23,5 +23,5 @@
     "optimistic_hashing": true,
     "prover_version": "master",
     "server": "production",
-    "verify": "SafeWebAuthnSignerSingleton:certora/specs/SafeWebAuthnSignerSingleton.spec"
+    "verify": "SafeWebAuthnSignerSingletonHarness:certora/specs/SafeWebAuthnSignerSingleton.spec"
 }
diff --git a/certora/specs/SafeWebAuthnSignerSingleton.spec b/certora/specs/SafeWebAuthnSignerSingleton.spec
@@ -1,23 +1,134 @@
-import "ERC20/erc20cvl.spec";
-import "ERC20/WETHcvl.spec";
-import "ERC721/erc721.spec";
-import "ERC1967/erc1967.spec";
-import "PriceAggregators/chainlink.spec";
-import "PriceAggregators/tellor.spec";
-
-import "spec_utils/problems.spec";
-import "spec_utils/unresolved.spec";
-import "spec_utils/optimizations.spec";
-
-import "spec_utils/generic.spec"; // pick additional rules from here
-
-use builtin rule sanity filtered { f -> f.contract == currentContract }
-
-use builtin rule hasDelegateCalls filtered { f -> f.contract == currentContract }
-use builtin rule msgValueInLoopRule;
-use builtin rule viewReentrancy;
-use rule privilegedOperation filtered { f -> f.contract == currentContract }
-use rule timeoutChecker filtered { f -> f.contract == currentContract }
-use rule simpleFrontRunning filtered { f -> f.contract == currentContract }
-use rule noRevert filtered { f -> f.contract == currentContract }
-use rule alwaysRevert filtered { f -> f.contract == currentContract }
+// import "ERC20/erc20cvl.spec";
+// import "ERC20/WETHcvl.spec";
+// import "ERC721/erc721.spec";
+// import "ERC1967/erc1967.spec";
+// import "PriceAggregators/chainlink.spec";
+// import "PriceAggregators/tellor.spec";
+
+// import "spec_utils/problems.spec";
+// import "spec_utils/unresolved.spec";
+// import "spec_utils/optimizations.spec";
+
+// import "spec_utils/generic.spec"; // pick additional rules from here
+
+// use builtin rule sanity filtered { f -> f.contract == currentContract }
+
+// use builtin rule hasDelegateCalls filtered { f -> f.contract == currentContract }
+// use builtin rule msgValueInLoopRule;
+// use builtin rule viewReentrancy;
+// use rule privilegedOperation filtered { f -> f.contract == currentContract }
+// use rule timeoutChecker filtered { f -> f.contract == currentContract }
+// use rule simpleFrontRunning filtered { f -> f.contract == currentContract }
+// use rule noRevert filtered { f -> f.contract == currentContract }
+// use rule alwaysRevert filtered { f -> f.contract == currentContract }
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Implementation of _verifySignature Function (Integrity)                                                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+rule verifySignatureIntegrity(env e){
+    bytes32 first_message;
+    bytes signature;
+
+    bool first_message_verified = verifySignatureHarnessed(e, first_message, signature);
+
+    bytes32 second_message;
+    bool second_message_verified = verifySignatureHarnessed(e, second_message, signature);
+
+    assert (first_message_verified == true && second_message_verified == true) => first_message == second_message;
+    assert first_message == second_message => first_message_verified == second_message_verified;
+}
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ getConfiguration Function (Integrity)                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+// TODO Not Completed Yet
+// rule verifyGetConfigurationIntegrity(env e){
+
+//     uint256 x;
+//     uint256 y;
+//     P256.Verifiers verifiers;
+//     uint256 new_x; uint256 new_y; P256.Verifiers new_verifiers;
+//     bytes32 message;
+
+//     // bytes data = assignValues(e, x, y, verifiers);
+//     (new_x, new_y, new_verifiers) = temp(e, x, y, verifiers);
+
+//     // (x, y, verifiers) = getConfiguration(e);
+//     // (new_x, new_y, new_verifiers) = getConfigurationHarnessed(e, data);
+
+//     assert x == new_x;
+//     assert y == new_y;
+//     assert verifiers == new_verifiers;
+//     satisfy true;
+// }
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Both is valid Signature behave the same way                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+rule verifyIsValidSignatureAreEqual(env e){
+    bytes data;
+    bytes first_signature;
+
+    bool hashed_data_verified = verifySignatureHarnessed(e, keccak256(data), first_signature);
+
+    bytes second_signature;
+    bytes32 message;
+    bool message_verified = verifySignatureHarnessed(e, message, second_signature);
+
+    assert (hashed_data_verified == true && message_verified == true) => message == keccak256(data);
+    assert message == keccak256(data) => hashed_data_verified == message_verified;
+}
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Once signer passed isValidSignature it will never fail on it after any call                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+rule verifyIsValidSignatureWillContinueToSucceed(env e){
+    bytes32 message;
+    bytes signature;
+
+    bool first_verified = verifySignatureHarnessed(e, message, signature);
+    require first_verified == true;
+
+    bool second_verified = verifySignatureHarnessed(e, message, signature);
+    assert second_verified;
+}
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Once isValidSignature failed, it will never pass before createSigner called                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+rule IsValidSignatureMustSucceedAfterCreation(env e){
+    method f;
+    calldataarg args;
+
+    bytes32 message;
+    bytes signature;
+
+    bool first_verified = verifySignatureHarnessed(e, message, signature);
+    require !first_verified;
+
+    f(e, args);
+
+
+    bool second_verified = verifySignatureHarnessed(e, message, signature);
+    assert second_verified => f.selector == sig:SafeWebAuthnSignerFactory.createSigner(uint256, uint256, P256.Verifiers).selector;
+}
+