From 99c9c6c32288b6aedbe97695bd038e2363516ccd Mon Sep 17 00:00:00 2001
From: yoavelmalem <yoav.el@certora.com>
Date: Sun, 23 Jun 2024 11:39:42 +0300
Subject: [PATCH] Added getConfiguration Rule

---
 certora/confs/GetConfigurationConf.conf       | 26 +++++++++++++++
 certora/harnesses/Utilities.sol               | 11 +++++++
 certora/specs/GetConfigurationSpec.spec       | 33 +++++++++++++++++++
 .../contracts/SafeWebAuthnSignerSingleton.sol |  4 ++-
 4 files changed, 73 insertions(+), 1 deletion(-)
 create mode 100644 certora/confs/GetConfigurationConf.conf
 create mode 100644 certora/specs/GetConfigurationSpec.spec

diff --git a/certora/confs/GetConfigurationConf.conf b/certora/confs/GetConfigurationConf.conf
new file mode 100644
index 000000000..deb5baf35
--- /dev/null
+++ b/certora/confs/GetConfigurationConf.conf
@@ -0,0 +1,26 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
+		"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
+		"certora/harnesses/Utilities.sol",
+		"modules/passkey/contracts/libraries/P256.sol"
+    ],
+    "link": [
+        "SafeWebAuthnSignerProxy:_VERIFIERS=P256",
+		"SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton"
+    ],
+    "packages":[
+        "@safe-global=node_modules/@safe-global",
+        "@account-abstraction=node_modules/@account-abstraction"
+    ],
+    "solc": "solc8.23",
+    "rule_sanity": "basic",
+    "solc_via_ir": false,
+    "optimistic_loop": true,
+    "loop_iter": "6",
+    "optimistic_hashing": true,
+    "prover_version": "jtoman/CERT-6221",
+    "server": "production",
+    "verify": "SafeWebAuthnSignerProxy:certora/specs/GetConfigurationSpec.spec"
+}
\ No newline at end of file
diff --git a/certora/harnesses/Utilities.sol b/certora/harnesses/Utilities.sol
index 608595af7..49ffd8cbc 100644
--- a/certora/harnesses/Utilities.sol
+++ b/certora/harnesses/Utilities.sol
@@ -1,3 +1,10 @@
+import {P256} from "../../modules/passkey/contracts/libraries/WebAuthn.sol";
+
+
+interface IConfigHolder {
+    function getConfiguration() external pure returns (uint256 x, uint256 y, P256.Verifiers verifiers);
+}
+
 contract Utilities {
     function havocAll() external {
         (bool success, ) = address(0xdeadbeef).call(abi.encodeWithSelector(0x12345678));
@@ -7,4 +14,8 @@ contract Utilities {
     function justRevert() external {
         revert();
     }
+
+    function getConfiguration(address proxy) external view returns (uint256 x, uint256 y, P256.Verifiers verifiers) {
+        return IConfigHolder(proxy).getConfiguration();
+    }
 }
\ No newline at end of file
diff --git a/certora/specs/GetConfigurationSpec.spec b/certora/specs/GetConfigurationSpec.spec
new file mode 100644
index 000000000..75f03311f
--- /dev/null
+++ b/certora/specs/GetConfigurationSpec.spec
@@ -0,0 +1,33 @@
+using Utilities as utilities;
+using SafeWebAuthnSignerProxy as proxy;
+
+methods {
+    function _._ external => DISPATCH [ SafeWebAuthnSignerProxy._, SafeWebAuthnSignerSingleton._ ] default HAVOC_ALL;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ getConfiguration Function (Integrity)                                                                               │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+rule configGetConfiguration {
+    env e;
+
+    uint256 xBefore = currentContract._X;
+    uint256 yBefore = currentContract._Y;
+    P256.Verifiers verifiersBefore = currentContract._VERIFIERS;
+
+    uint256 xAfter;
+    uint256 yAfter;
+    P256.Verifiers verifiersAfter;
+
+    xAfter, yAfter, verifiersAfter = utilities.getConfiguration(e, proxy);
+
+
+    assert xBefore == xAfter &&
+           yBefore == yAfter &&
+           verifiersBefore == verifiersAfter;
+    satisfy true;
+}
+
diff --git a/modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol b/modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol
index 799f5450a..d83d8bbf7 100644
--- a/modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol
+++ b/modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol
@@ -31,10 +31,12 @@ contract SafeWebAuthnSignerSingleton is SignatureValidator {
      */
     function getConfiguration() public pure returns (uint256 x, uint256 y, P256.Verifiers verifiers) {
         // solhint-disable-next-line no-inline-assembly
+        uint256 mask = type(uint176).max;
         assembly ("memory-safe") {
             x := calldataload(sub(calldatasize(), 86))
             y := calldataload(sub(calldatasize(), 54))
-            verifiers := shr(80, calldataload(sub(calldatasize(), 22)))
+            // verifiers := shr(80, calldataload(sub(calldatasize(), 22)))
+            verifiers := and(mask, calldataload(sub(calldatasize(), 32)))
         }
     }
 }