diff --git a/modules/4337/certora/conf/SignatureLengthCheck.conf b/modules/4337/certora/conf/SignatureLengthCheck.conf new file mode 100644 index 000000000..055bca8a5 --- /dev/null +++ b/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" + ] +} diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index 680111031..788881671 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/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 diff --git a/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol b/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol new file mode 100644 index 000000000..5552c88b0 --- /dev/null +++ b/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); + } +} diff --git a/modules/4337/certora/specs/SignatureLengthCheck.spec b/modules/4337/certora/specs/SignatureLengthCheck.spec new file mode 100644 index 000000000..ba80d9348 --- /dev/null +++ b/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); +}