mirror
/
openzeppelin-contracts
mirror of https://github.com/OpenZeppelin/openzeppelin-contracts
2
1
Fork 1
Code Issues Releases Wiki Activity

Improve FV specifications for AccessControlDefaultAdminRules (#4223)

Browse Source 
Co-authored-by: ernestognw <ernestognw@gmail.com>
Co-authored-by: Francisco <fg@frang.io>
fv/Governor^2
Hadrien Croubois 2 years ago committed by GitHub
parent dfef6a68ee
commit a1d57bac50
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 113 additions and 140 deletions
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Show Stats Download Patch File Download Diff File
  1. 244
      certora/specs/AccessControlDefaultAdminRules.spec
  2. 9
      certora/specs/helpers/helpers.spec

244
certora/specs/AccessControlDefaultAdminRules.spec
Unescape View File

@ -12,44 +12,23 @@ use rule onlyGrantCanGrant filtered {
│ Helpers │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition timeSanity(env e) returns bool =
e.block.timestamp > 0 && e.block.timestamp + defaultAdminDelay(e) < max_uint48();
function max_uint48() returns mathint {
return (1 << 48) - 1;
}
definition delayChangeWaitSanity(env e, uint48 newDelay) returns bool =
e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48();
function nonZeroAccount(address account) returns bool {
return account != 0;
}
definition isSet(uint48 schedule) returns bool =
schedule != 0;
function timeSanity(env e) returns bool {
return
e.block.timestamp > 0 && // Avoids 0 schedules
e.block.timestamp + defaultAdminDelay(e) < max_uint48();
}
definition hasPassed(env e, uint48 schedule) returns bool =
schedule < e.block.timestamp;
function delayChangeWaitSanity(env e, uint48 newDelay) returns bool {
return e.block.timestamp + delayChangeWait_(e, newDelay) < max_uint48();
}
definition increasingDelaySchedule(env e, uint48 newDelay) returns mathint =
e.block.timestamp + min(newDelay, defaultAdminDelayIncreaseWait());
function isSet(uint48 schedule) returns bool {
return schedule != 0;
}
function hasPassed(env e, uint48 schedule) returns bool {
return schedule < e.block.timestamp;
}
function min(uint48 a, uint48 b) returns mathint {
return a < b ? a : b;
}
function increasingDelaySchedule(env e, uint48 newDelay) returns mathint {
return e.block.timestamp + min(newDelay, defaultAdminDelayIncreaseWait());
}
function decreasingDelaySchedule(env e, uint48 newDelay) returns mathint {
return e.block.timestamp + defaultAdminDelay(e) - newDelay;
}
definition decreasingDelaySchedule(env e, uint48 newDelay) returns mathint =
e.block.timestamp + defaultAdminDelay(e) - newDelay;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@ -57,11 +36,10 @@ function decreasingDelaySchedule(env e, uint48 newDelay) returns mathint {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant defaultAdminConsistency(address account)
defaultAdmin() == account <=> hasRole(DEFAULT_ADMIN_ROLE(), account)
(account == defaultAdmin() && account != 0) <=> hasRole(DEFAULT_ADMIN_ROLE(), account)
{
preserved {
// defaultAdmin() returns the zero address when there's no default admin
require nonZeroAccount(account);
preserved with (env e) {
require nonzerosender(e);
}
}
@ -72,10 +50,12 @@ invariant defaultAdminConsistency(address account)
*/
invariant singleDefaultAdmin(address account, address another)
hasRole(DEFAULT_ADMIN_ROLE(), account) && hasRole(DEFAULT_ADMIN_ROLE(), another) => another == account
// We filter here because we couldn't find a way to force Certora to have an initial state with
// only one DEFAULT_ADMIN_ROLE enforced, so a counter example is a different default admin since inception
// triggering the transfer, which is known to be impossible by definition.
filtered { f -> f.selector != acceptDefaultAdminTransfer().selector }
{
preserved {
requireInvariant defaultAdminConsistency(account);
requireInvariant defaultAdminConsistency(another);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@ -118,7 +98,8 @@ rule revokeRoleEffect(env e, bytes32 role) {
"roles can only be revoked by their owner except for the default admin role";
// effect
assert success => !hasRole(role, account), "role is revoked";
assert success => !hasRole(role, account),
"role is revoked";
// no side effect
assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount),
@ -137,35 +118,59 @@ rule renounceRoleEffect(env e, bytes32 role) {
address account;
address otherAccount;
bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
uint48 scheduleBefore = pendingDefaultAdminSchedule_();
bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
address adminBefore = defaultAdmin();
address pendingAdminBefore = pendingDefaultAdmin_();
uint48 scheduleBefore = pendingDefaultAdminSchedule_();
renounceRole@withrevert(e, role, account);
bool success = !lastReverted;
bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
address adminAfter = defaultAdmin();
address pendingAdminAfter = pendingDefaultAdmin_();
uint48 scheduleAfter = pendingDefaultAdminSchedule_();
// liveness
assert success <=> (
account == e.msg.sender &&
(
role != DEFAULT_ADMIN_ROLE() ||
account != adminBefore ||
(
role != DEFAULT_ADMIN_ROLE()
) || (
role == DEFAULT_ADMIN_ROLE() &&
pendingAdminBefore == 0 &&
isSet(scheduleBefore) &&
hasPassed(e, scheduleBefore)
)
)
), "an account only can renounce by itself with a delay for the default admin role";
),
"an account only can renounce by itself with a delay for the default admin role";
// effect
assert success => !hasRole(role, account), "role is renounced";
assert success => !hasRole(role, account),
"role is renounced";
assert success => (
(
role == DEFAULT_ADMIN_ROLE() &&
account == adminBefore
) ? (
adminAfter == 0 &&
pendingAdminAfter == 0 &&
scheduleAfter == 0
) : (
adminAfter == adminBefore &&
pendingAdminAfter == pendingAdminBefore &&
scheduleAfter == scheduleBefore
)
),
"renouncing default admin role cleans state iff called by previous admin";
// no side effect
assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount),
assert hasOtherRoleBefore != hasOtherRoleAfter => (
role == otherRole &&
account == otherAccount
),
"no other role is affected";
}
@ -175,10 +180,6 @@ rule renounceRoleEffect(env e, bytes32 role) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule noDefaultAdminChange(env e, method f, calldataarg args) {
require nonZeroAccount(e.msg.sender);
requireInvariant defaultAdminConsistency(defaultAdmin());
requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
address adminBefore = defaultAdmin();
f(e, args);
address adminAfter = defaultAdmin();
@ -186,18 +187,17 @@ rule noDefaultAdminChange(env e, method f, calldataarg args) {
assert adminBefore != adminAfter => (
f.selector == acceptDefaultAdminTransfer().selector ||
f.selector == renounceRole(bytes32,address).selector
), "default admin is only affected by accepting an admin transfer or renoucing";
),
"default admin is only affected by accepting an admin transfer or renoucing";
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: pendingDefaultAdmin is only affected by beginning, accepting or canceling an admin transfer │
│ Rule: pendingDefaultAdmin is only affected by beginning, completing (accept or renounce), or canceling an admin │
│ transfer │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule noPendingDefaultAdminChange(env e, method f, calldataarg args) {
requireInvariant defaultAdminConsistency(defaultAdmin());
requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
address pendingAdminBefore = pendingDefaultAdmin_();
address scheduleBefore = pendingDefaultAdminSchedule_();
f(e, args);
@ -210,8 +210,10 @@ rule noPendingDefaultAdminChange(env e, method f, calldataarg args) {
) => (
f.selector == beginDefaultAdminTransfer(address).selector ||
f.selector == acceptDefaultAdminTransfer().selector ||
f.selector == cancelDefaultAdminTransfer().selector
), "pending admin and its schedule is only affected by beginning, accepting or cancelling an admin transfer";
f.selector == cancelDefaultAdminTransfer().selector ||
f.selector == renounceRole(bytes32,address).selector
),
"pending admin and its schedule is only affected by beginning, completing, or cancelling an admin transfer";
}
/*
@ -224,7 +226,8 @@ rule noDefaultAdminDelayChange(env e, method f, calldataarg args) {
f(e, args);
uint48 delayAfter = defaultAdminDelay(e);
assert delayBefore == delayAfter, "delay can't be changed atomically by any function";
assert delayBefore == delayAfter,
"delay can't be changed atomically by any function";
}
/*
@ -240,7 +243,8 @@ rule noPendingDefaultAdminDelayChange(env e, method f, calldataarg args) {
assert pendingDelayBefore != pendingDelayAfter => (
f.selector == changeDefaultAdminDelay(uint48).selector ||
f.selector == rollbackDefaultAdminDelay().selector
), "pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay";
),
"pending delay is only affected by changeDefaultAdminDelay or rollbackDefaultAdminDelay";
}
/*
@ -263,10 +267,10 @@ rule noDefaultAdminDelayIncreaseWaitChange(env e, method f, calldataarg args) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule beginDefaultAdminTransfer(env e, address newAdmin) {
require nonpayable(e);
require timeSanity(e);
requireInvariant defaultAdminConsistency(defaultAdmin());
requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
require nonpayable(e);
require nonzerosender(e);
requireInvariant defaultAdminConsistency(e.msg.sender);
beginDefaultAdminTransfer@withrevert(e, newAdmin);
bool success = !lastReverted;
@ -288,18 +292,24 @@ rule beginDefaultAdminTransfer(env e, address newAdmin) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args, address newAdmin) {
require e1.block.timestamp < e2.block.timestamp;
require e1.block.timestamp <= e2.block.timestamp;
uint48 delayBefore = defaultAdminDelay(e1);
address adminBefore = defaultAdmin();
// There might be a better way to generalize this without requiring `beginDefaultAdminTransfer`, but currently
// it's the only way in which we can attest that only `delayBefore` has passed before a change.
beginDefaultAdminTransfer(e1, newAdmin);
f(e2, args);
address adminAfter = defaultAdmin();
assert adminAfter == newAdmin => ((e2.block.timestamp >= e1.block.timestamp + delayBefore) || adminBefore == newAdmin),
"A delay can't change in less than applied schedule";
// change can only happen towards the newAdmin, with the delay
assert adminAfter != adminBefore => (
adminAfter == newAdmin &&
e2.block.timestamp >= e1.block.timestamp + delayBefore
),
"The admin can only change after the enforced delay and to the previously scheduled new admin";
}
/*
@ -309,17 +319,19 @@ rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args
*/
rule acceptDefaultAdminTransfer(env e) {
require nonpayable(e);
requireInvariant defaultAdminConsistency(defaultAdmin());
requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
address pendingAdminBefore = pendingDefaultAdmin_();
uint48 scheduleAfter = pendingDefaultAdminSchedule_();
uint48 scheduleBefore = pendingDefaultAdminSchedule_();
acceptDefaultAdminTransfer@withrevert(e);
bool success = !lastReverted;
// liveness
assert success <=> e.msg.sender == pendingAdminBefore && isSet(scheduleAfter) && hasPassed(e, scheduleAfter),
assert success <=> (
e.msg.sender == pendingAdminBefore &&
isSet(scheduleBefore) &&
hasPassed(e, scheduleBefore)
),
"only the pending default admin can accept the role after the schedule has been set and passed";
// effect
@ -338,8 +350,8 @@ rule acceptDefaultAdminTransfer(env e) {
*/
rule cancelDefaultAdminTransfer(env e) {
require nonpayable(e);
requireInvariant defaultAdminConsistency(defaultAdmin());
requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
require nonzerosender(e);
requireInvariant defaultAdminConsistency(e.msg.sender);
cancelDefaultAdminTransfer@withrevert(e);
bool success = !lastReverted;
@ -361,11 +373,11 @@ rule cancelDefaultAdminTransfer(env e) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule changeDefaultAdminDelay(env e, uint48 newDelay) {
require nonpayable(e);
require timeSanity(e);
require nonpayable(e);
require nonzerosender(e);
require delayChangeWaitSanity(e, newDelay);
requireInvariant defaultAdminConsistency(defaultAdmin());
requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
requireInvariant defaultAdminConsistency(e.msg.sender);
uint48 delayBefore = defaultAdminDelay(e);
@ -377,7 +389,9 @@ rule changeDefaultAdminDelay(env e, uint48 newDelay) {
"only the current default admin can begin a delay change";
// effect
assert success => pendingDelay_(e) == newDelay, "pending delay is set";
assert success => pendingDelay_(e) == newDelay,
"pending delay is set";
assert success => (
pendingDelaySchedule_(e) > e.block.timestamp ||
delayBefore == newDelay || // Interpreted as decreasing, x - x = 0
@ -392,17 +406,22 @@ rule changeDefaultAdminDelay(env e, uint48 newDelay) {
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule pendingDelayWaitEnforced(env e1, env e2, method f, calldataarg args, uint48 newDelay) {
require e1.block.timestamp < e2.block.timestamp;
require e1.block.timestamp <= e2.block.timestamp;
uint48 delayBefore = defaultAdminDelay(e1);
changeDefaultAdminDelay(e1, newDelay);
f(e2, args);
uint48 delayAfter = defaultAdminDelay(e2);
mathint delayWait = newDelay > delayBefore ? increasingDelaySchedule(e1, newDelay) : decreasingDelaySchedule(e1, newDelay);
assert delayAfter == newDelay => (e2.block.timestamp >= delayWait || delayBefore == newDelay),
"A delay can't change in less than applied schedule";
assert delayAfter != delayBefore => (
delayAfter == newDelay &&
e2.block.timestamp >= delayWait
),
"A delay can only change after the applied schedule";
}
/*
@ -427,8 +446,8 @@ rule pendingDelayWait(env e, uint48 newDelay) {
*/
rule rollbackDefaultAdminDelay(env e) {
require nonpayable(e);
requireInvariant defaultAdminConsistency(defaultAdmin());
requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
require nonzerosender(e);
requireInvariant defaultAdminConsistency(e.msg.sender);
rollbackDefaultAdminDelay@withrevert(e);
bool success = !lastReverted;
@ -443,58 +462,3 @@ rule rollbackDefaultAdminDelay(env e) {
assert success => pendingDelaySchedule_(e) == 0,
"Pending default admin delay is reset";
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: pending default admin and the delay can only change along with their corresponding schedules │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule pendingValueAndScheduleCoupling(env e, address newAdmin, uint48 newDelay) {
requireInvariant defaultAdminConsistency(defaultAdmin());
requireInvariant singleDefaultAdmin(e.msg.sender, defaultAdmin());
// Pending admin
address pendingAdminBefore = pendingDefaultAdmin_();
uint48 pendingAdminScheduleBefore = pendingDefaultAdminSchedule_();
beginDefaultAdminTransfer(e, newAdmin);
address pendingAdminAfter = pendingDefaultAdmin_();
uint48 pendingAdminScheduleAfter = pendingDefaultAdminSchedule_();
assert (
pendingAdminScheduleBefore != pendingDefaultAdminSchedule_() &&
pendingAdminBefore == pendingAdminAfter
) => newAdmin == pendingAdminBefore, "pending admin stays the same if the new admin set is the same";
assert (
pendingAdminBefore != pendingAdminAfter &&
pendingAdminScheduleBefore == pendingDefaultAdminSchedule_()
) => (
// Schedule doesn't change if:
// - The defaultAdminDelay was reduced to a value such that added to the block.timestamp is equal to previous schedule
e.block.timestamp + defaultAdminDelay(e) == pendingAdminScheduleBefore
), "pending admin stays the same if a default admin transfer is begun on accepted edge cases";
// Pending delay
address pendingDelayBefore = pendingDelay_(e);
uint48 pendingDelayScheduleBefore = pendingDelaySchedule_(e);
changeDefaultAdminDelay(e, newDelay);
address pendingDelayAfter = pendingDelay_(e);
uint48 pendingDelayScheduleAfter = pendingDelaySchedule_(e);
assert (
pendingDelayScheduleBefore != pendingDelayScheduleAfter &&
pendingDelayBefore == pendingDelayAfter
) => newDelay == pendingDelayBefore || pendingDelayBefore == 0, "pending delay stays the same if the new delay set is the same";
assert (
pendingDelayBefore != pendingDelayAfter &&
pendingDelayScheduleBefore == pendingDelayScheduleAfter
) => (
increasingDelaySchedule(e, newDelay) == pendingDelayScheduleBefore ||
decreasingDelaySchedule(e, newDelay) == pendingDelayScheduleBefore
), "pending delay stays the same if a default admin transfer is begun on accepted edge cases";
}

9
certora/specs/helpers/helpers.spec
Unescape View File

@ -1 +1,10 @@
// environment
definition nonpayable(env e) returns bool = e.msg.value == 0;
definition nonzerosender(env e) returns bool = e.msg.sender != 0;
// constants
definition max_uint48() returns mathint = (1 << 48) - 1;
// math
definition min(mathint a, mathint b) returns mathint = a < b ? a : b;
definition max(mathint a, mathint b) returns mathint = a > b ? a : b;

Write Preview
Loading…
Cancel
Save