diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 000000000..d51626537 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,53 @@ +name: certora + +on: + push: + branches: + - main + pull_request: + branches: + - main + + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v3 + + - name: Install python + uses: actions/setup-python@v4 + with: { python-version: 3.11 } + + - name: Install java + uses: actions/setup-java@v3 + with: { java-version: "17", java-package: jre, distribution: semeru } + + - name: Install certora cli-beta + run: pip install certora-cli-beta + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.7.6/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc7.6 + + - name: Verify rule ${{ matrix.rule }} + run: | + cd certora + touch applyHarness.patch + make munged + cd .. + echo "key length" ${#CERTORAKEY} + ./certora/scripts/${{ matrix.rule }} + env: + CERTORAKEY: ${{ secrets.CERTORA_KEY }} + + strategy: + fail-fast: false + max-parallel: 16 + matrix: + rule: + - verifySafe.sh diff --git a/.gitignore b/.gitignore index 18cdf9169..3d7b70cca 100644 --- a/.gitignore +++ b/.gitignore @@ -11,4 +11,9 @@ bin/ solc coverage/ coverage.json -yarn-error.log \ No newline at end of file +yarn-error.log + +# Certora Formal Verification related files +.certora_internal +.certora_recent_jobs.json +.zip-output-url.txt \ No newline at end of file diff --git a/certora/.gitignore b/certora/.gitignore new file mode 100644 index 000000000..284379223 --- /dev/null +++ b/certora/.gitignore @@ -0,0 +1 @@ +munged \ No newline at end of file diff --git a/certora/Makefile b/certora/Makefile new file mode 100644 index 000000000..2afda13d2 --- /dev/null +++ b/certora/Makefile @@ -0,0 +1,25 @@ +default: help + +PATCH = applyHarness.patch +CONTRACTS_DIR = ../contracts +MUNGED_DIR = munged + +help: + @echo "usage:" + @echo " make clean: remove all generated files (those ignored by git)" + @echo " make munged: create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)" + @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)" + +munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) + rm -rf $@ + cp -r $(CONTRACTS_DIR) $@ + patch -p0 -d $@ < $(PATCH) + +record: + diff -druN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH) + +refresh: munged record + +clean: + git clean -fdX + touch $(PATCH) diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch new file mode 100644 index 000000000..106c4562e --- /dev/null +++ b/certora/applyHarness.patch @@ -0,0 +1,24 @@ +diff -druN Safe.sol Safe.sol +--- Safe.sol 2023-04-11 15:01:13 ++++ Safe.sol 2023-04-11 15:01:55 +@@ -76,7 +76,7 @@ + * so we create a Safe with 0 owners and threshold 1. + * This is an unusable Safe, perfect for the singleton + */ +- threshold = 1; ++ // threshold = 1; MUNGED: remove and add to constructor of the harness + } + + /** +diff -druN base/Executor.sol base/Executor.sol +--- base/Executor.sol 2023-04-11 15:01:13 ++++ base/Executor.sol 2023-04-11 15:01:18 +@@ -25,6 +25,8 @@ + Enum.Operation operation, + uint256 txGas + ) internal returns (bool success) { ++ // MUNGED lets just be a bit more optimistic, `execute` does nothing and always returns true ++ return true; + if (operation == Enum.Operation.DelegateCall) { + // solhint-disable-next-line no-inline-assembly + assembly { diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol new file mode 100644 index 000000000..db95b3dcd --- /dev/null +++ b/certora/harnesses/SafeHarness.sol @@ -0,0 +1,22 @@ +// SPDX-License-Identifier: LGPL-3.0-only +import "../munged/Safe.sol"; + +contract SafeHarness is Safe { + constructor( + address[] memory _owners, + uint256 _threshold, + address to, + bytes memory data, + address fallbackHandler, + address paymentToken, + uint256 payment, + address payable paymentReceiver + ) { + this.setup(_owners, _threshold, to, data, fallbackHandler, paymentToken, payment, paymentReceiver); + } + + // harnessed getters + function getModule(address module) public view returns (address) { + return modules[module]; + } +} diff --git a/certora/scripts/verifySafe.sh b/certora/scripts/verifySafe.sh new file mode 100755 index 000000000..fd14d87fa --- /dev/null +++ b/certora/scripts/verifySafe.sh @@ -0,0 +1,19 @@ +#!/bin/bash + +params=("--send_only") + +if [[ -n "$CI" ]]; then + params=() +fi + +certoraRun certora/harnesses/SafeHarness.sol \ + --verify SafeHarness:certora/specs/Safe.spec \ + --solc solc7.6 \ + --optimistic_loop \ + --settings -optimisticFallback=true \ + --loop_iter 3 \ + --optimistic_hashing \ + --hashing_length_bound 352 \ + --rule_sanity \ + "${params[@]}" \ + --msg "Safe $1 " \ No newline at end of file diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec new file mode 100644 index 000000000..17950ca02 --- /dev/null +++ b/certora/specs/Safe.spec @@ -0,0 +1,84 @@ +methods { + // + function getThreshold() external returns (uint256) envfree; + function disableModule(address,address) external; + function nonce() external returns (uint256) envfree; + + // harnessed + function getModule(address) external returns (address) envfree; + + // optional + function execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation) external returns (bool, bytes memory); + function execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation) external returns (bool); + function execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes) external returns (bool); +} + +definition noHavoc(method f) returns bool = + f.selector != sig:execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation).selector + && f.selector != sig:execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation).selector + && f.selector != sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector; + +definition reachableOnly(method f) returns bool = + f.selector != sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector + && f.selector != sig:simulateAndRevert(address,bytes).selector; + +/// Nonce must never decrease +rule nonceMonotonicity(method f) filtered { + f -> noHavoc(f) && reachableOnly(f) +} { + uint256 nonceBefore = nonce(); + + calldataarg args; env e; + f(e, args); + + uint256 nonceAfter = nonce(); + + assert nonceAfter == nonceBefore || to_mathint(nonceAfter) == nonceBefore + 1; +} + + +/// The sentinel must never point to the zero address. +/// @notice It should either point to itself or some nonzero value +invariant liveSentinel() + getModule(1) != 0 + filtered { f -> noHavoc(f) && reachableOnly(f) } + { preserved { + requireInvariant noDeadEnds(getModule(1), 1); + }} + +/// Threshold must always be nonzero. +invariant nonzeroThreshold() + getThreshold() > 0 + filtered { f -> noHavoc(f) && reachableOnly(f) } + +/// Two different modules must not point to the same module/ +invariant uniquePrevs(address prev1, address prev2) + prev1 != prev2 && getModule(prev1) != 0 => getModule(prev1) != getModule(prev2) + filtered { f -> noHavoc(f) && reachableOnly(f) } + { + preserved { + requireInvariant noDeadEnds(getModule(prev1), prev1); + requireInvariant noDeadEnds(getModule(prev2), prev2); + requireInvariant uniquePrevs(prev1, 1); + requireInvariant uniquePrevs(prev2, 1); + requireInvariant uniquePrevs(prev1, getModule(prev2)); + requireInvariant uniquePrevs(prev2, getModule(prev1)); + } + } + +/// A module that points to the zero address must not have another module pointing to it. +invariant noDeadEnds(address dead, address lost) + dead != 0 && getModule(dead) == 0 => getModule(lost) != dead + filtered { f -> noHavoc(f) && reachableOnly(f) } + { + preserved { + requireInvariant liveSentinel(); + requireInvariant noDeadEnds(getModule(1), 1); + } + preserved disableModule(address prevModule, address module) with (env e) { + requireInvariant uniquePrevs(prevModule, lost); + requireInvariant uniquePrevs(prevModule, dead); + requireInvariant noDeadEnds(dead, module); + requireInvariant noDeadEnds(module, dead); + } + } \ No newline at end of file diff --git a/certora/specs/properties.md b/certora/specs/properties.md new file mode 100644 index 000000000..761112ec0 --- /dev/null +++ b/certora/specs/properties.md @@ -0,0 +1,63 @@ +# Safe Contract implementation properties + +## Reminder on property categories + +The categories are based on Certora's workshop [notes](https://github.com/Certora/Tutorials/blob/40ad7970bfafd081f6f416fe36b31981e48c6857/3DayWorkshop/SymbolicPool/properties.md). + +1. Valid states + Usually, there can be only one valid state at any given time. Such properties ensure the system is always in exactly one of its valid states. + +2. State transitions + Such properties verify the correctness of transactions between valid states. E.g., confirm valid states change according to their correct order or transitions only occur under the right conditions. + +3. Variable transitions + Similar to state transitions, but for variables. E.g., verify that Safe nonce is monotonically increasing. + +4. High-level properties + The most powerful type of properties covering the entire system. E.g., for any given operation, Safe threshold must remain lower or equal to the number of owners. + +5. Unit test + Such properties target specific function individually to verify their correctness. E.g., verify that a specific function can only be called by a specific address. + +6. Risk assessment + Such properties verify that worst cases that can happen to the system are handled correctly. E.g., verify that a transaction cannot be replayed. + +## Safe Contract Properties + +Verification doesn't hold for the `DELEGATECALL` operation. + +### Valid states + +### State transitions + +### Variable transitions + +### High-level properties + +### Unit test + +### Risk assessment + +- nonce monotonicity, it can only increase by 1 after execTransaction call + +- consistency of owner and module lists + +verify that `ownerCount` is in sync with the linked list. +always circular - each address for which `isModuleEnabled` returns true should be a part of the list + +- configuration changes to safe can only be done by the safe + who can swap owner? + module management + who should be able to? + +who should be allowed to make contract do delegate calls? +contract creator +address specified by contract creator + +- setup only be done once + +module states +enabled +cancelled + +execTransactionFromModuleReturnData