diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index ee4b0f75..2218f4a4 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -27,6 +27,7 @@ jobs: - Reentrancy - Reverts - Roles + - Timelock - Tokens steps: @@ -46,13 +47,13 @@ jobs: run: | wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux chmod +x solc-static-linux - sudo mv solc-static-linux /usr/local/bin/solc8.19 + sudo mv solc-static-linux /usr/local/bin/solc-0.8.19 - name: Install solc (0.8.21) run: | wget https://github.com/ethereum/solidity/releases/download/v0.8.21/solc-static-linux chmod +x solc-static-linux - sudo mv solc-static-linux /usr/local/bin/solc + sudo mv solc-static-linux /usr/local/bin/solc-0.8.21 - name: Apply munging run: make -C certora munged diff --git a/certora/README.md b/certora/README.md index 2a735112..44ddb86a 100644 --- a/certora/README.md +++ b/certora/README.md @@ -63,6 +63,7 @@ rule revokePendingTimelockRevertCondition(env e) { ## Timelock MetaMorpho features a timelock mechanism that applies to every operation that could potentially increase risk for users. +There are computations that give a lower bound for the period during which we know the values are under timelock, and this is verified in [`Timelock.spec`](specs/Timelock.spec). The following function defined in [`PendingValues.spec`](specs/PendingValues.spec) is verified to always return `true`. ```solidity @@ -196,6 +197,7 @@ The [`certora/specs`](specs) folder contains the following files: - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that MetaMorpho is reentrancy safe by making sure that there are no untrusted external calls. - [`Reverts.spec`](specs/Reverts.spec) checks the revert conditions on entrypoints. - [`Roles.spec`](specs/Roles.spec) checks the access control and authorization granted by the respective MetaMorpho roles. In particular it checks the hierarchy of roles. +- [`Timelock.spec`](specs/Timelock.spec) gives computations (and verifies them) for periods during which we know the values are under timelock. - [`Tokens.spec`](specs/Tokens.spec) checks that tokens are not kept on the MetaMorpho contract. Any deposit ends up in Morpho Blue and any withdrawal is forwarded to the user. The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file. @@ -212,7 +214,8 @@ graph Tokens --> ConsistentState Liveness --> ConsistentState Reverts --> ConsistentState -ConsistentState --> LastUpdated +ConsistentState --> Timelock +Timelock --> LastUpdated LastUpdated --> Enabled Enabled --> DistinctIdentifiers DistinctIdentifiers --> PendingValues diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf index c56fb844..366d4e4c 100644 --- a/certora/confs/ConsistentState.conf +++ b/certora/confs/ConsistentState.conf @@ -3,13 +3,13 @@ "lib/morpho-blue/certora/harness/MorphoHarness.sol", "certora/helpers/MetaMorphoHarness.sol", ], + "solc_map": { + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", + }, "parametric_contracts": [ "MetaMorphoHarness", ], - "solc_map": { - "MorphoHarness": "solc8.19", - "MetaMorphoHarness": "solc", - }, "verify": "MetaMorphoHarness:certora/specs/ConsistentState.spec", "loop_iter": "2", "optimistic_loop": true, diff --git a/certora/confs/DistinctIdentifiers.conf b/certora/confs/DistinctIdentifiers.conf index d21c51be..a14ba101 100644 --- a/certora/confs/DistinctIdentifiers.conf +++ b/certora/confs/DistinctIdentifiers.conf @@ -2,6 +2,7 @@ "files": [ "certora/helpers/MetaMorphoHarness.sol", ], + "solc": "solc-0.8.21", "verify": "MetaMorphoHarness:certora/specs/DistinctIdentifiers.spec", "loop_iter": "2", "optimistic_loop": true, diff --git a/certora/confs/Enabled.conf b/certora/confs/Enabled.conf index 9d829ff3..650f7489 100644 --- a/certora/confs/Enabled.conf +++ b/certora/confs/Enabled.conf @@ -2,6 +2,7 @@ "files": [ "certora/helpers/MetaMorphoHarness.sol", ], + "solc": "solc-0.8.21", "verify": "MetaMorphoHarness:certora/specs/Enabled.spec", "loop_iter": "2", "optimistic_loop": true, diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf index fc89bd63..2e3802f7 100644 --- a/certora/confs/Immutability.conf +++ b/certora/confs/Immutability.conf @@ -2,6 +2,7 @@ "files": [ "certora/helpers/MetaMorphoHarness.sol", ], + "solc": "solc-0.8.21", "verify": "MetaMorphoHarness:certora/specs/Immutability.spec", "loop_iter": "2", "optimistic_loop": true, diff --git a/certora/confs/LastUpdated.conf b/certora/confs/LastUpdated.conf index c784b4a2..855c7359 100644 --- a/certora/confs/LastUpdated.conf +++ b/certora/confs/LastUpdated.conf @@ -3,12 +3,9 @@ "lib/morpho-blue/certora/harness/MorphoHarness.sol", "certora/helpers/MetaMorphoHarness.sol", ], - "parametric_contracts": [ - "MetaMorphoHarness", - ], "solc_map": { - "MorphoHarness": "solc8.19", - "MetaMorphoHarness": "solc", + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", }, "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec", "loop_iter": "2", diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index 1ba98147..ed583baf 100644 --- a/certora/confs/Liveness.conf +++ b/certora/confs/Liveness.conf @@ -8,9 +8,9 @@ "MetaMorphoHarness:MORPHO=MorphoHarness", ], "solc_map": { - "MorphoHarness": "solc8.19", - "MetaMorphoHarness": "solc", - "Util": "solc", + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", + "Util": "solc-0.8.21", }, "verify": "MetaMorphoHarness:certora/specs/Liveness.spec", "loop_iter": "2", diff --git a/certora/confs/PendingValues.conf b/certora/confs/PendingValues.conf index bdfd5036..c2e22bc5 100644 --- a/certora/confs/PendingValues.conf +++ b/certora/confs/PendingValues.conf @@ -2,6 +2,7 @@ "files": [ "certora/helpers/MetaMorphoHarness.sol", ], + "solc": "solc-0.8.21", "verify": "MetaMorphoHarness:certora/specs/PendingValues.spec", "loop_iter": "2", "optimistic_loop": true, diff --git a/certora/confs/Range.conf b/certora/confs/Range.conf index 062e2b57..383bcc8d 100644 --- a/certora/confs/Range.conf +++ b/certora/confs/Range.conf @@ -2,6 +2,7 @@ "files": [ "certora/helpers/MetaMorphoHarness.sol", ], + "solc": "solc-0.8.21", "verify": "MetaMorphoHarness:certora/specs/Range.spec", "loop_iter": "2", "optimistic_loop": true, diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index 5e6e3616..2c078aef 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -2,6 +2,7 @@ "files": [ "certora/helpers/MetaMorphoHarness.sol", ], + "solc": "solc-0.8.21", "verify": "MetaMorphoHarness:certora/specs/Reentrancy.spec", "loop_iter": "2", "optimistic_loop": true, diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index c371399e..a3407b2b 100644 --- a/certora/confs/Reverts.conf +++ b/certora/confs/Reverts.conf @@ -9,10 +9,10 @@ "MetaMorphoHarness:MORPHO=MorphoHarness", ], "solc_map": { - "MorphoHarness": "solc8.19", - "MetaMorphoHarness": "solc", - "Util": "solc", - "ERC20Standard": "solc", + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", + "Util": "solc-0.8.21", + "ERC20Standard": "solc-0.8.21", }, "verify": "MetaMorphoHarness:certora/specs/Reverts.spec", "loop_iter": "2", diff --git a/certora/confs/Roles.conf b/certora/confs/Roles.conf index 72cd8283..0db5cb2d 100644 --- a/certora/confs/Roles.conf +++ b/certora/confs/Roles.conf @@ -2,6 +2,7 @@ "files": [ "certora/helpers/MetaMorphoHarness.sol", ], + "solc": "solc-0.8.21", "verify": "MetaMorphoHarness:certora/specs/Roles.spec", "loop_iter": "2", "optimistic_loop": true, diff --git a/certora/confs/Timelock.conf b/certora/confs/Timelock.conf new file mode 100644 index 00000000..c98a9ae8 --- /dev/null +++ b/certora/confs/Timelock.conf @@ -0,0 +1,24 @@ +{ + "files": [ + "lib/morpho-blue/certora/harness/MorphoHarness.sol", + "certora/helpers/MetaMorphoHarness.sol", + ], + "parametric_contracts": [ + "MetaMorphoHarness", + ], + "solc_map": { + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", + }, + "verify": "MetaMorphoHarness:certora/specs/Timelock.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 300", + ], + "rule_sanity": "basic", + "server": "production", + "msg": "MetaMorpho Timelock" +} diff --git a/certora/confs/Tokens.conf b/certora/confs/Tokens.conf index 1203da4d..e533c66b 100644 --- a/certora/confs/Tokens.conf +++ b/certora/confs/Tokens.conf @@ -11,12 +11,12 @@ "MetaMorphoHarness:MORPHO=MorphoHarness", ], "solc_map": { - "MorphoHarness": "solc8.19", - "MetaMorphoHarness": "solc", - "Util": "solc", - "ERC20NoRevert": "solc", - "ERC20Standard": "solc", - "ERC20USDT": "solc", + "MorphoHarness": "solc-0.8.19", + "MetaMorphoHarness": "solc-0.8.21", + "Util": "solc-0.8.21", + "ERC20NoRevert": "solc-0.8.21", + "ERC20Standard": "solc-0.8.21", + "ERC20USDT": "solc-0.8.21", }, "verify": "MetaMorphoHarness:certora/specs/Tokens.spec", "loop_iter": "2", diff --git a/certora/helpers/MetaMorphoHarness.sol b/certora/helpers/MetaMorphoHarness.sol index f8c90f45..d2bbcaf1 100644 --- a/certora/helpers/MetaMorphoHarness.sol +++ b/certora/helpers/MetaMorphoHarness.sol @@ -1,7 +1,9 @@ // SPDX-License-Identifier: GPL-2.0-or-later pragma solidity 0.8.21; -import {MetaMorpho, Id, ConstantsLib, PendingUint192, PendingAddress, MarketConfig} from "../munged/MetaMorpho.sol"; +import { + Math, MetaMorpho, Id, ConstantsLib, PendingUint192, PendingAddress, MarketConfig +} from "../munged/MetaMorpho.sol"; contract MetaMorphoHarness is MetaMorpho { constructor( @@ -44,4 +46,43 @@ contract MetaMorphoHarness is MetaMorpho { function maxFee() external pure returns (uint256) { return ConstantsLib.MAX_FEE; } + + function nextGuardianUpdateTime() external view returns (uint256 nextTime) { + nextTime = block.timestamp + timelock; + + if (pendingTimelock.validAt != 0) { + nextTime = Math.min(nextTime, pendingTimelock.validAt + pendingTimelock.value); + } + + uint256 validAt = pendingGuardian.validAt; + if (validAt != 0) nextTime = Math.min(nextTime, validAt); + } + + function nextCapIncreaseTime(Id id) external view returns (uint256 nextTime) { + nextTime = block.timestamp + timelock; + + if (pendingTimelock.validAt != 0) { + nextTime = Math.min(nextTime, pendingTimelock.validAt + pendingTimelock.value); + } + + uint256 validAt = pendingCap[id].validAt; + if (validAt != 0) nextTime = Math.min(nextTime, validAt); + } + + function nextTimelockDecreaseTime() external view returns (uint256 nextTime) { + nextTime = block.timestamp + timelock; + + if (pendingTimelock.validAt != 0) nextTime = Math.min(nextTime, pendingTimelock.validAt); + } + + function nextRemovableTime(Id id) external view returns (uint256 nextTime) { + nextTime = block.timestamp + timelock; + + if (pendingTimelock.validAt != 0) { + nextTime = Math.min(nextTime, pendingTimelock.validAt + pendingTimelock.value); + } + + uint256 removableAt = config[id].removableAt; + if (removableAt != 0) nextTime = Math.min(nextTime, removableAt); + } } diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 9423b20e..8185f85b 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -1,5 +1,5 @@ // SPDX-License-Identifier: GPL-2.0-or-later -import "LastUpdated.spec"; +import "Timelock.spec"; function hasCuratorRole(address user) returns bool { return user == owner() || user == curator(); diff --git a/certora/specs/Timelock.spec b/certora/specs/Timelock.spec new file mode 100644 index 00000000..51c2acb1 --- /dev/null +++ b/certora/specs/Timelock.spec @@ -0,0 +1,213 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +import "LastUpdated.spec"; + +methods { + function _.supplyShares(MetaMorphoHarness.Id id, address user) external => summarySupplyshares(id, user) expect uint256; +} + +ghost lastSupplyShares(MetaMorphoHarness.Id, address) returns uint256; + +function summarySupplyshares(MetaMorphoHarness.Id id, address user) returns uint256 { + uint256 res; + require lastSupplyShares(id, user) == res; + return res; +} + +// Show that nextGuardianUpdateTime does not revert. +rule nextGuardianUpdateTimeDoesNotRevert() { + // The environment e yields the current time. + env e; + require e.msg.value == 0; + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + // Safe require because it is a verified invariant. + require isTimelockInRange(); + // Safe require because it is a verified invariant. + require isPendingTimelockInRange(); + + nextGuardianUpdateTime@withrevert(e); + + assert !lastReverted; +} + +// Show that nextGuardianUpdateTime is increasing with time and that no change of guardian can happen before it. +rule guardianUpdateTime(env e_next, method f, calldataarg args) { + // The environment e yields the current time. + env e; + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + // Safe require because it is a verified invariant. + require isTimelockInRange(); + + uint256 nextTime = nextGuardianUpdateTime(e); + address prevGuardian = guardian(); + + // Assume that the guardian is already set. + require prevGuardian != 0; + // Sane assumption on the current time, as any following transaction should happen after it. + require e_next.block.timestamp >= e.block.timestamp; + uint256 nextGuardianUpdateTimeBeforeInteraction = nextGuardianUpdateTime(e); + // Increasing nextGuardianUpdateTime with no interaction; + assert nextGuardianUpdateTimeBeforeInteraction >= nextTime; + + f(e_next, args); + + if (e_next.block.timestamp < nextTime) { + // Check that guardian cannot change. + assert guardian() == prevGuardian; + // Increasing nextGuardianUpdateTime with an interaction; + assert nextGuardianUpdateTime(e_next) >= nextGuardianUpdateTimeBeforeInteraction; + } + assert true; +} + +// Show that nextCapIncreaseTime does not revert. +rule nextCapIncreaseTimeDoesNotRevert(MetaMorphoHarness.Id id) { + // The environment e yields the current time. + env e; + require e.msg.value == 0; + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + // Safe require because it is a verified invariant. + require isTimelockInRange(); + // Safe require because it is a verified invariant. + require isPendingTimelockInRange(); + + nextCapIncreaseTime@withrevert(e, id); + + assert !lastReverted; +} + +// Show that nextCapIncreaseTime is increasing with time and that no increase of cap can happen before it. +rule capIncreaseTime(env e_next, method f, calldataarg args) { + // The environment e yields the current time. + env e; + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + MetaMorphoHarness.Id id; + + // Safe require because it is a verified invariant. + require isTimelockInRange(); + + uint256 nextTime = nextCapIncreaseTime(e, id); + uint184 prevCap = config_(id).cap; + + // Sane assumption on the current time, as any following transaction should happen after it. + require e_next.block.timestamp >= e.block.timestamp; + uint256 nextCapIncreaseTimeBeforeInteraction = nextCapIncreaseTime(e_next, id); + // Increasing nextCapIncreaseTime with no interaction; + assert nextCapIncreaseTimeBeforeInteraction >= nextTime; + + f(e_next, args); + + if (e_next.block.timestamp < nextTime) { + // Check that cap cannot increase. + assert config_(id).cap <= prevCap; + // Increasing nextCapIncreaseTime with an interaction; + assert nextCapIncreaseTime(e_next, id) >= nextCapIncreaseTimeBeforeInteraction; + } + assert true; +} + +// Show that nextTimelockDecreaseTime does not revert. +rule nextTimelockDecreaseTimeDoesNotRevert() { + // The environment e yields the current time. + env e; + require e.msg.value == 0; + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + // Safe require because it is a verified invariant. + require isTimelockInRange(); + // Safe require because it is a verified invariant. + require isPendingTimelockInRange(); + + nextTimelockDecreaseTime@withrevert(e); + + assert !lastReverted; +} + +// Show that nextTimelockDecreaseTime is increasing with time and that no decrease of timelock can happen before it. +rule timelockDecreaseTime(env e_next, method f, calldataarg args) { + // The environment e yields the current time. + env e; + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + // Safe require because it is a verified invariant. + require isTimelockInRange(); + + uint256 nextTime = nextTimelockDecreaseTime(e); + uint256 prevTimelock = timelock(); + + // Sane assumption on the current time, as any following transaction should happen after it. + require e_next.block.timestamp >= e.block.timestamp; + uint256 nextTimelockDecreaseTimeBeforeInteraction = nextTimelockDecreaseTime(e_next); + // Increasing nextTimelockDecreaseTime with no interaction; + assert nextTimelockDecreaseTimeBeforeInteraction >= nextTime; + + f(e_next, args); + + if (e_next.block.timestamp < nextTime) { + // Check that timelock cannot decrease. + assert timelock() >= prevTimelock; + // Increasing nextTimelockDecreaseTime with an interaction; + assert nextTimelockDecreaseTime(e_next) >= nextTimelockDecreaseTimeBeforeInteraction; + } + assert true; +} + +// Show that nextRemovableTime does not revert. +rule nextRemovableTimeDoesNotRevert(MetaMorphoHarness.Id id) { + // The environment e yields the current time. + env e; + require e.msg.value == 0; + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + // Safe require because it is a verified invariant. + require isTimelockInRange(); + // Safe require because it is a verified invariant. + require isPendingTimelockInRange(); + + nextRemovableTime@withrevert(e, id); + + assert !lastReverted; +} + +// Show that nextRemovableTime is increasing with time and that no removal can happen before it. +rule removableTime(env e_next, method f, calldataarg args) { + // The environment e yields the current time. + env e; + // Safe require as it corresponds to some time very far into the future. + require e.block.timestamp < 2^63; + + MetaMorphoHarness.Id id; + + // Safe require because it is a verified invariant. + require isTimelockInRange(); + + uint256 nextTime = nextRemovableTime(e, id); + + // Assume that the market is enabled. + require config_(id).enabled; + // Sane assumption on the current time, as any following transaction should happen after it. + require e_next.block.timestamp >= e.block.timestamp; + uint256 nextRemovableTimeBeforeInteraction = nextRemovableTime(e_next, id); + // Increasing nextRemovableTime with no interaction; + assert nextRemovableTimeBeforeInteraction >= nextTime; + + f(e_next, args); + + if (e_next.block.timestamp < nextTime) { + // Check that no forced removal happened. + assert lastSupplyShares(id, currentContract) > 0 => config_(id).enabled; + // Increasing nextRemovableTime with an interaction; + assert nextRemovableTime(e_next, id) >= nextRemovableTimeBeforeInteraction; + } + assert true; +}