Skip to content

Commit bd73de3

Browse files
colin-morphocolin-morpho
authored
Merge pull request #178 from morpho-org/colin@verif/bundler-safety
[Certora] Check Bundler safety
2 parents 4db02f2 + f5c5cc6 commit bd73de3

File tree

9 files changed

+272
-0
lines changed

9 files changed

+272
-0
lines changed

‎.github/actions/install/action.yml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,3 +17,6 @@ runs:
1717
restore-keys: |
1818
forge-${{ github.base_ref }}
1919
forge-
20+
21+
- name: Install jq
22+
uses: sergeysova/jq-action@v2

‎.github/workflows/certora.yml

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
name: Certora
2+
3+
on:
4+
push:
5+
branches:
6+
- main
7+
pull_request:
8+
workflow_dispatch:
9+
10+
jobs:
11+
verify:
12+
runs-on: ubuntu-latest
13+
14+
strategy:
15+
fail-fast: false
16+
17+
matrix:
18+
conf:
19+
- Bundler
20+
21+
steps:
22+
- uses: actions/checkout@v4
23+
with:
24+
submodules: recursive
25+
26+
- name: Install python
27+
uses: actions/setup-python@v5
28+
with:
29+
python-version: ">=3.11"
30+
31+
- name: Install certora
32+
run: pip install certora-cli
33+
34+
- name: Install solc (0.8.28)
35+
run: |
36+
wget https://github.com/ethereum/solidity/releases/download/v0.8.28/solc-static-linux
37+
chmod +x solc-static-linux
38+
sudo mv solc-static-linux /usr/local/bin/solc-0.8.28
39+
40+
- name: Apply munging
41+
run: make -C certora munged
42+
43+
- name: Verify ${{ matrix.conf }} specification
44+
run: certoraRun certora/confs/${{ matrix.conf }}.conf
45+
env:
46+
CERTORAKEY: ${{ secrets.CERTORAKEY }}

‎.github/workflows/formatting.yml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,3 +23,5 @@ jobs:
2323

2424
- name: Run Linter
2525
run: find ./ -type f -name '*.sol' -exec perl -pi -e 's/transient //g' {} + && forge fmt --check
26+
- name: Run Certora Config Linter
27+
run: for file in certora/confs/*.conf; do diff <(jq < "$file") "$file"; done

‎.gitignore

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,3 +21,7 @@ data/
2121
broadcast/
2222

2323
*.log
24+
25+
# Certora
26+
.certora_internal
27+
munged/

‎certora/Makefile

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
munged: ../munged
2+
3+
../munged: $(wildcard ../src/*.sol) applyMunging.patch
4+
@rm -rf ../munged
5+
@cp -r ../src ../munged
6+
@patch -p0 -d ../munged < applyMunging.patch
7+
8+
record:
9+
diff -ruN ../src ../munged | sed -E 's,\.\./src/|\.\./munged/,,g' | sed -E 's,((\-\-\-|\+\+\+) [^[:space:]]*).*,\1,' > applyMunging.patch
10+
11+
clean:
12+
rm -rf ../munged
13+
14+
.PHONY: clean record munged # Do not add ../munged here, as it is useful to protect munged edits

‎certora/README.md

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
# Bundler V3 formal verification
2+
3+
This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index.html) specification and verification setup for the [Bundler](../src/Bunlder.sol) V3.
4+
5+
## Getting started
6+
7+
The verification is performed on modified source files, which can generated with the command:
8+
9+
```
10+
make -C certora munged
11+
```
12+
13+
This project depends on several [Solidity](https://soliditylang.org/) versions which are required for running the verification.
14+
The compiler binaries should be available at the paths:
15+
16+
- `solc-0.8.19` for the solidity compiler version `0.8.19`;
17+
- `solc-0.8.28` for the solidity compiler version `0.8.28`.
18+
19+
To verify a specification, run the command `certoraRun Spec.conf` where `Spec.conf` is the configuration file of the matching CVL specification.
20+
Configuration files are available in [`certora/confs`](confs).
21+
Please ensure that `CERTORAKEY` is set up in your environment.
22+
23+
## Overview
24+
25+
The Bundler contract enables an EOA to call different endpoint contracts onchain as well as grouping several calls in a single bundle.
26+
These calls may themselves reenter the bundler.
27+
28+
### Bundler
29+
30+
This is checked in [`Bundler.spec`](specs/Bundler.spec).
31+
32+
## Verification architecture
33+
34+
### Folders and file structure
35+
36+
The [`certora/specs`](specs) folder contains the following files:
37+
38+
- [`Bundler.spec`](specs/Bundler.spec) checks that Bundler entry points behave as expected.
39+
40+
The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
41+
42+
The [`certora/Makefile`](Makefile) is used to track and perform the required modifications on source files.

‎certora/applyMunging.patch

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
diff -ruN Bundler.sol Bundler.sol
2+
--- Bundler.sol
3+
+++ Bundler.sol
4+
@@ -15,10 +15,37 @@
5+
/* TRANSIENT STORAGE */
6+
7+
/// @notice The initiator of the multicall transaction.
8+
- address public transient initiator;
9+
+ //address public transient initiator;
10+
+ function setInitiator(address _initiator) internal {
11+
+ assembly ("memory-safe") {
12+
+ // keccak256("Morpho Bundler Initiator Slot")
13+
+ tstore(0x33a59cbcc71c90d612d5afca82f27022cd1319f49b953968504d8209c045bd1f, _initiator)
14+
+ }
15+
+ }
16+
+
17+
+ function initiator() public view returns (address _initiator) {
18+
+ assembly ("memory-safe") {
19+
+ // keccak256("Morpho Bundler Initiator Slot")
20+
+ _initiator := tload(0x33a59cbcc71c90d612d5afca82f27022cd1319f49b953968504d8209c045bd1f)
21+
+ }
22+
+ }
23+
24+
/// @notice Hash of the concatenation of the sender and the hash of the calldata of the next call to `reenter`.
25+
- bytes32 public transient reenterHash;
26+
+ //bytes32 public transient reenterHash;
27+
+
28+
+ function setReenterHash(bytes32 _reenterHash) internal {
29+
+ assembly ("memory-safe") {
30+
+ // keccak256("Morpho Bundler Reenter Hash Slot")
31+
+ tstore(0xf76fe07d24a8fe20766ea4a3e6e9805bd23d7cda61e69a0df6c4774484a4adf8, _reenterHash)
32+
+ }
33+
+ }
34+
+
35+
+ function reenterHash() public view returns (bytes32 _reenterHash) {
36+
+ assembly ("memory-safe") {
37+
+ // keccak256("Morpho Bundler Reenter Hash Slot")
38+
+ _reenterHash := tload(0xf76fe07d24a8fe20766ea4a3e6e9805bd23d7cda61e69a0df6c4774484a4adf8)
39+
+ }
40+
+ }
41+
42+
/* EXTERNAL */
43+
44+
@@ -26,13 +53,13 @@
45+
/// @dev Locks the initiator so that the sender can be identified by other contracts.
46+
/// @param bundle The ordered array of calldata to execute.
47+
function multicall(Call[] calldata bundle) external payable {
48+
- require(initiator == address(0), ErrorsLib.AlreadyInitiated());
49+
+ require(initiator() == address(0), ErrorsLib.AlreadyInitiated());
50+
51+
- initiator = msg.sender;
52+
+ setInitiator(msg.sender);
53+
54+
_multicall(bundle);
55+
56+
- initiator = address(0);
57+
+ setInitiator(address(0));
58+
}
59+
60+
/// @notice Executes a sequence of calls.
61+
@@ -41,7 +68,7 @@
62+
/// @param bundle The ordered array of calldata to execute.
63+
function reenter(Call[] calldata bundle) external {
64+
require(
65+
- reenterHash == keccak256(bytes.concat(bytes20(msg.sender), keccak256(msg.data[4:]))),
66+
+ reenterHash() == keccak256(bytes.concat(bytes20(msg.sender), keccak256(msg.data[4:]))),
67+
ErrorsLib.IncorrectReenterHash()
68+
);
69+
_multicall(bundle);
70+
@@ -57,13 +84,13 @@
71+
for (uint256 i; i < bundle.length; ++i) {
72+
address to = bundle[i].to;
73+
bytes32 callbackHash = bundle[i].callbackHash;
74+
- if (callbackHash == bytes32(0)) reenterHash = bytes32(0);
75+
- else reenterHash = keccak256(bytes.concat(bytes20(to), callbackHash));
76+
+ if (callbackHash == bytes32(0)) setReenterHash(bytes32(0));
77+
+ else setReenterHash(keccak256(bytes.concat(bytes20(to), callbackHash)));
78+
79+
(bool success, bytes memory returnData) = to.call{value: bundle[i].value}(bundle[i].data);
80+
if (!bundle[i].skipRevert && !success) UtilsLib.lowLevelRevert(returnData);
81+
82+
- require(reenterHash == bytes32(0), ErrorsLib.MissingExpectedReenter());
83+
+ require(reenterHash() == bytes32(0), ErrorsLib.MissingExpectedReenter());
84+
}
85+
}
86+
}

‎certora/confs/Bundler.conf

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
{
2+
"files": [
3+
"munged/Bundler.sol"
4+
],
5+
"solc": "solc-0.8.28",
6+
"verify": "Bundler:certora/specs/Bundler.spec",
7+
"rule_sanity": "basic",
8+
"server": "production",
9+
"msg": "Bundler V3",
10+
"loop_iter": "3",
11+
"optimistic_loop": true,
12+
"optimistic_hashing": true
13+
}

‎certora/specs/Bundler.spec

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
// SPDX-License-Identifier: GPL-2.0-or-later
2+
3+
using Bundler as Bundler;
4+
5+
methods {
6+
function initiator() external returns address envfree;
7+
function reenterHash() external returns bytes32 envfree;
8+
}
9+
10+
// True when `multicall` has been called.
11+
persistent ghost bool multicallCalled;
12+
13+
// True when `reenter` has been called.
14+
persistent ghost bool reenterCalled;
15+
16+
hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
17+
if (selector == sig:multicall(Bundler.Call[]).selector) {
18+
multicallCalled = true;
19+
} else if (selector == sig:reenter(Bundler.Call[]).selector) {
20+
reenterCalled = true;
21+
}
22+
}
23+
24+
// Check that reentering is possible only if `multicall` has been called.
25+
rule reenterAfterMulticall(method f, env e, calldataarg data) {
26+
27+
// Set up the initial state.
28+
require !multicallCalled;
29+
require !reenterCalled;
30+
// Safe require since it's transiently stored so it's nullified after a reentrant call.
31+
require reenterHash() == to_bytes32(0);
32+
33+
// Capture the first method call which is not performed with a CALL opcode.
34+
if (f.selector == sig:multicall(Bundler.Call[]).selector) {
35+
multicallCalled = true;
36+
} else if (f.selector == sig:reenter(Bundler.Call[]).selector) {
37+
reenterCalled = true;
38+
}
39+
40+
f@withrevert(e,data);
41+
42+
// Avoid failing vacuity checks, either the proposition is true or the execution reverts.
43+
assert !lastReverted => (reenterCalled => multicallCalled);
44+
}
45+
46+
// Check that non zero initiator will trigger a revert upon a multicall.
47+
rule nonZeroInitiatorRevertsMulticall(env e, Bundler.Call[] bundle) {
48+
address initiatorBefore = initiator();
49+
50+
multicall@withrevert(e, bundle);
51+
52+
assert initiatorBefore != 0 => lastReverted;
53+
}
54+
55+
// Check that a null reenterHash will trigger a revert upon reentering the bundler.
56+
rule zeroReenterHashRevertsReenter(env e, Bundler.Call[] bundle) {
57+
bytes32 reenterHashBefore = reenterHash();
58+
59+
reenter@withrevert(e, bundle);
60+
61+
assert reenterHashBefore == to_bytes32(0) => lastReverted;
62+
}

0 commit comments

Comments
 (0)