Added getConfiguration Rule

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

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();
+    }
 }

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;
+}
+

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