NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add setAuthority rule to AccessManaged

Browse Source
This commit is contained in:
ernestognw
2024-04-19 12:02:44 -06:00
parent 52665fd9b3
commit cd86596938
2 changed files with 32 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

24
certora/specs/AccessManaged.spec
View File

@ -7,9 +7,10 @@ methods {
function authority_canCall_immediate(address) external returns (bool);
function authority_canCall_delay(address) external returns (uint32);
function authority_getSchedule(address) external returns (uint48);
function _hasCode(address) external returns (bool) envfree;
// Summaries
function _.setAuthority(address) external => DISPATCHER(true);
function _.setAuthority(address) external => DISPATCHER(true);
}
invariant isConsumingScheduledOpClean()
@ -35,3 +36,24 @@ rule callRestrictedFunction(env e) {
)
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: Only valid authorities can be set by the current authority │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setAuthority(env e) {
require nonpayable(e);
address newAuthority;
address previousAuthority = authority();
setAuthority@withrevert(e, newAuthority);
bool success = !lastReverted;
assert (success && authority() == newAuthority) <=> (
previousAuthority == e.msg.sender &&
_hasCode(newAuthority)
);
}