Skip to content

Commit 908b586

Browse files
mmv08mmv08
committed
Merge branch 'main' of github.com:safe-global/safe-contracts into feat/memory-safe-assembly
2 parents 0c98fc0 + ad9b319 commit 908b586

File tree

11 files changed

+300
-4
lines changed

11 files changed

+300
-4
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

‎.github/workflows/cla.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ jobs:
1212
- name: "CLA Assistant"
1313
if: (github.event.comment.body == 'recheck' || github.event.comment.body == 'I have read the CLA Document and I hereby sign the CLA') || github.event_name == 'pull_request_target'
1414
# Beta Release
15-
uses: cla-assistant/github-action@v2.1.3-beta
15+
uses: cla-assistant/github-action@v2.3.0
1616
env:
1717
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
1818
# the below token should have repo scope and must be manually added by you in the repository's secret
@@ -33,4 +33,4 @@ jobs:
3333
#custom-pr-sign-comment: 'The signature to be committed in order to sign the CLA'
3434
#custom-allsigned-prcomment: 'pull request comment when all contributors has signed, defaults to **CLA Assistant Lite bot** All Contributors have signed the CLA.'
3535
#lock-pullrequest-aftermerge: false - if you don't want this bot to automatically lock the pull request after merging (default - true)
36-
#use-dco-flag: true - If you are using DCO instead of CLA
36+
#use-dco-flag: true - If you are using DCO instead of CLA

‎.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

‎CHANGELOG.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ This method uses the `CREATE` opcode, which is not counterfactual for a specific
107107

108108
If the initializer data is provided, the Factory now checks that the Singleton contract exists and the success of the call to avoid a proxy being deployed uninitialized
109109

110-
#### Add `createNetworkSpecificProxy`
110+
#### Add `createChainSpecificProxyWithNonce`
111111

112112
This method will use the chain id in the `CREATE2` salt; therefore, deploying a proxy to the same address on other networks is impossible.
113113
This method should enable the creation of proxies that should exist only on one network (e.g. specific governance or admin accounts)

‎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+
}

0 commit comments

Comments
 (0)