Skip to content

Commit 915ca18

Browse files
mdgeorge4153shellygrRedLikeRosesssMichaelMorami
authored
Add Certora's Governance verification rules (OpenZeppelin#2997)
Co-authored-by: Shelly Grossman <[email protected]> Co-authored-by: Aleksander Kryukov <[email protected]> Co-authored-by: Michael M <[email protected]> Co-authored-by: Aleksander Kryukov <[email protected]>
1 parent a0a8bbb commit 915ca18

18 files changed

+1310
-0
lines changed

.gitignore

+5
Original file line numberDiff line numberDiff line change
@@ -57,3 +57,8 @@ allFiredEvents
5757
# hardhat
5858
cache
5959
artifacts
60+
61+
# Certora
62+
.certora*
63+
.last_confs
64+
certora_*

certora/Makefile

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
default: help
2+
3+
PATCH = applyHarness.patch
4+
CONTRACTS_DIR = ../contracts
5+
MUNGED_DIR = munged
6+
7+
help:
8+
@echo "usage:"
9+
@echo " make clean: remove all generated files (those ignored by git)"
10+
@echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
11+
@echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
12+
13+
munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
14+
rm -rf $@
15+
cp -r $(CONTRACTS_DIR) $@
16+
patch -p0 -d $@ < $(PATCH)
17+
18+
record:
19+
diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
20+
21+
clean:
22+
git clean -fdX
23+
touch $(PATCH)
24+

certora/README.md

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
# Running the certora verification tool
2+
3+
These instructions detail the process for running CVT on the OpenZeppelin (Wizard/Governor) contracts.
4+
5+
Documentation for CVT and the specification language are available
6+
[here](https://certora.atlassian.net/wiki/spaces/CPD/overview)
7+
8+
## Running the verification
9+
10+
The scripts in the `certora/scripts` directory are used to submit verification
11+
jobs to the Certora verification service. After the job is complete, the results will be available on
12+
[the Certora portal](https://vaas-stg.certora.com/).
13+
14+
These scripts should be run from the root directory; for example by running
15+
16+
```
17+
sh certora/scripts/verifyAll.sh <meaningful comment>
18+
```
19+
20+
The most important of these is `verifyAll.sh`, which checks
21+
all of the harnessed contracts (`certora/harness/Wizard*.sol`) against all of
22+
the specifications (`certora/spec/*.spec`).
23+
24+
The other scripts run a subset of the specifications or the contracts. You can
25+
verify different contracts or specifications by changing the `--verify` option,
26+
and you can run a single rule or method with the `--rule` or `--method` option.
27+
28+
For example, to verify the `WizardFirstPriority` contract against the
29+
`GovernorCountingSimple` specification, you could change the `--verify` line of
30+
the `WizardControlFirstPriortity.sh` script to:
31+
32+
```
33+
--verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \
34+
```
35+
36+
## Adapting to changes in the contracts
37+
38+
Some of our rules require the code to be simplified in various ways. Our
39+
primary tool for performing these simplifications is to run verification on a
40+
contract that extends the original contracts and overrides some of the methods.
41+
These "harness" contracts can be found in the `certora/harness` directory.
42+
43+
This pattern does require some modifications to the original code: some methods
44+
need to be made virtual or public, for example. These changes are handled by
45+
applying a patch to the code before verification.
46+
47+
When one of the `verify` scripts is executed, it first applies the patch file
48+
`certora/applyHarness.patch` to the `contracts` directory, placing the output
49+
in the `certora/munged` directory. We then verify the contracts in the
50+
`certora/munged` directory.
51+
52+
If the original contracts change, it is possible to create a conflict with the
53+
patch. In this case, the verify scripts will report an error message and output
54+
rejected changes in the `munged` directory. After merging the changes, run
55+
`make record` in the `certora` directory; this will regenerate the patch file,
56+
which can then be checked into git.

certora/applyHarness.patch

+101
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
diff -ruN .gitignore .gitignore
2+
--- .gitignore 1969-12-31 19:00:00.000000000 -0500
3+
+++ .gitignore 2021-12-09 14:46:33.923637220 -0500
4+
@@ -0,0 +1,2 @@
5+
+*
6+
+!.gitignore
7+
diff -ruN governance/compatibility/GovernorCompatibilityBravo.sol governance/compatibility/GovernorCompatibilityBravo.sol
8+
--- governance/compatibility/GovernorCompatibilityBravo.sol 2021-12-03 15:24:56.523654357 -0500
9+
+++ governance/compatibility/GovernorCompatibilityBravo.sol 2021-12-09 14:46:33.923637220 -0500
10+
@@ -245,7 +245,7 @@
11+
/**
12+
* @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum.
13+
*/
14+
- function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
15+
+ function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
16+
ProposalDetails storage details = _proposalDetails[proposalId];
17+
return quorum(proposalSnapshot(proposalId)) <= details.forVotes;
18+
}
19+
@@ -253,7 +253,7 @@
20+
/**
21+
* @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes.
22+
*/
23+
- function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
24+
+ function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal
25+
ProposalDetails storage details = _proposalDetails[proposalId];
26+
return details.forVotes > details.againstVotes;
27+
}
28+
diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
29+
--- governance/extensions/GovernorCountingSimple.sol 2021-12-03 15:24:56.523654357 -0500
30+
+++ governance/extensions/GovernorCountingSimple.sol 2021-12-09 14:46:33.923637220 -0500
31+
@@ -64,7 +64,7 @@
32+
/**
33+
* @dev See {Governor-_quorumReached}.
34+
*/
35+
- function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) {
36+
+ function _quorumReached(uint256 proposalId) public view virtual override returns (bool) {
37+
ProposalVote storage proposalvote = _proposalVotes[proposalId];
38+
39+
return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes;
40+
@@ -73,7 +73,7 @@
41+
/**
42+
* @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes.
43+
*/
44+
- function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) {
45+
+ function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) {
46+
ProposalVote storage proposalvote = _proposalVotes[proposalId];
47+
48+
return proposalvote.forVotes > proposalvote.againstVotes;
49+
diff -ruN governance/extensions/GovernorTimelockControl.sol governance/extensions/GovernorTimelockControl.sol
50+
--- governance/extensions/GovernorTimelockControl.sol 2021-12-03 15:24:56.523654357 -0500
51+
+++ governance/extensions/GovernorTimelockControl.sol 2021-12-09 14:46:33.923637220 -0500
52+
@@ -111,7 +111,7 @@
53+
bytes[] memory calldatas,
54+
bytes32 descriptionHash
55+
) internal virtual override {
56+
- _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
57+
+ _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash);
58+
}
59+
60+
/**
61+
diff -ruN governance/Governor.sol governance/Governor.sol
62+
--- governance/Governor.sol 2021-12-03 15:24:56.523654357 -0500
63+
+++ governance/Governor.sol 2021-12-09 14:46:56.411503587 -0500
64+
@@ -38,8 +38,8 @@
65+
66+
string private _name;
67+
68+
- mapping(uint256 => ProposalCore) private _proposals;
69+
-
70+
+ mapping(uint256 => ProposalCore) public _proposals;
71+
+
72+
/**
73+
* @dev Restrict access to governor executing address. Some module might override the _executor function to make
74+
* sure this modifier is consistant with the execution model.
75+
@@ -167,12 +167,12 @@
76+
/**
77+
* @dev Amount of votes already cast passes the threshold limit.
78+
*/
79+
- function _quorumReached(uint256 proposalId) internal view virtual returns (bool);
80+
+ function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
81+
82+
/**
83+
* @dev Is the proposal successful or not.
84+
*/
85+
- function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool);
86+
+ function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal
87+
88+
/**
89+
* @dev Register a vote with a given support and voting weight.
90+
diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
91+
--- token/ERC20/extensions/ERC20Votes.sol 2021-12-03 15:24:56.527654330 -0500
92+
+++ token/ERC20/extensions/ERC20Votes.sol 2021-12-09 14:46:33.927637196 -0500
93+
@@ -84,7 +84,7 @@
94+
*
95+
* - `blockNumber` must have been already mined
96+
*/
97+
- function getPastVotes(address account, uint256 blockNumber) public view returns (uint256) {
98+
+ function getPastVotes(address account, uint256 blockNumber) public view virtual returns (uint256) {
99+
require(blockNumber < block.number, "ERC20Votes: block not yet mined");
100+
return _checkpointsLookup(_checkpoints[account], blockNumber);
101+
}
+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
import "../munged/token/ERC20/extensions/ERC20Votes.sol";
2+
3+
contract ERC20VotesHarness is ERC20Votes {
4+
constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {}
5+
6+
mapping(address => mapping(uint256 => uint256)) public _getPastVotes;
7+
8+
function _afterTokenTransfer(
9+
address from,
10+
address to,
11+
uint256 amount
12+
) internal virtual override {
13+
super._afterTokenTransfer(from, to, amount);
14+
_getPastVotes[from][block.number] -= amount;
15+
_getPastVotes[to][block.number] += amount;
16+
}
17+
18+
/**
19+
* @dev Change delegation for `delegator` to `delegatee`.
20+
*
21+
* Emits events {DelegateChanged} and {DelegateVotesChanged}.
22+
*/
23+
function _delegate(address delegator, address delegatee) internal virtual override{
24+
super._delegate(delegator, delegatee);
25+
_getPastVotes[delegator][block.number] -= balanceOf(delegator);
26+
_getPastVotes[delegatee][block.number] += balanceOf(delegator);
27+
}
28+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,150 @@
1+
// SPDX-License-Identifier: MIT
2+
pragma solidity ^0.8.2;
3+
4+
import "../munged/governance/Governor.sol";
5+
import "../munged/governance/extensions/GovernorCountingSimple.sol";
6+
import "../munged/governance/extensions/GovernorVotes.sol";
7+
import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol";
8+
import "../munged/governance/extensions/GovernorTimelockControl.sol";
9+
import "../munged/governance/extensions/GovernorProposalThreshold.sol";
10+
11+
/*
12+
Wizard options:
13+
ProposalThreshhold = 10
14+
ERC20Votes
15+
TimelockController
16+
*/
17+
18+
contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl {
19+
constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction)
20+
Governor(name)
21+
GovernorVotes(_token)
22+
GovernorVotesQuorumFraction(quorumFraction)
23+
GovernorTimelockControl(_timelock)
24+
{}
25+
26+
//HARNESS
27+
28+
function isExecuted(uint256 proposalId) public view returns (bool) {
29+
return _proposals[proposalId].executed;
30+
}
31+
32+
function isCanceled(uint256 proposalId) public view returns (bool) {
33+
return _proposals[proposalId].canceled;
34+
}
35+
36+
uint256 _votingDelay;
37+
38+
uint256 _votingPeriod;
39+
40+
uint256 _proposalThreshold;
41+
42+
mapping(uint256 => uint256) public ghost_sum_vote_power_by_id;
43+
44+
function _castVote(
45+
uint256 proposalId,
46+
address account,
47+
uint8 support,
48+
string memory reason
49+
) internal override virtual returns (uint256) {
50+
51+
uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS
52+
ghost_sum_vote_power_by_id[proposalId] += deltaWeight;
53+
54+
return deltaWeight;
55+
}
56+
57+
function snapshot(uint256 proposalId) public view returns (uint64) {
58+
return _proposals[proposalId].voteStart._deadline;
59+
}
60+
61+
62+
function getExecutor() public view returns (address){
63+
return _executor();
64+
}
65+
66+
// original code, harnessed
67+
68+
function votingDelay() public view override returns (uint256) { // HARNESS: pure -> view
69+
return _votingDelay; // HARNESS: parametric
70+
}
71+
72+
function votingPeriod() public view override returns (uint256) { // HARNESS: pure -> view
73+
return _votingPeriod; // HARNESS: parametric
74+
}
75+
76+
function proposalThreshold() public view override returns (uint256) { // HARNESS: pure -> view
77+
return _proposalThreshold; // HARNESS: parametric
78+
}
79+
80+
// original code, not harnessed
81+
// The following functions are overrides required by Solidity.
82+
83+
function quorum(uint256 blockNumber)
84+
public
85+
view
86+
override(IGovernor, GovernorVotesQuorumFraction)
87+
returns (uint256)
88+
{
89+
return super.quorum(blockNumber);
90+
}
91+
92+
function getVotes(address account, uint256 blockNumber)
93+
public
94+
view
95+
override(IGovernor, GovernorVotes)
96+
returns (uint256)
97+
{
98+
return super.getVotes(account, blockNumber);
99+
}
100+
101+
function state(uint256 proposalId)
102+
public
103+
view
104+
override(Governor, GovernorTimelockControl)
105+
returns (ProposalState)
106+
{
107+
return super.state(proposalId);
108+
}
109+
110+
function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description)
111+
public
112+
override(Governor, GovernorProposalThreshold, IGovernor)
113+
returns (uint256)
114+
{
115+
return super.propose(targets, values, calldatas, description);
116+
}
117+
118+
function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
119+
internal
120+
override(Governor, GovernorTimelockControl)
121+
{
122+
super._execute(proposalId, targets, values, calldatas, descriptionHash);
123+
}
124+
125+
function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash)
126+
internal
127+
override(Governor, GovernorTimelockControl)
128+
returns (uint256)
129+
{
130+
return super._cancel(targets, values, calldatas, descriptionHash);
131+
}
132+
133+
function _executor()
134+
internal
135+
view
136+
override(Governor, GovernorTimelockControl)
137+
returns (address)
138+
{
139+
return super._executor();
140+
}
141+
142+
function supportsInterface(bytes4 interfaceId)
143+
public
144+
view
145+
override(Governor, GovernorTimelockControl)
146+
returns (bool)
147+
{
148+
return super.supportsInterface(interfaceId);
149+
}
150+
}

0 commit comments

Comments
 (0)