diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index d4c5c3f..01f909f 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -17,6 +17,7 @@ jobs: matrix: conf: - Immutability + - Liveness - Reentrancy steps: diff --git a/certora/README.md b/certora/README.md index a5ca080..e3d3b47 100644 --- a/certora/README.md +++ b/certora/README.md @@ -1,34 +1,22 @@ # Pre-liquidation Contract Formal Verification -This folder contains the -[CVL](https://docs.certora.com/en/latest/docs/cvl/index.html) -specification and verification setup for the -[pre-liquidation](../src/PreLiquidation.sol) contract using the -[Certora Prover](https://www.certora.com/). +This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index.html) specification and verification setup for the [PreLiquidation](../src/PreLiquidation.sol) contract. ## Getting Started -This project depends on two different versions of -[Solidity](https://soliditylang.org/) which are required for running -the verification. The compiler binaries should be available under the -following path names: +This project depends on two different versions of [Solidity](https://soliditylang.org/) which are required for running the verification. +The compiler binaries should be available under the following path names: - - `solc-0.8.19` for the solidity compiler version `0.8.19`, which is - used for `Morpho`; - - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is - used for `PreLiquidation`. +- `solc-0.8.19` for the solidity compiler version `0.8.19`, which is used for `Morpho`; +- `solc-0.8.27` for the solidity compiler version `0.8.27`, which is used for `PreLiquidation`. -To verifying a specification, run the command `certoraRun Spec.conf` -where `Spec.conf` is the configuration file of the matching CVL -specification. Configuration files are available in -[`certora/conf`](./confs). Please ensure that `CERTORAKEY` is set up -in your environment. +To verify a specification, run the command `certoraRun Spec.conf`where `Spec.conf` is the configuration file of the matching CVL specification. +Configuration files are available in [`certora/confs`](confs). +Please ensure that `CERTORAKEY` is set up in your environment. ## Overview -The PreLiquidation contract enables Morpho Blue borrowers to set up a -safer liquidation plan on a given position, thus preventing undesired -liquidations. +The PreLiquidation contract enables Morpho borrowers to set up a safer liquidation plan on a given position, thus preventing undesired liquidations. ### Reentrancy @@ -38,28 +26,22 @@ This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec). This is checked in [`Immutability.spec`](specs/Immutability.spec). +### Liveness properties + +This is checked in [`Liveness.spec`](specs/Liveness.spec). + ## Verification architecture ### Folders and file structure The [`certora/specs`](specs) folder contains the following files: -- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that - PreLiquidation is reentrancy safe by checking that the storage is never - used. - -- [`Immutability.spec`](specs/Immutability.spec) checks that - PreLiquidation contract is immutable because it doesn't perform any - delegate call. - -The [`certora/confs`](confs) folder contains a configuration file for -each corresponding specification file. +- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that PreLiquidation is reentrancy safe by checking that the storage is never used; +- [`Immutability.spec`](specs/Immutability.spec) checks that PreLiquidation contract is immutable because it doesn't perform any delegate call; +- [`Liveness.spec`](specs/Liveness.spec) ensure that expected computations will always be performed. + For instance, pre-liquidations will always trigger a repay operation. -The [`certora/helpers`](helpers) folder contains helper contracts that -enable the verification of PreLiquidation. Notably, this allows -handling the fact that library functions should be called from a -contract to be verified independently, and it allows defining needed -getters. +The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file. ## TODO diff --git a/certora/confs/Immutability.conf b/certora/confs/Immutability.conf index 6fae19c..be04841 100644 --- a/certora/confs/Immutability.conf +++ b/certora/confs/Immutability.conf @@ -1,16 +1,16 @@ { - "files": [ - "src/PreLiquidation.sol", - ], - "solc": "solc-0.8.27", - "solc_via_ir" : true, - "verify": "PreLiquidation:certora/specs/Immutability.spec", - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 120", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "PreLiquidation Immutability", + "files": [ + "src/PreLiquidation.sol" + ], + "solc": "solc-0.8.27", + "solc_via_ir": true, + "verify": "PreLiquidation:certora/specs/Immutability.spec", + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 120" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "PreLiquidation Immutability" } diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf new file mode 100644 index 0000000..5485f14 --- /dev/null +++ b/certora/confs/Liveness.conf @@ -0,0 +1,31 @@ +{ + "files": [ + "src/PreLiquidation.sol", + "lib/morpho-blue/src/Morpho.sol" + ], + "link": [ + "PreLiquidation:MORPHO=Morpho" + ], + "parametric_contracts": [ + "PreLiquidation" + ], + "solc_via_ir": true, + "verify": "PreLiquidation:certora/specs/Liveness.spec", + "solc_optimize_map": { + "Morpho": "99999", + "PreLiquidation": "99999" + }, + "solc_map": { + "Morpho": "solc-0.8.19", + "PreLiquidation": "solc-0.8.27" + }, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 120", + "-smt_nonLinearArithmetic true" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "PreLiquidation Liveness" +} diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index f217f93..494929d 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -1,17 +1,17 @@ { - "files": [ - "src/PreLiquidation.sol", - ], - "solc": "solc-0.8.27", - "solc_via_ir" : true, - "verify": "PreLiquidation:certora/specs/Reentrancy.spec", - "prover_args": [ - "-enableStorageSplitting false", - "-depth 3", - "-mediumTimeout 20", - "-timeout 120", - ], - "rule_sanity": "basic", - "server": "production", - "msg": "PreLiquidation Reentrancy", + "files": [ + "src/PreLiquidation.sol" + ], + "solc": "solc-0.8.27", + "solc_via_ir": true, + "verify": "PreLiquidation:certora/specs/Reentrancy.spec", + "prover_args": [ + "-enableStorageSplitting false", + "-depth 3", + "-mediumTimeout 20", + "-timeout 120" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "PreLiquidation Reentrancy" } diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec new file mode 100644 index 0000000..28f686b --- /dev/null +++ b/certora/specs/Liveness.spec @@ -0,0 +1,44 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +using PreLiquidation as preLiq; + +methods { + function preLiq.MORPHO() external returns address envfree; +} + +// True when `preLiquidate` has been called. +persistent ghost bool preLiquidateCalled; + +// True when `onMorphoRepay` has been called. +persistent ghost bool onMorphoRepayCalled; + +hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + if (selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) { + preLiquidateCalled = true; + } else if (selector == sig:onMorphoRepay(uint256, bytes).selector) { + onMorphoRepayCalled = true; + } +} + +// Check that pre-liquidations happen if and only if `onMorphoRepay` is called. +rule preLiquidateRepays(method f, env e, calldataarg data) { + + // Set up the initial state. + require !preLiquidateCalled; + require !onMorphoRepayCalled; + + // Safe require because Morpho cannot send transactions. + require e.msg.sender != preLiq.MORPHO(); + + // Capture the first method call which is not performed with a CALL opcode. + if (f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) { + preLiquidateCalled = true; + } else if (f.selector == sig:onMorphoRepay(uint256, bytes).selector) { + onMorphoRepayCalled = true; + } + + f@withrevert(e,data); + + // Avoid failing vacuity checks, either the proposition is true or the execution reverts. + assert !lastReverted => (preLiquidateCalled <=> onMorphoRepayCalled); +} diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec index 12c808d..b6a7432 100644 --- a/certora/specs/Reentrancy.spec +++ b/certora/specs/Reentrancy.spec @@ -1,7 +1,5 @@ // SPDX-License-Identifier: GPL-2.0-or-later - - // True when storage has been accessed with either a SSTORE or a SLOAD. persistent ghost bool hasAccessedStorage;