From 37725a0f2c4fdcaea229ff5aecddee7e6a96f515 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Wed, 24 Nov 2021 19:48:39 +0200 Subject: [PATCH] CleaningAndScriptForAllAndReadme --- certora/README.md | 49 +++++++++++++++++++ ...rdHarness1.sol => WizardFirstPriority.sol} | 2 +- ...norBasicHarness.sol => WizardFirstTry.sol} | 2 +- certora/scripts/AvengersAssemble.sh | 28 +++++++++++ ...zardHarness1.sh => WizardFirstPriority.sh} | 6 +-- .../{GovernorBasic.sh => WizardFirstTry.sh} | 4 +- certora/scripts/sanity.sh | 4 +- certora/specs/Privileged.spec | 31 ------------ 8 files changed, 86 insertions(+), 40 deletions(-) create mode 100644 certora/README.md rename certora/harnesses/{WizardHarness1.sol => WizardFirstPriority.sol} (96%) rename certora/harnesses/{GovernorBasicHarness.sol => WizardFirstTry.sol} (96%) create mode 100644 certora/scripts/AvengersAssemble.sh rename certora/scripts/{WizardHarness1.sh => WizardFirstPriority.sh} (53%) rename certora/scripts/{GovernorBasic.sh => WizardFirstTry.sh} (65%) delete mode 100644 certora/specs/Privileged.spec diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 000000000..b6cdc810e --- /dev/null +++ b/certora/README.md @@ -0,0 +1,49 @@ +# Running the certora verification tool + +These instructions detail the process for running CVT on the OpenZeppelin (Wizard/Governor) contracts. + +Documentation for CVT and the specification language are available +[here](https://certora.atlassian.net/wiki/spaces/CPD/overview) + +## Running the verification + +Due to current time and space limitations in the tool, many of the rules need to +be verified separately, so there are many steps required to reverify everything. + +The scripts in the `certora/scripts` directory are used to submit verification +jobs to the Certora verification service. These scripts should be run from the +root directory; for example by running + +``` +sh certora/scripts/WizardFirstPriority.sh +``` + +After the job is complete, the results will be available on +[the Certora portal](https://vaas-stg.certora.com/). + +The `AvengersAssemble` script runs all spec files agains all contracts in the `certora/harness` that start with `Wizard` meaning that a contract generated in [wizard](`certora/scripts`). If you want to verify new wizard's instance you also need to harness this contract. We don't recommend to do it because a list of harnesses may go beyond wizard's contract. The main goal of this script is to run all specs written by the team against all contracts properly harnessed. + +The `WizardFirstPriority` and `WizardFirstTry` scripts run one of the scripts for the corresponding contract. In order to run another spec you should change spec file name `` in the third line of a script: + +``` +--verify WizardFirstPriority:certora/specs/.spec \ + +for example: + +--verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \ +``` + + +MENTION TIMEOUTS ISSUES + + +## Adapting to changes + +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. diff --git a/certora/harnesses/WizardHarness1.sol b/certora/harnesses/WizardFirstPriority.sol similarity index 96% rename from certora/harnesses/WizardHarness1.sol rename to certora/harnesses/WizardFirstPriority.sol index 346e18360..d35cbb227 100644 --- a/certora/harnesses/WizardHarness1.sol +++ b/certora/harnesses/WizardFirstPriority.sol @@ -15,7 +15,7 @@ ERC20Votes TimelockCOntroller */ -contract WizardHarness1 is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl { +contract WizardFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl { constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction) Governor(name) GovernorVotes(_token) diff --git a/certora/harnesses/GovernorBasicHarness.sol b/certora/harnesses/WizardFirstTry.sol similarity index 96% rename from certora/harnesses/GovernorBasicHarness.sol rename to certora/harnesses/WizardFirstTry.sol index f63aaa161..f4d95c841 100644 --- a/certora/harnesses/GovernorBasicHarness.sol +++ b/certora/harnesses/WizardFirstTry.sol @@ -13,7 +13,7 @@ ERC20Votes TimelockCompound */ -contract GovernorBasicHarness is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound { +contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound { constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction) Governor(name) GovernorVotes(_token) diff --git a/certora/scripts/AvengersAssemble.sh b/certora/scripts/AvengersAssemble.sh new file mode 100644 index 000000000..1e59bde43 --- /dev/null +++ b/certora/scripts/AvengersAssemble.sh @@ -0,0 +1,28 @@ +for contract in certora/harnesses/Wizard*.sol; +do + for spec in certora/specs/*.spec; + do + contractFile=$(basename $contract) + specFile=$(basename $spec) + echo "Processing ${contractFile%.*} with $specFile" + if [ "${contractFile%.*}" = "WizardFirstPriority" ]; + then + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --link WizardFirstPriority:token=ERC20VotesHarness \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc8.2 \ + --staging shelly/forSasha \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --msg "checking $spec on ${contractFile%.*}" + else + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc8.2 \ + --staging shelly/forSasha \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --msg "checking $spec on ${contractFile%.*}" + fi + done +done diff --git a/certora/scripts/WizardHarness1.sh b/certora/scripts/WizardFirstPriority.sh similarity index 53% rename from certora/scripts/WizardHarness1.sh rename to certora/scripts/WizardFirstPriority.sh index 64fd52d33..980f617ea 100644 --- a/certora/scripts/WizardHarness1.sh +++ b/certora/scripts/WizardFirstPriority.sh @@ -1,6 +1,6 @@ -certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardHarness1.sol \ - --link WizardHarness1:token=ERC20VotesHarness \ - --verify WizardHarness1:certora/specs/GovernorCountingSimple.spec \ +certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstPriority.sol \ + --link WizardFirstPriority:token=ERC20VotesHarness \ + --verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \ --solc solc8.2 \ --staging shelly/forSasha \ --optimistic_loop \ diff --git a/certora/scripts/GovernorBasic.sh b/certora/scripts/WizardFirstTry.sh similarity index 65% rename from certora/scripts/GovernorBasic.sh rename to certora/scripts/WizardFirstTry.sh index 6f9c84059..8aa46e8cb 100644 --- a/certora/scripts/GovernorBasic.sh +++ b/certora/scripts/WizardFirstTry.sh @@ -1,5 +1,5 @@ -certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \ - --verify GovernorBasicHarness:certora/specs/GovernorBase.spec \ +certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \ + --verify WizardFirstTry:certora/specs/GovernorBase.spec \ --solc solc8.2 \ --staging shelly/forSasha \ --optimistic_loop \ diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh index 7ffaf52f7..58b27cc7d 100644 --- a/certora/scripts/sanity.sh +++ b/certora/scripts/sanity.sh @@ -1,11 +1,11 @@ -for f in certora/harnesses/*.sol +for f in certora/harnesses/Wizard*.sol do echo "Processing $f" file=$(basename $f) echo ${file%.*} certoraRun certora/harnesses/$file \ --verify ${file%.*}:certora/specs/sanity.spec "$@" \ - --solc solc8.0 --staging \ + --solc solc8.2 --staging shelly/forSasha \ --optimistic_loop \ --msg "checking sanity on ${file%.*}" --settings -copyLoopUnroll=4 diff --git a/certora/specs/Privileged.spec b/certora/specs/Privileged.spec deleted file mode 100644 index f9615a619..000000000 --- a/certora/specs/Privileged.spec +++ /dev/null @@ -1,31 +0,0 @@ -definition knownAsNonPrivileged(method f) returns bool = false -/* ( f.selector == isWhitelistedOtoken(address).selector || - f.selector == isWhitelistedProduct(address,address,address,bool).selector || - f.selector == owner().selector || - f.selector == isWhitelistedCallee(address).selector || - f.selector == whitelistOtoken(address).selector || - f.selector == addressBook().selector || - f.selector == isWhitelistedCollateral(address).selector )*/; - - - -rule privilegedOperation(method f, address privileged) -description "$f can be called by more than one user without reverting" -{ - env e1; - calldataarg arg; - require !knownAsNonPrivileged(f); - require e1.msg.sender == privileged; - - storage initialStorage = lastStorage; - invoke f(e1, arg); // privileged succeeds executing candidate privileged operation. - bool firstSucceeded = !lastReverted; - - env e2; - calldataarg arg2; - require e2.msg.sender != privileged; - invoke f(e2, arg2) at initialStorage; // unprivileged - bool secondSucceeded = !lastReverted; - - assert !(firstSucceeded && secondSucceeded), "${f.selector} can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged"; -}