Merge pull request #4 from Certora/Singleton_Rules

Added all properties.

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"
 }

certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol

@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+pragma solidity >=0.8.0;
+
+import {SafeWebAuthnSignerSingleton} from "../../modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol";
+import {SignatureValidator} from "../../modules/passkey/contracts/base/SignatureValidator.sol";
+import {P256, WebAuthn} from "../../modules/passkey/contracts/libraries/WebAuthn.sol";
+
+/**
+ * @title Safe WebAuthn Signer Singleton
+ * @dev A singleton contract that implements WebAuthn signature verification. This singleton
+ * contract must be used with the specialized proxy {SafeWebAuthnSignerProxy}, as it encodes the
+ * credential configuration (public key coordinates and P-256 verifier to use) in calldata, which is
+ * required by this implementation.
+ * @custom:security-contact [email protected]
+ */
+contract SafeWebAuthnSignerSingletonHarness is SafeWebAuthnSignerSingleton {
+
+    function verifySignatureHarnessed(bytes32 message, bytes calldata signature) public view virtual returns (bool success) {
+        (uint256 x, uint256 y, P256.Verifiers verifiers) = getConfiguration();
+        success = WebAuthn.verifySignature(message, signature, WebAuthn.USER_VERIFICATION, x, y, verifiers);
+    }
+}

certora/specs/SafeWebAuthnSignerSingleton.spec

@@ -1,23 +1,110 @@
-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;
+}
+