Skip to content

Commit

Permalink
authorizer: add changes from review
Browse files Browse the repository at this point in the history
  • Loading branch information
@lgalende
lgalende committed Sep 20, 2023
1 parent 8a99b67 commit 792d76b
Show file tree
Hide file tree
Showing 4 changed files with 91 additions and 115 deletions.
170 changes: 72 additions & 98 deletions packages/authorizer/certora/specs/Authorizer.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ import "./General.spec";

using Helpers as helpers;

// METHODS
methods {
// Helpers
function helpers.authParams(address,address,bytes4) external returns (uint256[]) envfree;
Expand All @@ -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,
Expand All @@ -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;
Expand Down Expand Up @@ -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);

Expand All @@ -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);

Expand All @@ -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"
{
Expand All @@ -176,27 +173,23 @@ rule otherFunctionsCannotAuthorize(env e, method f, calldataarg args, address wh
f(e, args);

bool authorizedAfter = isAuthorized(who, where, what, how);

assert !authorizedBefore => !authorizedAfter;
}

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;

authorize(e, who, where, what, params);
unauthorize(e, who, where, what);

storage currentStorage = lastStorage;

assert initStorage[currentContract] == currentStorage[currentContract];
}

Expand All @@ -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;

Expand All @@ -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);
Expand All @@ -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;

Expand All @@ -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;

Expand All @@ -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);

Expand Down
4 changes: 2 additions & 2 deletions packages/authorizer/certora/specs/General.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
Loading

0 comments on commit 792d76b

Please sign in to comment.