Skip to content

Commit ad9b319

Browse files
mmv08mmv08
authored
Merge pull request #560 from safe-global/formal-verification
Bootstrap formal verification setup
2 parents 4b9c46f + c8932d4 commit ad9b319

File tree

9 files changed

+297
-1
lines changed

9 files changed

+297
-1
lines changed

‎.github/workflows/certora.yml‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
name: certora
2+
3+
on:
4+
push:
5+
branches:
6+
- main
7+
pull_request:
8+
branches:
9+
- main
10+
11+
workflow_dispatch:
12+
13+
jobs:
14+
verify:
15+
runs-on: ubuntu-latest
16+
17+
steps:
18+
- uses: actions/checkout@v3
19+
20+
- name: Install python
21+
uses: actions/setup-python@v4
22+
with: { python-version: 3.11 }
23+
24+
- name: Install java
25+
uses: actions/setup-java@v3
26+
with: { java-version: "17", java-package: jre, distribution: semeru }
27+
28+
- name: Install certora cli-beta
29+
run: pip install certora-cli-beta
30+
31+
- name: Install solc
32+
run: |
33+
wget https://github.com/ethereum/solidity/releases/download/v0.7.6/solc-static-linux
34+
chmod +x solc-static-linux
35+
sudo mv solc-static-linux /usr/local/bin/solc7.6
36+
37+
- name: Verify rule ${{ matrix.rule }}
38+
run: |
39+
cd certora
40+
touch applyHarness.patch
41+
make munged
42+
cd ..
43+
echo "key length" ${#CERTORAKEY}
44+
./certora/scripts/${{ matrix.rule }}
45+
env:
46+
CERTORAKEY: ${{ secrets.CERTORA_KEY }}
47+
48+
strategy:
49+
fail-fast: false
50+
max-parallel: 16
51+
matrix:
52+
rule:
53+
- verifySafe.sh

‎.gitignore‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,4 +11,9 @@ bin/
1111
solc
1212
coverage/
1313
coverage.json
14-
yarn-error.log
14+
yarn-error.log
15+
16+
# Certora Formal Verification related files
17+
.certora_internal
18+
.certora_recent_jobs.json
19+
.zip-output-url.txt

‎certora/.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
munged

‎certora/Makefile‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
default: help
2+
3+
PATCH = applyHarness.patch
4+
CONTRACTS_DIR = ../contracts
5+
MUNGED_DIR = munged
6+
7+
help:
8+
@echo "usage:"
9+
@echo " make clean: remove all generated files (those ignored by git)"
10+
@echo " make munged: create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
11+
@echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
12+
13+
munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
14+
rm -rf $@
15+
cp -r $(CONTRACTS_DIR) $@
16+
patch -p0 -d $@ < $(PATCH)
17+
18+
record:
19+
diff -druN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
20+
21+
refresh: munged record
22+
23+
clean:
24+
git clean -fdX
25+
touch $(PATCH)

‎certora/applyHarness.patch‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
diff -druN Safe.sol Safe.sol
2+
--- Safe.sol 2023-04-11 15:01:13
3+
+++ Safe.sol 2023-04-11 15:01:55
4+
@@ -76,7 +76,7 @@
5+
* so we create a Safe with 0 owners and threshold 1.
6+
* This is an unusable Safe, perfect for the singleton
7+
*/
8+
- threshold = 1;
9+
+ // threshold = 1; MUNGED: remove and add to constructor of the harness
10+
}
11+
12+
/**
13+
diff -druN base/Executor.sol base/Executor.sol
14+
--- base/Executor.sol 2023-04-11 15:01:13
15+
+++ base/Executor.sol 2023-04-11 15:01:18
16+
@@ -25,6 +25,8 @@
17+
Enum.Operation operation,
18+
uint256 txGas
19+
) internal returns (bool success) {
20+
+ // MUNGED lets just be a bit more optimistic, `execute` does nothing and always returns true
21+
+ return true;
22+
if (operation == Enum.Operation.DelegateCall) {
23+
// solhint-disable-next-line no-inline-assembly
24+
assembly {

‎certora/harnesses/SafeHarness.sol‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// SPDX-License-Identifier: LGPL-3.0-only
2+
import "../munged/Safe.sol";
3+
4+
contract SafeHarness is Safe {
5+
constructor(
6+
address[] memory _owners,
7+
uint256 _threshold,
8+
address to,
9+
bytes memory data,
10+
address fallbackHandler,
11+
address paymentToken,
12+
uint256 payment,
13+
address payable paymentReceiver
14+
) {
15+
this.setup(_owners, _threshold, to, data, fallbackHandler, paymentToken, payment, paymentReceiver);
16+
}
17+
18+
// harnessed getters
19+
function getModule(address module) public view returns (address) {
20+
return modules[module];
21+
}
22+
}

‎certora/scripts/verifySafe.sh‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
#!/bin/bash
2+
3+
params=("--send_only")
4+
5+
if [[ -n "$CI" ]]; then
6+
params=()
7+
fi
8+
9+
certoraRun certora/harnesses/SafeHarness.sol \
10+
--verify SafeHarness:certora/specs/Safe.spec \
11+
--solc solc7.6 \
12+
--optimistic_loop \
13+
--settings -optimisticFallback=true \
14+
--loop_iter 3 \
15+
--optimistic_hashing \
16+
--hashing_length_bound 352 \
17+
--rule_sanity \
18+
"${params[@]}" \
19+
--msg "Safe $1 "

‎certora/specs/Safe.spec‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
methods {
2+
//
3+
function getThreshold() external returns (uint256) envfree;
4+
function disableModule(address,address) external;
5+
function nonce() external returns (uint256) envfree;
6+
7+
// harnessed
8+
function getModule(address) external returns (address) envfree;
9+
10+
// optional
11+
function execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation) external returns (bool, bytes memory);
12+
function execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation) external returns (bool);
13+
function execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes) external returns (bool);
14+
}
15+
16+
definition noHavoc(method f) returns bool =
17+
f.selector != sig:execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation).selector
18+
&& f.selector != sig:execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation).selector
19+
&& f.selector != sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector;
20+
21+
definition reachableOnly(method f) returns bool =
22+
f.selector != sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector
23+
&& f.selector != sig:simulateAndRevert(address,bytes).selector;
24+
25+
/// Nonce must never decrease
26+
rule nonceMonotonicity(method f) filtered {
27+
f -> noHavoc(f) && reachableOnly(f)
28+
} {
29+
uint256 nonceBefore = nonce();
30+
31+
calldataarg args; env e;
32+
f(e, args);
33+
34+
uint256 nonceAfter = nonce();
35+
36+
assert nonceAfter == nonceBefore || to_mathint(nonceAfter) == nonceBefore + 1;
37+
}
38+
39+
40+
/// The sentinel must never point to the zero address.
41+
/// @notice It should either point to itself or some nonzero value
42+
invariant liveSentinel()
43+
getModule(1) != 0
44+
filtered { f -> noHavoc(f) && reachableOnly(f) }
45+
{ preserved {
46+
requireInvariant noDeadEnds(getModule(1), 1);
47+
}}
48+
49+
/// Threshold must always be nonzero.
50+
invariant nonzeroThreshold()
51+
getThreshold() > 0
52+
filtered { f -> noHavoc(f) && reachableOnly(f) }
53+
54+
/// Two different modules must not point to the same module/
55+
invariant uniquePrevs(address prev1, address prev2)
56+
prev1 != prev2 && getModule(prev1) != 0 => getModule(prev1) != getModule(prev2)
57+
filtered { f -> noHavoc(f) && reachableOnly(f) }
58+
{
59+
preserved {
60+
requireInvariant noDeadEnds(getModule(prev1), prev1);
61+
requireInvariant noDeadEnds(getModule(prev2), prev2);
62+
requireInvariant uniquePrevs(prev1, 1);
63+
requireInvariant uniquePrevs(prev2, 1);
64+
requireInvariant uniquePrevs(prev1, getModule(prev2));
65+
requireInvariant uniquePrevs(prev2, getModule(prev1));
66+
}
67+
}
68+
69+
/// A module that points to the zero address must not have another module pointing to it.
70+
invariant noDeadEnds(address dead, address lost)
71+
dead != 0 && getModule(dead) == 0 => getModule(lost) != dead
72+
filtered { f -> noHavoc(f) && reachableOnly(f) }
73+
{
74+
preserved {
75+
requireInvariant liveSentinel();
76+
requireInvariant noDeadEnds(getModule(1), 1);
77+
}
78+
preserved disableModule(address prevModule, address module) with (env e) {
79+
requireInvariant uniquePrevs(prevModule, lost);
80+
requireInvariant uniquePrevs(prevModule, dead);
81+
requireInvariant noDeadEnds(dead, module);
82+
requireInvariant noDeadEnds(module, dead);
83+
}
84+
}

‎certora/specs/properties.md‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
# Safe Contract implementation properties
2+
3+
## Reminder on property categories
4+
5+
The categories are based on Certora's workshop [notes](https://github.com/Certora/Tutorials/blob/40ad7970bfafd081f6f416fe36b31981e48c6857/3DayWorkshop/SymbolicPool/properties.md).
6+
7+
1. Valid states
8+
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.
9+
10+
2. State transitions
11+
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.
12+
13+
3. Variable transitions
14+
Similar to state transitions, but for variables. E.g., verify that Safe nonce is monotonically increasing.
15+
16+
4. High-level properties
17+
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.
18+
19+
5. Unit test
20+
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.
21+
22+
6. Risk assessment
23+
Such properties verify that worst cases that can happen to the system are handled correctly. E.g., verify that a transaction cannot be replayed.
24+
25+
## Safe Contract Properties
26+
27+
Verification doesn't hold for the `DELEGATECALL` operation.
28+
29+
### Valid states
30+
31+
### State transitions
32+
33+
### Variable transitions
34+
35+
### High-level properties
36+
37+
### Unit test
38+
39+
### Risk assessment
40+
41+
- nonce monotonicity, it can only increase by 1 after execTransaction call
42+
43+
- consistency of owner and module lists
44+
45+
verify that `ownerCount` is in sync with the linked list.
46+
always circular - each address for which `isModuleEnabled` returns true should be a part of the list
47+
48+
- configuration changes to safe can only be done by the safe
49+
who can swap owner?
50+
module management
51+
who should be able to?
52+
53+
who should be allowed to make contract do delegate calls?
54+
contract creator
55+
address specified by contract creator
56+
57+
- setup only be done once
58+
59+
module states
60+
enabled
61+
cancelled
62+
63+
execTransactionFromModuleReturnData

0 commit comments

Comments
 (0)