From 792d76bd111ccd2b241aa960bf86b693adf0c9bf Mon Sep 17 00:00:00 2001 From: lgalende Date: Wed, 20 Sep 2023 18:29:11 -0300 Subject: [PATCH] authorizer: add changes from review --- .../authorizer/certora/specs/Authorizer.spec | 170 ++++++++---------- .../authorizer/certora/specs/General.spec | 4 +- packages/authorizer/contracts/Authorizer.sol | 21 +-- .../contracts/interfaces/IAuthorizer.sol | 11 +- 4 files changed, 91 insertions(+), 115 deletions(-) diff --git a/packages/authorizer/certora/specs/Authorizer.spec b/packages/authorizer/certora/specs/Authorizer.spec index 1e07a241..b3b4c628 100644 --- a/packages/authorizer/certora/specs/Authorizer.spec +++ b/packages/authorizer/certora/specs/Authorizer.spec @@ -2,6 +2,7 @@ import "./General.spec"; using Helpers as helpers; +// METHODS methods { // Helpers function helpers.authParams(address,address,bytes4) external returns (uint256[]) envfree; @@ -10,29 +11,19 @@ methods { function ANYONE() external returns (address) envfree => ALWAYS(0xFFfFfFffFFfffFFfFFfFFFFFffFFFffffFfFFFfF); function ANYWHERE() external returns (address) envfree => ALWAYS(0xFFfFfFffFFfffFFfFFfFFFFFffFFFffffFfFFFfF); function hasPermissions(address,address) external returns (bool) envfree; + function hasPermission(address,address,bytes4) external returns (bool) envfree; function isAuthorized(address,address,bytes4,uint256[]) external returns (bool) envfree; - function hasPermission(address who, address where, bytes4 what) external returns (bool) envfree; function getPermissionParams(address,address,bytes4) external returns (IAuthorizer.Param[]) envfree; function getPermissionsLength(address,address) external returns (uint256) envfree; } -definition INITIALIZE() returns uint8 = 0; -definition AUTHORIZE() returns uint8 = 1; -definition UNAUTHORIZE() returns uint8 = 2; -definition CHANGE_PERMISSIONS() returns uint8 = 3; - -definition getSelector(uint8 f) returns uint32 = ( - f == INITIALIZE() ? - sig:initialize(address[]).selector : ( - f == AUTHORIZE() ? - sig:authorize(address, address, bytes4, IAuthorizer.Param[]).selector : ( - f == UNAUTHORIZE() ? - sig:unauthorize(address, address, bytes4).selector : ( - f == CHANGE_PERMISSIONS() ? - sig:changePermissions(IAuthorizer.PermissionChange[]).selector : 0 - ))) -); +// DEFINITIONS +definition INITIALIZE() returns uint32 = sig:initialize(address[]).selector; +definition AUTHORIZE() returns uint32 = sig:authorize(address, address, bytes4, IAuthorizer.Param[]).selector; +definition UNAUTHORIZE() returns uint32 = sig:unauthorize(address, address, bytes4).selector; +definition CHANGE_PERMISSIONS() returns uint32 = sig:changePermissions(IAuthorizer.PermissionChange[]).selector; +// FUNCTIONS function buildPermissionChange( address where, bool withGrant, @@ -41,7 +32,8 @@ function buildPermissionChange( bool withRevoke, address revokeWho, bytes4 revokeWhat - ) returns IAuthorizer.PermissionChange +) + returns IAuthorizer.PermissionChange { IAuthorizer.PermissionChange change; require change.where == where; @@ -70,78 +62,83 @@ function getPermissionParamsLength(address who, address where, bytes4 what) retu return permissionParams.length; } -function requireNonGenericPermissions(address who, address where, bytes4 what, uint256[] how) { - require !isAuthorized(ANYONE(), where, what, how); - require !isAuthorized(who, ANYWHERE(), what, how); +function requireNonGenericPermissions(address who, address where, bytes4 what) { + require !hasPermission(ANYONE(), where, what); + require !hasPermission(who, ANYWHERE(), what); + require !hasPermission(ANYONE(), ANYWHERE(), what); } +// GHOSTS AND HOOKS +// Params length ghost mapping(address => mapping(address => mapping(bytes4 => uint256))) ghostParamsLength { init_state axiom forall address who . forall address where . forall bytes4 what . ghostParamsLength[who][where][what] == 0; } -ghost mapping(address => mapping(address => mapping(bytes4 => bool))) ghostAuthorized { - init_state axiom forall address who . forall address where . forall bytes4 what . !ghostAuthorized[who][where][what]; +hook Sload uint256 length currentContract._permissionsLists[KEY address who][KEY address where].(offset 32)[KEY bytes4 what].(offset 32) STORAGE { + require ghostParamsLength[who][where][what] == length; } -ghost mapping(address => mapping(address => uint256)) ghostCount { - init_state axiom forall address who . forall address where . ghostCount[who][where] == 0; +hook Sstore currentContract._permissionsLists[KEY address who][KEY address where].(offset 32)[KEY bytes4 what].(offset 32) uint256 newLength STORAGE { + ghostParamsLength[who][where][what] = newLength; } -hook Sload uint256 length currentContract._permissionsLists[KEY address who][KEY address where].(offset 32)[KEY bytes4 what].(offset 32) STORAGE { - require ghostParamsLength[who][where][what] == length; +invariant checkLength(address who, address where, bytes4 what) + ghostParamsLength[who][where][what] == getPermissionParamsLength(who, where, what); + +// Authorized +ghost mapping(address => mapping(address => mapping(bytes4 => bool))) ghostAuthorized { + init_state axiom forall address who . forall address where . forall bytes4 what . ghostAuthorized[who][where][what] == false; } hook Sload bool authorized currentContract._permissionsLists[KEY address who][KEY address where].permissions[KEY bytes4 what].authorized STORAGE { require ghostAuthorized[who][where][what] == authorized; } -hook Sload uint256 count currentContract._permissionsLists[KEY address who][KEY address where].count STORAGE { - require ghostCount[who][where] == count; +hook Sstore currentContract._permissionsLists[KEY address who][KEY address where].permissions[KEY bytes4 what].authorized bool newAuthorized STORAGE { + ghostAuthorized[who][where][what] = newAuthorized; } -hook Sstore currentContract._permissionsLists[KEY address who][KEY address where].(offset 32)[KEY bytes4 what].(offset 32) uint256 newLength STORAGE { - ghostParamsLength[who][where][what] = newLength; +invariant checkAuthorized(address who, address where, bytes4 what) + ghostAuthorized[who][where][what] == hasPermission(who, where, what); + +// Count +ghost mapping(address => mapping(address => uint256)) ghostCount { + init_state axiom forall address who . forall address where . ghostCount[who][where] == 0; } -hook Sstore currentContract._permissionsLists[KEY address who][KEY address where].permissions[KEY bytes4 what].authorized bool newAuthorized STORAGE { - ghostAuthorized[who][where][what] = newAuthorized; +hook Sload uint256 count currentContract._permissionsLists[KEY address who][KEY address where].count STORAGE { + require ghostCount[who][where] == count; } hook Sstore currentContract._permissionsLists[KEY address who][KEY address where].count uint256 newCount STORAGE { ghostCount[who][where] = newCount; } -invariant checkLength(address who, address where, bytes4 what) - ghostParamsLength[who][where][what] == getPermissionParamsLength(who, where, what); - -invariant checkAuthorized(address who, address where, bytes4 what) - ghostAuthorized[who][where][what] == hasPermission(who, where, what); - invariant checkCount(address who, address where) ghostCount[who][where] == getPermissionsLength(who, 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); -// TODO: (exists bytes4 what . ghostCount[who][where] > 0 => ghostAuthorized[who][where][what]) - +// RULES use rule sanity; use rule reentrancyGuard filtered { f -> !f.isView - && f.selector != getSelector(CHANGE_PERMISSIONS()) - && f.selector != getSelector(INITIALIZE()) + && f.selector != CHANGE_PERMISSIONS() + && f.selector != INITIALIZE() } rule senderMustBeAuthorizedToAuthorizeOthers(env e, address who, address where, bytes4 what, IAuthorizer.Param[] params) good_description "Only authorized users can authorize other users" { - bytes4 sigAuthorize = to_bytes4(getSelector(AUTHORIZE())); + bytes4 authorizeSig = to_bytes4(AUTHORIZE()); uint256[] how = helpers.authParams(who, where, what); - bool senderCanAuthorize = isAuthorized(e.msg.sender, currentContract, sigAuthorize, how); + bool senderCanAuthorize = isAuthorized(e.msg.sender, currentContract, authorizeSig, how); authorize(e, who, where, what, params); @@ -151,9 +148,9 @@ rule senderMustBeAuthorizedToAuthorizeOthers(env e, address who, address where, rule senderMustBeAuthorizedToUnauthorizeOthers(env e, address who, address where, bytes4 what) good_description "Only authorized users can unauthorize other users" { - bytes4 sigAuthorize = to_bytes4(getSelector(UNAUTHORIZE())); + bytes4 unauthorizeSig = to_bytes4(UNAUTHORIZE()); uint256[] how = helpers.authParams(who, where, what); - bool senderCanUnauthorize = isAuthorized(e.msg.sender, currentContract, sigAuthorize, how); + bool senderCanUnauthorize = isAuthorized(e.msg.sender, currentContract, unauthorizeSig, how); unauthorize(e, who, where, what); @@ -164,9 +161,9 @@ rule otherFunctionsCannotAuthorize(env e, method f, calldataarg args, address wh filtered { f -> !f.isView - && f.selector != getSelector(AUTHORIZE()) - && f.selector != getSelector(CHANGE_PERMISSIONS()) - && f.selector != getSelector(INITIALIZE()) + && f.selector != AUTHORIZE() + && f.selector != CHANGE_PERMISSIONS() + && f.selector != INITIALIZE() } good_description "Permissions can only be granted by authorize or changePermissions functions" { @@ -176,7 +173,6 @@ rule otherFunctionsCannotAuthorize(env e, method f, calldataarg args, address wh f(e, args); bool authorizedAfter = isAuthorized(who, where, what, how); - assert !authorizedBefore => !authorizedAfter; } @@ -184,11 +180,9 @@ rule unauthorizeAfterAuthorizeShouldNotChangeStorage (env e, address who, address where, bytes4 what, IAuthorizer.Param[] params) good_description "Doing authorize and then unauthorize shouldn't change the storage" { - require params.length == 0 && ghostReentrancyStatus == 1; - - uint256[] how = helpers.authParams(who, where, what); - require !isAuthorized(who, where, what, how); - require getPermissionParamsLength(who, where, what) == 0; // TODO: write an invariant for this + require params.length == 0; + require !hasPermission(who, where, what); + require getPermissionParamsLength(who, where, what) == 0; // TODO: delete this line once the invarian works storage initStorage = lastStorage; @@ -196,7 +190,6 @@ rule unauthorizeAfterAuthorizeShouldNotChangeStorage unauthorize(e, who, where, what); storage currentStorage = lastStorage; - assert initStorage[currentContract] == currentStorage[currentContract]; } @@ -205,51 +198,40 @@ rule authorizeWorksProperly(env e, address who, address where, bytes4 what, IAut { require params.length == 0 && where != where2 && what != what2; - uint256[] how = helpers.authParams(who, where, what); - require !isAuthorized(who, where, what, how); - - uint256[] how2 = helpers.authParams(who, where2, what2); - require !isAuthorized(who, where2, what2, how2); + require !hasPermission(who, where, what); + require !hasPermission(who, where2, what2); authorize(e, who, where, what, params); - assert isAuthorized(who, where, what, how); - assert !isAuthorized(who, where2, what2, how2); + assert hasPermission(who, where, what); + assert !hasPermission(who, where2, what2); } -rule unauthorizeWorksProperly(env e, address who, address where, bytes4 what, uint256[] anyhow) - good_description "If a user has permissions to do `what` on `where` with `params`, if we call unauthorize, then isAuthorized must return false for any `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" { - requireNonGenericPermissions(who, where, what, anyhow); - - // TODO: "whith params"? - uint256[] how = helpers.authParams(who, where, what); - require isAuthorized(who, where, what, how); + require hasPermission(who, where, what); unauthorize(e, who, where, what); - assert !isAuthorized(who, where, what, anyhow); + assert !hasPermission(who, where, what); } -rule unauthorizedUserCannotDoAnything(address who, address where, bytes4 what, uint256[] anyhow) +rule unauthorizedUserCannotDoAnything(address who, address where, bytes4 what, uint256[] how) good_description "If a user does not have permissions to do `what` on `where`, then isAuthorized must return false for any `how`" { - requireNonGenericPermissions(who, where, what, anyhow); + requireNonGenericPermissions(who, where, what); require !hasPermission(who, where, what); - assert !isAuthorized(who, where, what, anyhow); + assert !isAuthorized(who, where, what, how); } -rule grantingPermissionsIsLikeAuthorizing - (env e, address who, address where, bytes4 what, IAuthorizer.Param[] params) +rule grantingPermissionsIsLikeAuthorizing(env e, address who, address where, bytes4 what, IAuthorizer.Param[] params) good_description "Calling changePermissions with 1 grant should be equivalent to calling authorize" { - require params.length == 0 && ghostReentrancyStatus == 1; - - // uint256[] how = helpers.authParams(who, where, what); - // require !isAuthorized(who, where, what, how); + require params.length == 0; require !hasPermission(who, where, what); - require getPermissionParamsLength(who, where, what) == 0; // TODO: write an invariant for this + require getPermissionParamsLength(who, where, what) == 0; // TODO: delete this line once the invarian works storage initStorage = lastStorage; @@ -266,8 +248,6 @@ rule grantingPermissionsIsLikeAuthorizing rule revokingPermissionsIsLikeUnauthorizing(env e, address who, address where, bytes4 what) good_description "Calling changePermissions with 1 revoke should be equivalent to calling unauthorize" { - require ghostReentrancyStatus == 1; - storage initStorage = lastStorage; IAuthorizer.PermissionChange change = buildPermissionChange(where, false, 0, to_bytes4(0), true, who, what); @@ -286,13 +266,11 @@ rule changePermissionsInBetweenShouldNotChangeStorage { require params.length == 0 && who != who2 && what != what2; - // uint256[] how = helpers.authParams(who, where, what); - // require !isAuthorized(who, where, what, how); require !hasPermission(who, where, what); - require getPermissionParamsLength(who, where, what) == 0; // TODO: write an invariant for this + 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: write an invariant for this + require getPermissionParamsLength(who2, where, what2) == 0; // TODO: delete this line once the invarian works storage initStorage = lastStorage; @@ -310,10 +288,8 @@ 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" { - // uint256[] how = helpers.authParams(who, where, what); - // require !isAuthorized(who, where, what, how); require !hasPermission(who, where, what); - require getPermissionParamsLength(who, where, what) == 0; // TODO: write an invariant for this + require getPermissionParamsLength(who, where, what) == 0; // TODO: delete this line once the invarian works storage initStorage = lastStorage; @@ -322,27 +298,25 @@ rule changePermissionsOrderMatters(env e, address who, address where, bytes4 wha storage currentStorage = lastStorage; - assert !hasPermission(who, where, what); // TODO: or !isAuthorized? + assert !hasPermission(who, where, what); assert initStorage[currentContract] == currentStorage[currentContract]; } -rule hasPermissionIsEquivalentToIsAuthorizedWithEmptyParams - (address who, address where, bytes4 what) +rule hasPermissionIsEquivalentToIsAuthorizedWithEmptyParams(address who, address where, bytes4 what) 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); - requireNonGenericPermissions(who, where, what, how); - 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 !isAuthorized(who, where, what, how); + require how.length == 3 && params.length <= 3; + require !hasPermission(who, where, what); authorize(e, who, where, what, params); diff --git a/packages/authorizer/certora/specs/General.spec b/packages/authorizer/certora/specs/General.spec index a69a6b46..aad60904 100644 --- a/packages/authorizer/certora/specs/General.spec +++ b/packages/authorizer/certora/specs/General.spec @@ -21,8 +21,8 @@ hook Sstore currentContract._status uint256 newStatus STORAGE { ghostReentrancyChangedTimes = ghostReentrancyChangedTimes + 1; } -rule - reentrancyGuard(env e, method f, calldataarg args) filtered { f -> !f.isView } +rule reentrancyGuard(env e, method f, calldataarg args) + filtered { f -> !f.isView } good_description "Ensure external methods cannot be reentered" { require ghostReentrancyChangedTimes == 0; diff --git a/packages/authorizer/contracts/Authorizer.sol b/packages/authorizer/contracts/Authorizer.sol index 9edb47ba..0c8ef8b7 100644 --- a/packages/authorizer/contracts/Authorizer.sol +++ b/packages/authorizer/contracts/Authorizer.sol @@ -102,6 +102,17 @@ contract Authorizer is IAuthorizer, AuthorizedHelpers, Initializable, Reentrancy return _permissionsLists[who][where].count; } + /** + * @dev Tells whether `who` has permission to call `what` on `where`. Note `how` is not evaluated here, + * which means `who` might be authorized on or not depending on the call at the moment of the execution + * @param who Address asking permission for + * @param where Target address asking permission for + * @param what Function selector asking permission for + */ + function hasPermission(address who, address where, bytes4 what) external view override returns (bool) { + return _permissionsLists[who][where].permissions[what].authorized; + } + /** * @dev Tells whether `who` is allowed to call `what` on `where` with `how` * @param who Address asking permission for @@ -122,16 +133,6 @@ contract Authorizer is IAuthorizer, AuthorizedHelpers, Initializable, Reentrancy return false; } - /** - * @dev Tells whether `who` has permission to call `what` on `where` - * @param who Address asking permission for - * @param where Target address asking permission for - * @param what Function selector asking permission for - */ - function hasPermission(address who, address where, bytes4 what) external view override returns (bool) { - return _permissionsLists[who][where].permissions[what].authorized; - } - /** * @dev Tells the params set for a given permission * @param who Address asking permission params of diff --git a/packages/authorizer/contracts/interfaces/IAuthorizer.sol b/packages/authorizer/contracts/interfaces/IAuthorizer.sol index 760259e6..ed8a518b 100644 --- a/packages/authorizer/contracts/interfaces/IAuthorizer.sol +++ b/packages/authorizer/contracts/interfaces/IAuthorizer.sol @@ -96,21 +96,22 @@ interface IAuthorizer { function getPermissionsLength(address who, address where) external view returns (uint256); /** - * @dev Tells whether `who` is allowed to call `what` on `where` with `how` + * @dev Tells whether `who` has permission to call `what` on `where`. Note `how` is not evaluated here, + * which means `who` might be authorized on or not depending on the call at the moment of the execution * @param who Address asking permission for * @param where Target address asking permission for * @param what Function selector asking permission for - * @param how Params asking permission for */ - function isAuthorized(address who, address where, bytes4 what, uint256[] memory how) external view returns (bool); + function hasPermission(address who, address where, bytes4 what) external view returns (bool); /** - * @dev Tells whether `who` has permission to call `what` on `where` + * @dev Tells whether `who` is allowed to call `what` on `where` with `how` * @param who Address asking permission for * @param where Target address asking permission for * @param what Function selector asking permission for + * @param how Params asking permission for */ - function hasPermission(address who, address where, bytes4 what) external view returns (bool); + function isAuthorized(address who, address where, bytes4 what, uint256[] memory how) external view returns (bool); /** * @dev Tells the params set for a given permission