Signature Length Check FV (#464)

Closes #461 

This PR adds a rule which verifies that the signature length check is
ensured using the `_checkSignaturesLength(...)` in the `Safe4337Module`.

The rule ensures that a signature that the bundler could manipulate,
which could clear the check in Safe using `checkSignatures(...)` will
still get caught using the `_checkSignaturesLength(...)`. For this, we
use a `canonicalSignatureHash(...)` which generates the same hash for
valid signatures, with and without the excess data. An example is added
to show this case before the function is written.

Also have added the workflow for checking the same in CI (Currently, it
uses a script, which will be modified in a later PR to be consistent
with our other repos).

.github/workflows/certora_4337.yml

@@ -19,7 +19,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        rule: ['verify4337Module.sh', 'verifyTransactionExecutionMethods.sh', 'verifyValidationData.sh']
+        rule: ['verify4337Module.sh', 'verifyTransactionExecutionMethods.sh', 'verifyValidationData.sh', 'verifySignatureLengthCheck.sh']
     steps:
       - uses: actions/checkout@v3
 

modules/4337/certora/conf/SignatureLengthCheck.conf

@@ -0,0 +1,16 @@
+{
+    "files": [
+        "certora/harnesses/Safe4337ModuleHarness.sol",
+        "certora/harnesses/Account.sol",
+    ],
+    "loop_iter": "3",
+    "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,45 @@ contract Account is Safe {
     function getValidUntilTimestamp(bytes calldata sigs) external pure returns (uint48) {
         return uint48(bytes6(sigs[6:12]));
     }
+
+    /**
+     * @dev This function encodes signature in a canonical format. This is required for formal verification.
+     * The canonical format ensures the signatures are tightly packed one after the other in order.
+     *
+     * For more details on signature encoding: https://docs.safe.global/advanced/smart-account-signatures
+    */
+    function canonicalSignature(bytes calldata signatures, uint256 safeThreshold) public pure returns (bytes memory canonical) {
+        uint256 dynamicOffset = safeThreshold * 0x41;
+        bytes memory staticPart = signatures[:dynamicOffset];
+        bytes memory dynamicPart = "";
+
+        for (uint256 i = 0; i < safeThreshold; 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:]));
+
+                uint256 signatureLength = uint256(bytes32(signatures[signatureOffset:]));
+                bytes memory 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 = abi.encodePacked(staticPart, dynamicPart);
+    }    
 }
 
 // @notice This is a harness contract for the rule that verfies the validation data

modules/4337/certora/harnesses/Safe4337ModuleHarness.sol

@@ -0,0 +1,11 @@
+// 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);
+    }
+}

modules/4337/certora/scripts/verifySignatureLengthCheck.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+params=()
+
+if [[ -n "$CI" ]]; then
+    params=("--wait_for_results")
+fi
+
+certoraRun certora/conf/SignatureLengthCheck.conf \
+    "${params[@]}" \
+    "$@"
+

modules/4337/certora/specs/SignatureLengthCheck.spec

@@ -0,0 +1,15 @@
+using Account as safeContract;
+
+methods {
+    function checkSignaturesLength(bytes, uint256) external returns(bool) envfree;
+
+    // Safe Contract functions
+    function safeContract.canonicalSignature(bytes, uint256) external returns(bytes) envfree;
+}
+
+// This rule verifies that if excess data is added to 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 signatureCannotBeLongerThanCanonicalEncoding(bytes signatures, uint256 threshold) {
+    bytes canonical = safeContract.canonicalSignature(signatures, threshold);
+    assert checkSignaturesLength(signatures, threshold) => signatures.length <= canonical.length;
+}