Image Not Showing Possible Reasons

The image was uploaded to a note which you don't have access to
The note which the image was originally uploaded to has been deleted

Formal Verification Report for OpenZeppelin Governance Contracts

Summary

This document describes the specification and verification of OpenZeppelin's Governor module using the Certora Prover. The work was undertaken from October 31 to November 23, 2021. The latest commit that was reviewed and ran through the Certora Prover was 4088540a.

The scope of this verification is OpenZeppelin's governance system, particularly the following contracts:

Governor.sol
extensions/GovernorCountingSimple.sol
extensions/GovernorProposalThreshold.sol
extensions/GovernorTimelockControl.sol
extensions/GovernorVotes.sol
extensions/GovernorVotesQuorumFraction.sol

The Certora Prover proved the implementation of the Governance system is correct with respect to formal specifications written by the the Certora team. The team also performed a manual audit of these contracts.

The formal specifications are focused on validating the integrity of the governance system –- valid states of proposals, correct transitions between proposal states, invocation privileges and integrity of vote casting and counting. The formal specifications have been submitted as a pull request against OpenZeppelin's public git repository.

Main Issues Discovered

Severity: High

Issue: Setting the proposalThreshold too high breaks the proposing system

Description: In any case where the proposalThreshold becomes too high for any user to propose, it will be impossible to set a new, more reasonable threshold to the system. That is since the setter setProposalThreshold is guarded by the modifier onlyGovernance, which must be executed via a proposal. This situation may occur by either accidentally setting the threshold too high, or by changes in ERC20Votes token's market value which will price users out of the ability to raise proposals.

Response: The obvious solution is to set a reasonable maximum to proposalThreshold, however we can't hardcode an opinionated maximum as it is highly dependent on the specifics of the governance system, e.g. different protocols may use different numbers of decimals and in this case a maximum threshold can be orders of magnitude off. An alternative is to provide the maximum as a configurable parameter, but this increases the complexity of setting up governance parameters in a way that could be counterproductive. The assumption is that a critical operation like changing the proposal threshold would be properly tested. Changes in the market value of the voting token are seen as a possibility that needs to be dealt with as part of the governance protocol.

Issue:	Setting the `proposalThreshold` too high breaks the proposing system
Description:	In any case where the `proposalThreshold` becomes too high for any user to propose, it will be impossible to set a new, more reasonable threshold to the system. That is since the setter `setProposalThreshold` is guarded by the modifier `onlyGovernance`, which must be executed via a proposal. This situation may occur by either accidentally setting the threshold too high, or by changes in `ERC20Votes` token's market value which will price users out of the ability to raise proposals.
Response:	The obvious solution is to set a reasonable maximum to proposalThreshold, however we can't hardcode an opinionated maximum as it is highly dependent on the specifics of the governance system, e.g. different protocols may use different numbers of decimals and in this case a maximum threshold can be orders of magnitude off. An alternative is to provide the maximum as a configurable parameter, but this increases the complexity of setting up governance parameters in a way that could be counterproductive. The assumption is that a critical operation like changing the proposal threshold would be properly tested. Changes in the market value of the voting token are seen as a possibility that needs to be dealt with as part of the governance protocol.

Severity: High

Issue: Two systems that use the same timelock can attack each other

Description: In case that two rival systems use the same timelock in GovernorTimelockControl, each one of them can propse to invoke onlyGovenrnace functions on behalf the other system. Since the timelock is the executor of both those systems, the function will be invoked successfuly. This vulnerability can easily be exploited to achieve a DOS attack in the following manner: one system may raise a proposal to set the proposalThreshold of the other system to a very high value. After execution, it will be practically impossible to raise any proposals on the attacked system which will render it practically unusable.

Response: We're looking into ways to mitigate this issue. In the meantime we will explain this possibility in our documentation and recommend against sharing a governance timelock with other executors.

Issue:	Two systems that use the same timelock can attack each other
Description:	In case that two rival systems use the same timelock in `GovernorTimelockControl`, each one of them can propse to invoke `onlyGovenrnace` functions on behalf the other system. Since the timelock is the executor of both those systems, the function will be invoked successfuly. This vulnerability can easily be exploited to achieve a DOS attack in the following manner: one system may raise a proposal to set the `proposalThreshold` of the other system to a very high value. After execution, it will be practically impossible to raise any proposals on the attacked system which will render it practically unusable.
Response:	We're looking into ways to mitigate this issue. In the meantime we will explain this possibility in our documentation and recommend against sharing a governance timelock with other executors.

Severity: High

Issue: Two systems that use the same timelock can not queue the same proposal

Description: Two systems that use the same TimelockController (given in the constructor), cannot queue the same proposal. In that case, the first system that calls queue() will queue the propsal and the second will revert. This can be exploited as a DoS attack if one system decide to attack the other. For example system A, that have a shorter voting period can always propose the same proposal in system B and queue them before system B can. That will make all the proposals in system B inaccessible.

Response: We're considering including the governor address as a salt so timelock ids do not clash between governors.

Issue:	Two systems that use the same timelock can not queue the same proposal
Description:	Two systems that use the same `TimelockController` (given in the constructor), cannot queue the same proposal. In that case, the first system that calls `queue()` will queue the propsal and the second will revert. This can be exploited as a DoS attack if one system decide to attack the other. For example system A, that have a shorter voting period can always propose the same proposal in system B and queue them before system B can. That will make all the proposals in system B inaccessible.
Response:	We're considering including the governor address as a salt so timelock ids do not clash between governors.

Severity: Low

Issue: Setting a new timelock removes all queued proposals along with the old timelock

Description: When queueing proposals in a timelock, the proposals are being stored and monitored by a specific address (timelock). Therefore, when changing a timelock, all the proposals that were queued but yet to be executed in the old timelock are now inaccessible through the current govenor. In this case, all these proposals that were in queueing state are lost, i.e. cannot be executed nor moved to the queue of the new timelock.
Note that the community can vote to change the timelock back to the old one, thereby regaining access to these queued proposals.

Response: Our recommendation would be to avoid changing the timelock while there are queued proposals. That said, we're considering alternatives to mitigate this at the contract level. Note that if the governor remains an executor in the timelock, a newer feature Governor.relay would allow triggering execution of a previously queued proposal.

Issue:	Setting a new timelock removes all queued proposals along with the old timelock
Description:	When queueing proposals in a timelock, the proposals are being stored and monitored by a specific address (timelock). Therefore, when changing a timelock, all the proposals that were queued but yet to be executed in the old timelock are now inaccessible through the current govenor. In this case, all these proposals that were in queueing state are lost, i.e. cannot be executed nor moved to the queue of the new timelock. Note that the community can vote to change the timelock back to the old one, thereby regaining access to these queued proposals.
Response:	Our recommendation would be to avoid changing the timelock while there are queued proposals. That said, we're considering alternatives to mitigate this at the contract level. Note that if the governor remains an executor in the timelock, a newer feature `Governor.relay` would allow triggering execution of a previously queued proposal.

Severity: Low

Issue: Voting period is 1 block less than expected

Description: The function state() categorize a proposal as Active if the current block number is in the range: [proposal.voteStart, proposal.voteEnd). On the other hand, when casting a vote, a require statment in the function demands: block.number > proposal.voteStart. This makes voting exactly at the start block impossible, even though the proposal is marked as Active. To put it simply, any user can vote only during the period [proposal.voteStart+1, proposal.voteEnd-1]. Hence, because the ending date of a proposal is being determined by 2 parameters:proposal.voteEnd = proposal.voteStart + votingPeriod, if the votingPeriod is set to 1 it is impossible to vote.
Note in particular that if a proposal's voting period is only one block long, the proposal will be entirely blocked.

Response: Fixed in a more recent commit. A proposal is considered Pending during block number voteStart.

Issue:	Voting period is 1 block less than expected
Description:	The function `state()` categorize a proposal as Active if the current block number is in the range: `[proposal.voteStart, proposal.voteEnd)`. On the other hand, when casting a vote, a `require` statment in the function demands: `block.number > proposal.voteStart`. This makes voting exactly at the start block impossible, even though the proposal is marked as Active. To put it simply, any user can vote only during the period `[proposal.voteStart+1, proposal.voteEnd-1]`. Hence, because the ending date of a proposal is being determined by 2 parameters:`proposal.voteEnd = proposal.voteStart + votingPeriod`, if the `votingPeriod` is set to 1 it is impossible to vote. Note in particular that if a proposal's voting period is only one block long, the proposal will be entirely blocked.
Response:	Fixed in a more recent commit. A proposal is considered Pending during block number voteStart.

Disclaimer

The Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of the Certora Prover are scoped to the provided specification, and the Certora Prover does not check any cases not covered by the specification.

We hope that this information is useful, but provide no warranty of any kind, explicit or implied. The contents of this report should not be construed as a complete guarantee that the contract is secure in all dimensions. In no event shall Certora or any of its employees be liable for any claim, damages or other liability, whether in an action of contract, tort or otherwise, arising from, out of or in connection with the results reported here.

Summary of formal verification

Overview of OpenZeppelin/Governance contracts

Our verification efforts focused on the OpenZeppelin Governance module. The Governance module contains several abstract contracts that implement the core functionality of a governance system. Developers can combine and extend these contracts to implement a governance system that fits their individual needs. See the OpenZeppelin Contracts documentation for a high-level overview of the Governance module, and the Governance API for a detailed description.

A governance system allows a community of stakeholders to collectively make decisions about a project by voting on proposals. The governance system defines the requirements for creating proposals, the voting process, the requirements for accepting or rejecting a proposal, and the process for executing a proposal that has been accepted.

For our verification effort, we created multiple concrete governance systems by combining the components defined by the OpenZeppelin Governance module. Our concrete systems were based on the output of the OpenZeppelin Contracts Wizard. We then wrote general-purpose verification conditions that describe the correct operation of a governance system, and verified that the concrete governance systems satisfied those specifications.

The remainder of this section describes the rules and invariants that we have checked.

Assumptions and simplifications made during verification

We made the following assumptions during our verification:

When verifying contracts that make external calls, we assume that those calls can have arbitrary side effects outside of the contracts, but that they do not affect the state of the contract being verified. This means that some reentrancy bugs may not be caught.
Due to limitations of the Certora Prover, two of the rules listed below timed out on certain methods. The list of unverified methods is included in the detailed description of each rule listed below. The Certora team is working to address these limitations.
We assume that the values returned by different calls to ERC20Votes.getPastTotalSupply and ERC20Votes.getPastVotes in the same transaction return the same value.
We assume that hash operations return an arbitrary deterministic value
We unroll loops. Violations that require a loop to execute more than once will not be detected.

Verification conditions

Notation

Image Not Showing Possible Reasons

The image was uploaded to a note which you don't have access to
The note which the image was originally uploaded to has been deleted

Learn More →

indicates the rule is formally verified on the latest reviewed commit. Footnotes describe any simplifications or assumptions used while verifying the rules (beyond the general assumptions listed above).

In this document, verification conditions are either shown as logical formulas or Hoare triples of the form {p} C {q}. A verification condition given by a logical formula denotes an invariant that holds if every reachable state satisfies the condition.

Hoare triples of the form {p} C {q} hold if any non-reverting execution of program C that starts in a state satsifying the precondition p ends in a state satisfying the postcondition q. The notation {p} C@withrevert {q} is similar but applies to both reverting and non-reverting executions. Preconditions and postconditions are similar to the Solidity require and assert statements.

Formulas relate the results of method calls. In most cases, these methods are getters defined in the contracts, but in some cases they are getters we have added to our harness or definitions provided in the rules file. Undefined variables in the formulas are treated as arbitrary: the rule is checked for every possible value of the variables.

Properties

( Image Not Showing Possible Reasons The image was uploaded to a note which you don't have access to The note which the image was originally uploaded to has been deleted Learn More → ) startAndEndDatesNonZero

Start and end dates are either initialized (non zero) or uninitialized (zero) simultaneously.

proposalSnapshot(proposalId) ≠ 0 ⇔ proposalDeadline(proposalId) ≠ 0

A proposal starting block number must be less than or equal to the proposal end block number.

proposalSnapshot(proposalId) > 0 ⇒  proposalSnapshot(proposalId) ≤ proposalDeadline(proposalId)

If a proposal is canceled it must have a start date and an end date.

isCanceled(proposalId) ⇒ proposalSnapshot(proposalId) ≠ 0

If a proposal is executed it must have a start date and an end date.

isExecuted(proposalId) ⇒ proposalSnapshot(proposalId) ≠ 0

A proposal cannot be both executed and canceled simultaneously.

¬isExecuted(proposalId) v ¬isCanceled(proposalId)

A proposal can be executed only if quorum was reached and vote succeeded.

{   
    isExecutedBefore = isExecuted(proposalId) ∧
    quorumReachedBefore = _quorumReached(e, proposalId) ∧
    voteSucceededBefore = _voteSucceeded(proposalId)
}
    <transaction>
{    
    isExecutedAfter = isExecuted(proposalId) ∧ 
    ((¬isExecutedBefore ∧ isExecutedAfter) ⇒ (quorumReachedBefore ∧ voteSucceededBefore))
}

A user cannot vote twice.

{ 
    hasVoted(proposalId, msg.sender) 
}
    castVote@withrevert(proposalId, support)
{ 
    lastReverted 
}

Once a proposal is created, voteStart and voteEnd are immutable.

{    
    _voteStart = proposalSnapshot(proposalId) ∧
    uint256 _voteEnd = proposalDeadline(proposalId) ∧
    proposalCreated(proposalId)
}
    <transaction>
{    
    voteStart_ = proposalSnapshot(proposalId) ∧
    voteEnd_ = proposalDeadline(proposalId) ∧
    _voteStart == voteStart_ ∧ _voteEnd == voteEnd_
}

Voting cannot start at a block number prior to proposal’s creation block number.

{
    previousStart = proposalSnapshot(proposalId) ∧
    ¬proposalCreated(proposalId)
}
    propose(e, args)
{
    newStart = proposalSnapshot(proposalId) ∧
    newStart ≠ previousStart ⇒ newStart ≥ e.block.number
}

A proposal can neither be executed nor canceled before it ends.

{
    ¬isExecuted(proposalId) ∧ ¬isCanceled(proposalId)
}
    <transaction>
{
    e.block.number < proposalDeadline(proposalId) ⇒ (¬isExecuted(proposalId) ∧ ¬isCanceled(proposalId))
}

Proposal can be switched to executed only via execute() function

{ ¬isExecuted(proposalId) }

<non-execute operation on proposalId>

{ ¬isExecuted(proposalId) }

All non-view functions should revert if proposal is executed/canceled.

{ isExecuted(proposalId) }

<non-view operation on proposalId>@withrevert

{ lastReverted }

and

{ isCanceled(proposalId) }

<non-view operation on proposalId>@withrevert

{ lastReverted }

The sum of all votes casted is equal to the sum of voting power of those who voted, per proposal.

tracked_weight(proposalId) == ghost_sum_vote_power_by_id(proposalId)

The sum of all votes casted is equal to the sum of voting power of those who voted.

sum_tracked_weight() == sum_all_votes_power()

The sum of all votes casted is greater or equal to the sum of voting power of those who voted as per specific proposal.

sum_all_votes_power() ≥ tracked_weight(proposalId)

Only sender's voting status can be changed by execution of any cast vote function.

{
    userVoteBefore = hasVoted(proposalId, user)
}
    castVote(proposalId, sup)
{
    userVoteAfter = hasVoted(proposalId, user) ∧
    user ≠ msg.sender ⇒ otherUserVoteBefore = otherUserVoteAfter
}

Total voting tally is monotonically non-decreasing in every operation.

{
    votingWeightBefore = sum_tracked_weight()
}
    <transaction>
{
    votingWeightAfter = sum_tracked_weight() ∧
    votingWeightBefore ≤ votingWeightAfter
}

A change in hasVoted must be correlated with a non-decreasing change of the vote supports (non-decreasing because user is allowed to vote with weight 0).

{
    acc = e.msg.sender ∧
    againstBefore = votesAgainst() ∧
    forBefore = votesFor() ∧
    abstainBefore = votesAbstain() ∧
    hasVotedBefore = hasVoted(e, proposalId, acc)
}
    <transaction on proposalId>
{
    (againstAfter = votesAgainst() ∧
    forAfter = votesFor() ∧
    abstainAfter = votesAbstain() ∧
    hasVotedAfter = hasVoted(e, proposalId, acc) ∧
    hasVotedAfter_User = hasVoted(e, proposalId, user) c
    ((¬hasVotedBefore ∧ hasVotedAfter) ⇒ againstBefore ≤ againstAfter ∨ forBefore ≤ forAfter v abstainBefore ≤ abstainAfter))
}

Only privileged users can execute privileged operations, e.g. change _quorumNumerator or _timelock.

{
    quorumNumBefore = quorumNumerator(e)
}
    <transaction>
{
    quorumNumAfter = quorumNumerator(e) ∧
    address executorCheck = getExecutor(e) ∧
    (quorumNumBefore ≠ quorumNumAfter ⇒ e.msg.sender == executorCheck)
}

and

{ timelockBefore = timelock() }

<transaction>

{ (timelock() ≠ timeLockBefore ⇒ e.msg.sender == timelockBefore) }

we verified this property on the castVote method but not the other two vote casting functions. We feel this is reasonable since the bulk of the code for all three functions is contained in the _castVote helper method. ↩︎ ↩︎
due to timeouts, these properties were not verified on calls to view functions, updateQuorumNumerator(), updateTimelock(), queue and __acceptAdmin() methods ↩︎

Michael George

2021/11/30 13:54:00

## Main Issues Discovered **Severity: <span style="c

Revisit (Edited)

2021/11/30 21:59:54

This is unclear (Edited)

2021/11/30 22:25:35

## Assumptions and simplifications made during verification We made the following assumpt

We should discuss (Edited)

2021/11/30 22:55:39

## Assum

Remove the rest of this section probably (Edited)

2021/11/30 22:56:16

- We

2021/12/01 12:57:41

- We ass

I think we should include an exhaustive list (Edited)

2021/12/01 13:10:54

The particular examples shown should be removed, since they either have no semantic effect or increase the generality of the verification (Edited)

2021/12/01 13:19:23

remove (Edited)

2021/12/01 13:20:04

No need to mention requireInvariants (Edited)

2021/12/01 13:20:55

I think this is important but should be included in the rules instead of here (Edited)

2021/12/01 13:21:21

is this an invariant that we prove? (Edited)

2021/12/01 14:48:35

This is a definition rather than a property

2021/12/01 13:23:00

use \lor instead of v (Edited)

2021/12/01 13:24:44

This would be a good place to put the state transition diagram (Edited)

2021/12/01 13:58:06

d multip

Is this accurate? (Edited)

2021/12/01 14:35:35

unroll

Double check (Edited)

2021/12/01 20:25:00

Default is actually 1; we should try running with 2 or more

2021/12/01 14:36:23

Move to new section (Edited)

2021/12/01 14:37:52

move (Edited)

2021/12/01 14:53:00

verification:

Make sure that these cover Yoav's bugs that rules don't catch (Edited)

2021/12/01 14:53:16

invoke `o

Explicitly note bugs not caught by the tool (Edited)

2021/12/01 14:54:34

mands: `block.number > proposa

Maybe raise to medium (Edited)

2021/12/01 14:54:43

can vot

mention that this can lock the system (Edited)

2021/12/01 14:54:52

Fix (Edited)

2021/12/01 20:12:30

Include rule names (Edited)

2021/12/01 20:23:20

ue to limitat

Update with list of methods and add footnotes to the relevant rules (Edited)

2021/12/01 22:20:34

Add some structure / organization to the conditions (Edited)

2021/12/02 19:24:43

oth

Fill in with which rule is violated, or why there is no such rule (Edited)

Francisco Giordano

2021/12/02 21:23:34

public git repository

The link seems odd. If we can open a PR including the rules I think it would make a good link here. (Edited)