Signature Length Check FV

modules/4337/certora/conf/SignatureLengthCheck.conf

@@ -0,0 +1,15 @@
+{
+    "files": [
+        "certora/harnesses/Safe4337ModuleHarness.sol",
+        "certora/harnesses/Account.sol",
+    ],
+	"optimistic_loop": true,
+    "msg": "Safe4337Module: Signatures Length Check",
+    "rule_sanity": "basic",
+    "solc": "solc8.23",
+    "verify": "Safe4337ModuleHarness:certora/specs/SignatureLengthCheck.spec",
+    "packages": [
+        "@account-abstraction=../../node_modules/.pnpm/@account-abstraction+contracts@0.7.0/node_modules/@account-abstraction",
+        "@safe-global=../../node_modules/.pnpm/@safe-global+safe-contracts@1.4.1-build.0_ethers@6.13.1_bufferutil@4.0.8_utf-8-validate@5.0.10_/node_modules/@safe-global"
+    ]
+}

modules/4337/certora/harnesses/Account.sol

@@ -53,6 +53,95 @@ contract Account is Safe {
     function getValidUntilTimestamp(bytes calldata sigs) external pure returns (uint48) {
         return uint48(bytes6(sigs[6:12]));
     }
+
+    /*
+    Actual Signature:
+    "0x" +
+    "0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" +     // encoded EIP-1271 signature 1
+    "0000000000000000000000000000000000000000000000000000000000000002 0000000000000000000000000000000000000000000000000000000000000103 00" +     // encoded EIP-1271 signature 2
+    "0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000000147 00" +     // encoded EIP-1271 signature 3
+    "0000000000000000000000000000000000000000000000000000000000000004 00000000000000000000000000000000000000000000000000000000deadbeef"          // length of bytes + data of bytes of signature 1
+    "0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"  // length of bytes + data of bytes of signature 2
+    "0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000efbeef"          // length of bytes + data of bytes of signature 3
+
+    0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c30000000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000103000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000014700000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000efbeef
+
+    With Excess Data Type 1:
+    "0x" +
+    "0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" +                    // encoded EIP-1271 signature 1
+    "0000000000000000000000000000000000000000000000000000000000000002 0000000000000000000000000000000000000000000000000000000000000103 00" +                    // encoded EIP-1271 signature 2
+    "0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000000147 00" +                    // encoded EIP-1271 signature 3
+    "0000000000000000000000000000000000000000000000000000000000000008 00000000000000000000000000000000000000000000000000000000deadbeef"                         // length of bytes + data of bytes of signature 1
+    "0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"                 // length of bytes + data of bytes of signature 2
+    "0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000efbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 3 + excess data
+
+    0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c30000000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000103000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000014700000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000efbeefdeadbeefdeadbeefdeadbeef
+
+    With Excess Data Type 2:
+    "0x" +
+    "0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" +     // encoded EIP-1271 signature 1
+    "0000000000000000000000000000000000000000000000000000000000000002 0000000000000000000000000000000000000000000000000000000000000107 00" +     // encoded EIP-1271 signature 2
+    "0000000000000000000000000000000000000000000000000000000000000003 000000000000000000000000000000000000000000000000000000000000014b 00" +     // encoded EIP-1271 signature 3
+    "0000000000000000000000000000000000000000000000000000000000000008 00000000000000000000000000000000000000000000000000000000deadbeefdeadbeef"  // length of bytes + data of bytes of signature 1 + excess data
+    "0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"  // length of bytes + data of bytes of signature 2
+    "0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000efbeef"          // length of bytes + data of bytes of signature 3
+
+    0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c30000000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000107000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000014b00000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000deadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000efbeef
+
+    All three will have the same canonical hash: 0xe304234a47e4f89d0a95d9fafb42e9c3143e23e951d38add9f781c34f962deb7
+    */
+    function canonicalSignatureHash(bytes calldata signatures, uint256 threshold) public pure returns (bytes32 canonical) {
+        uint256 dynamicOffset = threshold * 0x41;
+        bytes memory staticPart = signatures[:dynamicOffset];
+        bytes memory dynamicPart = "";
+
+        for (uint256 i = 0; i < threshold; i++) {
+            uint256 ptr = i * 0x41;
+            uint8 v = uint8(signatures[ptr + 0x40]);
+
+            // Check to see if we have a smart contract signature, and if we do, then append
+            // the signature to the dynamic part.
+            if (v == 0) {
+                uint256 signatureOffset = uint256(bytes32(signatures[ptr + 0x20:]));
+                require(signatureOffset >= dynamicOffset, "Invalid signature offset");
+
+                uint256 signatureLength = uint256(bytes32(signatures[signatureOffset:]));
+                require(signatureLength > 0, "Invalid signature length");
+
+                bytes memory signature;
+                if (signatureLength < 0x20) {
+                    signature = signatures[signatureOffset+0x40-signatureLength:][:signatureLength];
+                }
+                else {
+                    signature = signatures[signatureOffset+0x20:][:signatureLength];
+                }
+
+                // Make sure to update the static part so that the smart contract signature
+                // points to the "canonical" signature offset (i.e. that all contract
+                // signatures are tightly packed one after the other in order). This ensures
+                // a canonical representation for the signatures.
+                /* solhint-disable no-inline-assembly */
+                assembly ("memory-safe") {
+                    mstore(add(staticPart, add(0x40, ptr)), dynamicOffset)
+                }
+                /* solhint-enable no-inline-assembly */
+                dynamicOffset += signatureLength + 0x20;
+                dynamicPart = abi.encodePacked(dynamicPart, signatureLength, signature);
+            }
+        }
+        canonical = keccak256(abi.encodePacked(staticPart, dynamicPart));
+    }
+
+    function containsContractSignature(bytes calldata signatures, uint256 threshold) public pure returns (bool) {
+        for (uint256 i = 0; i < threshold; i++) {
+            uint256 ptr = i * 0x41;
+            uint8 v = uint8(signatures[ptr + 0x40]);
+            if (v == 0) {
+                return true;
+            }
+        }
+        return false;
+    }
 }
 
 // @notice This is a harness contract for the rule that verfies the validation data

modules/4337/certora/harnesses/Safe4337ModuleHarness.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+pragma solidity >=0.8.0;
+import {Safe4337Module} from "./../../contracts/Safe4337Module.sol";
+
+contract Safe4337ModuleHarness is Safe4337Module {
+    constructor(address entryPoint) Safe4337Module(entryPoint) {}
+
+    function checkSignaturesLength(bytes calldata signatures, uint256 threshold) external pure returns (bool) {
+        return _checkSignaturesLength(signatures, threshold);
+    }
+
+    function combineBytes(bytes calldata signatures, bytes calldata data) external pure returns (bytes memory) {
+        return abi.encode(signatures, data);
+    }
+}

modules/4337/certora/specs/SignatureLengthCheck.spec

@@ -0,0 +1,27 @@
+using Account as safeContract;
+
+methods {
+    function checkSignaturesLength(bytes, uint256) external returns(bool) envfree;
+    function combineBytes(bytes, bytes) external returns(bytes) envfree;
+
+    // Safe Contract functions
+    function safeContract.containsContractSignature(bytes, uint256) external returns(bool) envfree;
+    function safeContract.canonicalSignatureHash(bytes, uint256) external returns(bytes32) envfree;
+}
+
+// This rule verifies that if excess data is added to the dynamic part of the signature, then the signature check will fail.
+rule signatureLengthCheckDirectly(bytes signatures, bytes gasGriefingData, uint256 threshold) {
+    require signatures.length > 0;
+    require gasGriefingData.length > 0;
+    assert checkSignaturesLength(signatures, threshold) => !checkSignaturesLength(combineBytes(signatures,gasGriefingData), threshold);
+}
+
+// This rule verifies that if excess data is added to the dynamic part of the signature, though it could pass in the safe contract's
+// `checkSignatures(...)`, it will be caught within the `_checkSignaturesLength(...)` call, as the dynamic length is checked.
+rule canonicalHashBasedLengthCheck(bytes signatures, bytes griefedSignatures, uint256 threshold) {
+    require safeContract.canonicalSignatureHash(signatures, threshold) == safeContract.canonicalSignatureHash(griefedSignatures, threshold);
+    require signatures.length < griefedSignatures.length;
+    require safeContract.containsContractSignature(signatures, threshold);
+
+    assert checkSignaturesLength(signatures, threshold) => !checkSignaturesLength(griefedSignatures, threshold);
+}