|
|
@@ -1,85 +1,133 @@
|
|
|
methods {
|
|
|
- grantRole(bytes32, address)
|
|
|
- revokeRole(bytes32, address)
|
|
|
- _checkRole(bytes32)
|
|
|
- safeTransferFrom(address, address, uint256, uint256, bytes)
|
|
|
- safeBatchTransferFrom(address, address, uint256[], uint256[], bytes)
|
|
|
-
|
|
|
- getRoleAdmin(bytes32) returns(bytes32) envfree
|
|
|
hasRole(bytes32, address) returns(bool) envfree
|
|
|
-}
|
|
|
-
|
|
|
-
|
|
|
-// STATUS - verified
|
|
|
-// If `onlyRole` modifier reverts then `grantRole()` reverts
|
|
|
-rule onlyRoleModifierCheckGrant(env e){
|
|
|
- bytes32 role; address account;
|
|
|
-
|
|
|
- _checkRole@withrevert(e, getRoleAdmin(role));
|
|
|
- bool checkRevert = lastReverted;
|
|
|
-
|
|
|
- grantRole@withrevert(e, role, account);
|
|
|
- bool grantRevert = lastReverted;
|
|
|
+ getRoleAdmin(bytes32) returns(bytes32) envfree
|
|
|
|
|
|
- assert checkRevert => grantRevert, "modifier goes bananas";
|
|
|
+ grantRole(bytes32, address)
|
|
|
+ revokeRole(bytes32, address)
|
|
|
+ renounceRole(bytes32, address)
|
|
|
}
|
|
|
|
|
|
|
|
|
-// STATUS - verified
|
|
|
-// check onlyRole modifier for revokeRole()
|
|
|
-rule onlyRoleModifierCheckRevoke(env e){
|
|
|
- bytes32 role; address account;
|
|
|
+/*
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+โ Rule: only grantRole can grant a role โ
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+*/
|
|
|
+rule onlyGrantCanGrant(env e, bytes32 role, address account) {
|
|
|
+ require !hasRole(role, account);
|
|
|
|
|
|
- _checkRole@withrevert(e, getRoleAdmin(role));
|
|
|
- bool checkRevert = lastReverted;
|
|
|
+ method f; calldataarg args;
|
|
|
+ f(e, args);
|
|
|
|
|
|
- revokeRole@withrevert(e, role, account);
|
|
|
- bool revokeRevert = lastReverted;
|
|
|
-
|
|
|
- assert checkRevert => revokeRevert, "modifier goes bananas";
|
|
|
+ assert hasRole(role, account) => f.selector == grantRole(bytes32, address).selector;
|
|
|
}
|
|
|
|
|
|
+/*
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+โ Rule: only revokeRole and renounceRole can grant a role โ
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+*/
|
|
|
+rule onlyRevokeAndRenounceCanRevoke(env e, bytes32 role, address account) {
|
|
|
+ require hasRole(role, account);
|
|
|
|
|
|
-// STATUS - verified
|
|
|
-// grantRole() does not affect another accounts
|
|
|
-rule grantRoleEffect(env e){
|
|
|
- bytes32 role; address account;
|
|
|
- bytes32 anotherRole; address nonEffectedAcc;
|
|
|
- require account != nonEffectedAcc;
|
|
|
-
|
|
|
- bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc);
|
|
|
+ method f; calldataarg args;
|
|
|
+ f(e, args);
|
|
|
|
|
|
- grantRole(e, role, account);
|
|
|
-
|
|
|
- bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc);
|
|
|
-
|
|
|
- assert hasRoleBefore == hasRoleAfter, "modifier goes bananas";
|
|
|
+ assert !hasRole(role, account) => (f.selector == revokeRole(bytes32, address).selector || f.selector == renounceRole(bytes32, address).selector);
|
|
|
}
|
|
|
|
|
|
+/*
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+โ Rule: only an account with admin role can call grantRole โ
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+*/
|
|
|
+rule onlyAdminCanGrant(env e, bytes32 role, address account) {
|
|
|
+ bool isAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
|
|
|
|
|
|
-// STATUS - verified
|
|
|
-// revokeRole() does not affect another accounts
|
|
|
-rule revokeRoleEffect(env e){
|
|
|
- bytes32 role; address account;
|
|
|
- bytes32 anotherRole; address nonEffectedAcc;
|
|
|
- require account != nonEffectedAcc;
|
|
|
-
|
|
|
- bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc);
|
|
|
-
|
|
|
- revokeRole(e, role, account);
|
|
|
-
|
|
|
- bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc);
|
|
|
+ grantRole@withrevert(e, role, account);
|
|
|
|
|
|
- assert hasRoleBefore == hasRoleAfter, "modifier goes bananas";
|
|
|
+ assert !lastReverted => isAdmin;
|
|
|
}
|
|
|
|
|
|
+/*
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+โ Rule: only an account with admin role can call revokeRole โ
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+*/
|
|
|
+rule onlyAdminCanRevoke(env e, bytes32 role, address account) {
|
|
|
+ bool isAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
|
|
|
|
|
|
+ revokeRole@withrevert(e, role, account);
|
|
|
|
|
|
+ assert !lastReverted => isAdmin;
|
|
|
+}
|
|
|
|
|
|
+/*
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+โ Rule: only the affected account can revoke โ
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+*/
|
|
|
+rule onlyUserCanRenounce(env e, bytes32 role, address account) {
|
|
|
+ renounceRole@withrevert(e, role, account);
|
|
|
+ assert !lastReverted => account == e.msg.sender;
|
|
|
+}
|
|
|
|
|
|
+/*
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+โ Rule: grantRole only affects the specified user/role combo โ
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+*/
|
|
|
+rule grantRoleEffect(env e) {
|
|
|
+ bytes32 role1; bytes32 role2;
|
|
|
+ address account1; address account2;
|
|
|
+
|
|
|
+ bool hasRoleBefore = hasRole(role1, account1);
|
|
|
+ grantRole(e, role2, account2);
|
|
|
+ bool hasRoleAfter = hasRole(role1, account1);
|
|
|
+
|
|
|
+ assert (
|
|
|
+ hasRoleBefore != hasRoleAfter
|
|
|
+ ) => (
|
|
|
+ hasRoleAfter == true && role1 == role2 && account1 == account2
|
|
|
+ );
|
|
|
+}
|
|
|
|
|
|
+/*
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+โ Rule: revokeRole only affects the specified user/role combo โ
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+*/
|
|
|
+rule revokeRoleEffect(env e) {
|
|
|
+ bytes32 role1; bytes32 role2;
|
|
|
+ address account1; address account2;
|
|
|
+
|
|
|
+ bool hasRoleBefore = hasRole(role1, account1);
|
|
|
+ revokeRole(e, role2, account2);
|
|
|
+ bool hasRoleAfter = hasRole(role1, account1);
|
|
|
+
|
|
|
+ assert (
|
|
|
+ hasRoleBefore != hasRoleAfter
|
|
|
+ ) => (
|
|
|
+ hasRoleAfter == false && role1 == role2 && account1 == account2
|
|
|
+ );
|
|
|
+}
|
|
|
|
|
|
-
|
|
|
-
|
|
|
-
|
|
|
-
|
|
|
+/*
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+โ Rule: renounceRole only affects the specified user/role combo โ
|
|
|
+โโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโโ
|
|
|
+*/
|
|
|
+rule renounceRoleEffect(env e) {
|
|
|
+ bytes32 role1; bytes32 role2;
|
|
|
+ address account1; address account2;
|
|
|
+
|
|
|
+ bool hasRoleBefore = hasRole(role1, account1);
|
|
|
+ renounceRole(e, role2, account2);
|
|
|
+ bool hasRoleAfter = hasRole(role1, account1);
|
|
|
+
|
|
|
+ assert (
|
|
|
+ hasRoleBefore != hasRoleAfter
|
|
|
+ ) => (
|
|
|
+ hasRoleAfter == false && role1 == role2 && account1 == account2
|
|
|
+ );
|
|
|
+}
|
Hadrien Croubois