diff --git a/packages/authorizer/certora/conf/authorizer.conf b/packages/authorizer/certora/conf/authorizer.conf index bdda21c7..59ea1032 100644 --- a/packages/authorizer/certora/conf/authorizer.conf +++ b/packages/authorizer/certora/conf/authorizer.conf @@ -1,9 +1,9 @@ { "files": [ - "contracts/Authorizer.sol", + "certora/harnesses/AuthorizerHarness.sol", "certora/helpers/Helpers.sol" ], - "verify": "Authorizer:certora/specs/Authorizer.spec", + "verify": "AuthorizerHarness:certora/specs/Authorizer.spec", "loop_iter": "3", "rule_sanity": "basic", "send_only": true, @@ -19,5 +19,5 @@ ], "solc_allow_path": ".", "process": "emv", - "msg": "Authorizer" + "msg": "AuthorizerHarness" } diff --git a/packages/authorizer/certora/harnesses/AuthorizerHarness.sol b/packages/authorizer/certora/harnesses/AuthorizerHarness.sol new file mode 100644 index 00000000..d55b9641 --- /dev/null +++ b/packages/authorizer/certora/harnesses/AuthorizerHarness.sol @@ -0,0 +1,36 @@ +// SPDX-License-Identifier: GPL-3.0-or-later + +pragma solidity ^0.8.17; + +import '../../contracts/Authorizer.sol'; + +contract AuthorizerHarness is Authorizer { + constructor() { + // solhint-disable-previous-line no-empty-blocks + } + + function changePermissions( + address where, + bool withGrant, + address grantWho, + bytes4 grantWhat, + bool withRevoke, + address revokeWho, + bytes4 revokeWhat + ) external { + IAuthorizer.PermissionChange[] memory changes; + changes[0].where = where; + + if (withGrant) { + changes[0].grants[0].who = grantWho; + changes[0].grants[0].what = grantWhat; + } + + if (withRevoke) { + changes[0].revokes[0].who = revokeWho; + changes[0].revokes[0].what = revokeWhat; + } + + changePermissions(changes); + } +} diff --git a/packages/authorizer/certora/specs/Authorizer.spec b/packages/authorizer/certora/specs/Authorizer.spec index b3b4c628..ccdf197f 100644 --- a/packages/authorizer/certora/specs/Authorizer.spec +++ b/packages/authorizer/certora/specs/Authorizer.spec @@ -7,6 +7,9 @@ methods { // Helpers function helpers.authParams(address,address,bytes4) external returns (uint256[]) envfree; + // AuthorizerHarness + function changePermissions(address,bool,address,bytes4,bool,address bytes4,IAuthorizer.Param[]) external; + // Authorizer function ANYONE() external returns (address) envfree => ALWAYS(0xFFfFfFffFFfffFFfFFfFFFFFffFFFffffFfFFFfF); function ANYWHERE() external returns (address) envfree => ALWAYS(0xFFfFfFffFFfffFFfFFfFFFFFffFFFffffFfFFFfF); @@ -30,7 +33,7 @@ function buildPermissionChange( address grantWho, bytes4 grantWhat, bool withRevoke, - address revokeWho, + address revokeWho, bytes4 revokeWhat ) returns IAuthorizer.PermissionChange @@ -68,6 +71,11 @@ function requireNonGenericPermissions(address who, address where, bytes4 what) { require !hasPermission(ANYONE(), ANYWHERE(), what); } +function cleanStorage(env e, address who, address where, bytes4 what) { + require getPermissionParamsLength(who, where, what) == 1; + unauthorize(e, who, where, what); +} + // GHOSTS AND HOOKS // Params length ghost mapping(address => mapping(address => mapping(bytes4 => uint256))) ghostParamsLength { @@ -120,9 +128,11 @@ invariant checkCount(address who, address where) // INVARIANTS invariant validPermissionsState(address who, address where) forall bytes4 what . (ghostCount[who][where] == 0 => !ghostAuthorized[who][where][what]) - && (!ghostAuthorized[who][where][what] => ghostParamsLength[who][where][what] == 0) && (ghostAuthorized[who][where][what] => ghostCount[who][where] > 0); +invariant validParamsLength(address who, address where, bytes4 what) + !ghostAuthorized[who][where][what] => ghostParamsLength[who][where][what] == 0; + // RULES use rule sanity; @@ -207,6 +217,17 @@ rule authorizeWorksProperly(env e, address who, address where, bytes4 what, IAut assert !hasPermission(who, where2, what2); } +rule someoneCanPerfomTheOperation(env e, address who, address where, bytes4 what, uint256[] how, IAuthorizer.Param[] params) + good_description "If we call authorize then someone can perform the operation" +{ + require how.length == 3 && params.length <= 3; + require !hasPermission(who, where, what); + + authorize(e, who, where, what, params); + + satisfy isAuthorized(who, where, what, how); +} + rule unauthorizeWorksProperly(env e, address who, address where, bytes4 what) good_description "If a user has permissions to do `what` on `where` and we call `unauthorize`, then the user must be unauthorized" { @@ -235,8 +256,7 @@ rule grantingPermissionsIsLikeAuthorizing(env e, address who, address where, byt storage initStorage = lastStorage; - IAuthorizer.PermissionChange change = buildPermissionChange(where, true, who, what, false, 0, to_bytes4(0)); - changePermissions(e, [change]); + changePermissions(e, where, true, who, what, false, 0, to_bytes4(0)); storage afterChangePermissions = lastStorage; authorize(e, who, where, what, params) at initStorage; @@ -266,11 +286,8 @@ rule changePermissionsInBetweenShouldNotChangeStorage { require params.length == 0 && who != who2 && what != what2; - require !hasPermission(who, where, what); - require getPermissionParamsLength(who, where, what) == 0; // TODO: delete this line once the invarian works - - require !hasPermission(who2, where, what2); - require getPermissionParamsLength(who2, where, what2) == 0; // TODO: delete this line once the invarian works + cleanStorage(e, who, where, what); + cleanStorage(e, who2, where, what2); storage initStorage = lastStorage; @@ -288,8 +305,7 @@ rule changePermissionsInBetweenShouldNotChangeStorage rule changePermissionsOrderMatters(env e, address who, address where, bytes4 what) good_description "Calling changePermissions with a grant and its corresponding revoke should leave the user unauthorized" { - require !hasPermission(who, where, what); - require getPermissionParamsLength(who, where, what) == 0; // TODO: delete this line once the invarian works + cleanStorage(e, who, where, what); storage initStorage = lastStorage; @@ -302,41 +318,32 @@ rule changePermissionsOrderMatters(env e, address who, address where, bytes4 wha assert initStorage[currentContract] == currentStorage[currentContract]; } -rule hasPermissionIsEquivalentToIsAuthorizedWithEmptyParams(address who, address where, bytes4 what) +rule hasPermissionIsEquivalentToIsAuthorizedWithEmptyParams(address who, address where, bytes4 what, uint256[] how) good_description "For a permission without params, hasPermission should be equivalent to isAuthorized" { require getPermissionParamsLength(who, where, what) == 0; requireNonGenericPermissions(who, where, what); - uint256[] how = helpers.authParams(who, where, what); assert isAuthorized(who, where, what, how) == hasPermission(who, where, what); } -rule someoneCanPerfomTheOperation(env e, address who, address where, bytes4 what, uint256[] how, IAuthorizer.Param[] params) - good_description "If we call authorize then someone can perform the operation" -{ - require how.length == 3 && params.length <= 3; - require !hasPermission(who, where, what); - - authorize(e, who, where, what, params); - - satisfy isAuthorized(who, where, what, how); -} - rule anyoneIsAuthorized(env e, address who, address where, bytes4 what, IAuthorizer.Param[] params, address somewhere, bytes4 somewhat) good_description "Anyone is authorized to do `what` on `where`" { require params.length == 0; require who != ANYONE() && where != ANYWHERE() && where != somewhere && what != somewhat; - uint256[] how = []; - require !isAuthorized(who, where, what, how); - require !isAuthorized(who, somewhere, what, how); - require !isAuthorized(who, where, somewhat, how); + require !hasPermission(who, where, what); + require !hasPermission(who, somewhere, what); + require !hasPermission(who, where, somewhat); + requireNonGenericPermissions(who, where, what); + requireNonGenericPermissions(who, somewhere, what); + requireNonGenericPermissions(who, where, somewhat); authorize(e, ANYONE(), where, what, params); - assert isAuthorized(who, where, what, how); + uint256[] how = []; + assert isAuthorized(who, where, what, how) && !hasPermission(who, where, what); assert !isAuthorized(who, somewhere, what, how); assert !isAuthorized(who, where, somewhat, how); } @@ -347,14 +354,17 @@ rule isAuthorizedAnywhere(env e, address who, address where, bytes4 what, IAutho require params.length == 0; require who != ANYONE() && who != someone && where != ANYWHERE() && what != somewhat; - uint256[] how = []; - require !isAuthorized(who, where, what, how); - require !isAuthorized(someone, where, what, how); - require !isAuthorized(who, where, somewhat, how); + require !hasPermission(who, where, what); + require !hasPermission(someone, where, what); + require !hasPermission(who, where, somewhat); + requireNonGenericPermissions(who, where, what); + requireNonGenericPermissions(someone, where, what); + requireNonGenericPermissions(who, where, somewhat); authorize(e, who, ANYWHERE(), what, params); - assert isAuthorized(who, where, what, how); + uint256[] how = []; + assert isAuthorized(who, where, what, how) && !hasPermission(who, where, what); assert !isAuthorized(someone, where, what, how); assert !isAuthorized(who, where, somewhat, how); } diff --git a/packages/authorizer/contracts/Authorizer.sol b/packages/authorizer/contracts/Authorizer.sol index 0c8ef8b7..546d8a26 100644 --- a/packages/authorizer/contracts/Authorizer.sol +++ b/packages/authorizer/contracts/Authorizer.sol @@ -152,7 +152,7 @@ contract Authorizer is IAuthorizer, AuthorizedHelpers, Initializable, Reentrancy * @dev Executes a list of permission changes. Sender must be authorized. * @param changes List of permission changes to be executed */ - function changePermissions(PermissionChange[] memory changes) external override { + function changePermissions(PermissionChange[] memory changes) public override { for (uint256 i = 0; i < changes.length; i++) { PermissionChange memory change = changes[i]; for (uint256 j = 0; j < change.grants.length; j++) {