From 1c8df659b98177b737fd8af411b30bf24c1cbef1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ernesto=20Garc=C3=ADa?= Date: Tue, 14 Mar 2023 15:14:01 -0700 Subject: [PATCH 1/3] Clarify Governor Bravo compatibility scope (#4090) Co-authored-by: Francisco --- docs/modules/ROOT/pages/governance.adoc | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/modules/ROOT/pages/governance.adoc b/docs/modules/ROOT/pages/governance.adoc index cd7dd4e6f..c5bcf58cd 100644 --- a/docs/modules/ROOT/pages/governance.adoc +++ b/docs/modules/ROOT/pages/governance.adoc @@ -20,7 +20,9 @@ The ERC20 extension to keep track of votes and vote delegation is one such case. === Governor & GovernorCompatibilityBravo -An OpenZeppelin Governor contract is by default not interface-compatible with GovernorAlpha or Bravo, since some of the functions are different or missing, although it shares all of the same events. However, it’s possible to opt in to full compatibility by inheriting from the GovernorCompatibilityBravo module. The contract will be cheaper to deploy and use without this module. +An OpenZeppelin Governor contract is by default not interface-compatible with Compound's GovernorAlpha or Bravo. Even though events are fully compatible, proposal lifecycle functions (creation, execution, etc.) have different signatures that are meant to optimize storage use. Other functions from GovernorAlpha are Bravo are likewise not available. It’s possible to opt in to a higher level of compatibility by inheriting from the GovernorCompatibilityBravo module, which covers the proposal lifecycle functions such as `propose` and `execute`. + +Note that even with the use of this module, there will still be differences in the way that `proposalId`s are calculated. Governor uses the hash of the proposal parameters with the purpose of keeping its data off-chain by event indexing, while the original Bravo implementation uses sequential `proposalId`s. Due to this and other differences, several of the functions from GovernorBravo are not included in the compatibility module. === GovernorTimelockControl & GovernorTimelockCompound From 4f4b6ab40315e2fbfc06e65d78f06c5b26d4646c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ernesto=20Garc=C3=ADa?= Date: Wed, 15 Mar 2023 08:06:25 -0600 Subject: [PATCH 2/3] Update certora/README.md (#4114) Co-authored-by: Francisco --- certora/README.md | 82 +++++++++++++++++++++++++---------------------- 1 file changed, 43 insertions(+), 39 deletions(-) diff --git a/certora/README.md b/certora/README.md index 55f84d42f..cd85ba3d4 100644 --- a/certora/README.md +++ b/certora/README.md @@ -1,56 +1,60 @@ # Running the certora verification tool -These instructions detail the process for running CVT on the OpenZeppelin (Wizard/Governor) contracts. +These instructions detail the process for running Certora Verification Tool on OpenZeppelin Contracts. -Documentation for CVT and the specification language are available -[here](https://certora.atlassian.net/wiki/spaces/CPD/overview) +Documentation for CVT and the specification language are available [here](https://certora.atlassian.net/wiki/spaces/CPD/overview). + +## Prerequisites + +Follow the [Certora installation guide](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html) in order to get the Certora Prover Package and the `solc` executable folder in your path. + +> **Note** +> An API Key is required for local testing. Although the prover will run on a Github Actions' CI environment on selected Pull Requests. ## Running the verification -The scripts in the `certora/scripts` directory are used to submit verification -jobs to the Certora verification service. After the job is complete, the results will be available on -[the Certora portal](https://vaas-stg.certora.com/). +The Certora Verification Tool proves specs for contracts, which are defined by the `./specs.json` file along with their pre-configured options. -These scripts should be run from the root directory; for example by running +The verification script `./run.js` is used to submit verification jobs to the Certora Verification service. -``` -sh certora/scripts/verifyAll.sh +You can run it from the root of the repository with the following command: + +```bash +node certora/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...] ``` -The most important of these is `verifyAll.sh`, which checks -all of the harnessed contracts (`certora/harness/Wizard*.sol`) against all of -the specifications (`certora/spec/*.spec`). +Where: -The other scripts run a subset of the specifications or the contracts. You can -verify different contracts or specifications by changing the `--verify` option, -and you can run a single rule or method with the `--rule` or `--method` option. +- `CONTRACT_NAME` matches the `contract` key in the `./spec.json` file and may be empty. It will run all matching contracts if not provided. +- `SPEC_NAME` refers to a `spec` key from the `./specs.json` file. It will run every spec if not provided. +- `OPTIONS` extend the [Certora Prover CLI options](https://docs.certora.com/en/latest/docs/prover/cli/options.html#certora-prover-cli-options) and will respect the preconfigured options in the `specs.json` file. -For example, to verify the `WizardFirstPriority` contract against the -`GovernorCountingSimple` specification, you could change the `--verify` line of -the `WizardControlFirstPriortity.sh` script to: +> **Note** +> A single spec may be configured to run for multiple contracts, whereas a single contract may run multiple specs. -``` ---verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \ +Example usage: + +```bash +node certora/run.js AccessControl # Run the AccessControl spec against every contract implementing it ``` ## Adapting to changes in the contracts -Some of our rules require the code to be simplified in various ways. Our -primary tool for performing these simplifications is to run verification on a -contract that extends the original contracts and overrides some of the methods. -These "harness" contracts can be found in the `certora/harness` directory. - -This pattern does require some modifications to the original code: some methods -need to be made virtual or public, for example. These changes are handled by -applying a patch to the code before verification. - -When one of the `verify` scripts is executed, it first applies the patch file -`certora/applyHarness.patch` to the `contracts` directory, placing the output -in the `certora/munged` directory. We then verify the contracts in the -`certora/munged` directory. - -If the original contracts change, it is possible to create a conflict with the -patch. In this case, the verify scripts will report an error message and output -rejected changes in the `munged` directory. After merging the changes, run -`make record` in the `certora` directory; this will regenerate the patch file, -which can then be checked into git. +Some of our rules require the code to be simplified in various ways. Our primary tool for performing these simplifications is to run verification on a contract that extends the original contracts and overrides some of the methods. These "harness" contracts can be found in the `certora/harness` directory. + +This pattern does require some modifications to the original code: some methods need to be made virtual or public, for example. These changes are handled by applying a patch +to the code before verification by running: + +```bash +make -C certora apply +``` + +Before running the `certora/run.js` script, it's required to apply the corresponding patches to the `contracts` directory, placing the output in the `certora/patched` directory. Then, the contracts are verified by running the verification for the `certora/patched` directory. + +If the original contracts change, it is possible to create a conflict with the patch. In this case, the verify scripts will report an error message and output rejected changes in the `patched` directory. After merging the changes, run `make record` in the `certora` directory; this will regenerate the patch file, which can then be checked into git. + +For more information about the `make` scripts available, run: + +```bash +make -C certora help +``` From 1a60b061d5bb809c3d7e4ee915c77a00b1eca95d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ernesto=20Garc=C3=ADa?= Date: Thu, 16 Mar 2023 13:08:28 -0600 Subject: [PATCH 3/3] Add Pausable FV (#4117) Co-authored-by: Hadrien Croubois --- .gitignore | 1 + certora/harnesses/PausableHarness.sol | 19 ++++++ certora/specs.json | 5 ++ certora/specs/Pausable.spec | 96 +++++++++++++++++++++++++++ 4 files changed, 121 insertions(+) create mode 100644 certora/harnesses/PausableHarness.sol create mode 100644 certora/specs/Pausable.spec diff --git a/.gitignore b/.gitignore index 9350b262e..2aac74485 100644 --- a/.gitignore +++ b/.gitignore @@ -68,3 +68,4 @@ contracts-exposed .certora* .last_confs certora_* +.zip-output-url.txt diff --git a/certora/harnesses/PausableHarness.sol b/certora/harnesses/PausableHarness.sol new file mode 100644 index 000000000..37c5d591d --- /dev/null +++ b/certora/harnesses/PausableHarness.sol @@ -0,0 +1,19 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/security/Pausable.sol"; + +contract PausableHarness is Pausable { + function pause() external { + _pause(); + } + + function unpause() external { + _unpause(); + } + + function onlyWhenPaused() external whenPaused {} + + function onlyWhenNotPaused() external whenNotPaused {} +} diff --git a/certora/specs.json b/certora/specs.json index e76db3084..80fbf26af 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -1,4 +1,9 @@ [ + { + "spec": "Pausable", + "contract": "PausableHarness", + "files": ["certora/harnesses/PausableHarness.sol"] + }, { "spec": "AccessControl", "contract": "AccessControlHarness", diff --git a/certora/specs/Pausable.spec b/certora/specs/Pausable.spec new file mode 100644 index 000000000..e49293ffc --- /dev/null +++ b/certora/specs/Pausable.spec @@ -0,0 +1,96 @@ +import "helpers.spec" + +methods { + paused() returns (bool) envfree + pause() + unpause() + onlyWhenPaused() + onlyWhenNotPaused() +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: _pause pauses the contract │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule pause(env e) { + require nonpayable(e); + + bool pausedBefore = paused(); + + pause@withrevert(e); + bool success = !lastReverted; + + bool pausedAfter = paused(); + + // liveness + assert success <=> !pausedBefore, "works if and only if the contract was not paused before"; + + // effect + assert success => pausedAfter, "contract must be paused after a successful call"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: _unpause unpauses the contract │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule unpause(env e) { + require nonpayable(e); + + bool pausedBefore = paused(); + + unpause@withrevert(e); + bool success = !lastReverted; + + bool pausedAfter = paused(); + + // liveness + assert success <=> pausedBefore, "works if and only if the contract was paused before"; + + // effect + assert success => !pausedAfter, "contract must be unpaused after a successful call"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: whenPaused modifier can only be called if the contract is paused │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule whenPaused(env e) { + require nonpayable(e); + + onlyWhenPaused@withrevert(e); + assert !lastReverted <=> paused(), "works if and only if the contract is paused"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule whenNotPaused(env e) { + require nonpayable(e); + + onlyWhenNotPaused@withrevert(e); + assert !lastReverted <=> !paused(), "works if and only if the contract is not paused"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: only _pause and _unpause can change paused status │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noPauseChange(env e) { + method f; + calldataarg args; + + bool pausedBefore = paused(); + f(e, args); + bool pausedAfter = paused(); + + assert pausedBefore != pausedAfter => ( + (!pausedAfter && f.selector == unpause().selector) || + (pausedAfter && f.selector == pause().selector) + ), "contract's paused status can only be changed by _pause() or _unpause()"; +}