From 3f0e7b57ba8415a535ffd399b51fb70217990bb9 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Thu, 18 Jul 2024 13:12:48 +0200 Subject: [PATCH] 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 | 2 +- .../certora/conf/SignatureLengthCheck.conf | 16 ++++++++ modules/4337/certora/harnesses/Account.sol | 39 +++++++++++++++++++ .../harnesses/Safe4337ModuleHarness.sol | 11 ++++++ .../scripts/verifySignatureLengthCheck.sh | 12 ++++++ .../certora/specs/SignatureLengthCheck.spec | 15 +++++++ 6 files changed, 94 insertions(+), 1 deletion(-) create mode 100644 modules/4337/certora/conf/SignatureLengthCheck.conf create mode 100644 modules/4337/certora/harnesses/Safe4337ModuleHarness.sol create mode 100755 modules/4337/certora/scripts/verifySignatureLengthCheck.sh create mode 100644 modules/4337/certora/specs/SignatureLengthCheck.spec diff --git a/.github/workflows/certora_4337.yml b/.github/workflows/certora_4337.yml index d6dd5c0e..510c2c78 100644 --- a/.github/workflows/certora_4337.yml +++ b/.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 diff --git a/modules/4337/certora/conf/SignatureLengthCheck.conf b/modules/4337/certora/conf/SignatureLengthCheck.conf new file mode 100644 index 00000000..b7090c48 --- /dev/null +++ b/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" + ] +} diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index 68011103..d0e95125 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/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 diff --git a/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol b/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol new file mode 100644 index 00000000..f3253048 --- /dev/null +++ b/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); + } +} diff --git a/modules/4337/certora/scripts/verifySignatureLengthCheck.sh b/modules/4337/certora/scripts/verifySignatureLengthCheck.sh new file mode 100755 index 00000000..702f55fe --- /dev/null +++ b/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[@]}" \ + "$@" + diff --git a/modules/4337/certora/specs/SignatureLengthCheck.spec b/modules/4337/certora/specs/SignatureLengthCheck.spec new file mode 100644 index 00000000..119e5881 --- /dev/null +++ b/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; +}