From 1842c56c9245dee2e1fee492d28adc25f5ab474a Mon Sep 17 00:00:00 2001 From: sunbreak1211 Date: Tue, 19 Nov 2024 08:28:04 -0300 Subject: [PATCH] Add some ALMProxy specs --- ALMProxy.conf | 19 +++++ ALMProxy.spec | 218 ++++++++++++++++++++++++++++++++++++++++++++++++++ Makefile | 1 + 3 files changed, 238 insertions(+) create mode 100644 ALMProxy.conf create mode 100644 ALMProxy.spec diff --git a/ALMProxy.conf b/ALMProxy.conf new file mode 100644 index 0000000..4217d70 --- /dev/null +++ b/ALMProxy.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "spark-alm-controller/src/ALMProxy.sol" + ], + "solc": "solc-0.8.21", + "solc_optimize": "200", + "packages": [ + "openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts", + "lib/openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts", + "src=spark-alm-controller/src" + ], + "verify": "ALMProxy:ALMProxy.spec", + "rule_sanity": "basic", + "multi_assert_check": true, + "parametric_contracts": ["ALMProxy"], + "smt_timeout": "7000", + "build_cache": true, + "msg": "ALMProxy" +} diff --git a/ALMProxy.spec b/ALMProxy.spec new file mode 100644 index 0000000..b451a1a --- /dev/null +++ b/ALMProxy.spec @@ -0,0 +1,218 @@ +// ALMProxy.spec + +methods { + // constants + function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree; + function CONTROLLER() external returns (bytes32) envfree; + // getters + function hasRole(bytes32,address) external returns (bool) envfree; + function getRoleAdmin(bytes32) external returns (bytes32) envfree; + // +} + +persistent ghost bool callSuccess; +persistent ghost mathint callRetLength; +hook CALL(uint256 g, address addr, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { + callSuccess = rc != 0; + callRetLength = retLength; +} + +persistent ghost bool delegateCallSuccess; +persistent ghost mathint delegateCallRetLength; +hook DELEGATECALL(uint256 g, address addr, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { + delegateCallSuccess = rc != 0; + delegateCallRetLength = retLength; +} + +// Verify no more entry points exist +rule entryPoints(method f) filtered { f -> !f.isView } { + env e; + + calldataarg args; + f(e, args); + + assert f.selector == sig:grantRole(bytes32,address).selector || + f.selector == sig:revokeRole(bytes32,address).selector || + f.selector == sig:renounceRole(bytes32,address).selector || + f.selector == sig:doCall(address,bytes).selector || + f.selector == sig:doCallWithValue(address,bytes,uint256).selector || + f.selector == sig:doDelegateCall(address,bytes).selector || + f.isFallback; +} + +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) filtered { f -> f.selector != sig:doDelegateCall(address,bytes).selector } { + env e; + + bytes32 anyBytes32; + address anyAddr; + + bool hasRoleBefore = hasRole(anyBytes32, anyAddr); + bytes32 roleAdminBefore = getRoleAdmin(anyBytes32); + + calldataarg args; + f(e, args); + + bool hasRoleAfter = hasRole(anyBytes32, anyAddr); + bytes32 roleAdminAfter = getRoleAdmin(anyBytes32); + + assert hasRoleAfter != hasRoleBefore => + f.selector == sig:grantRole(bytes32,address).selector || + f.selector == sig:revokeRole(bytes32,address).selector || + f.selector == sig:renounceRole(bytes32,address).selector, "Assert 1"; + assert roleAdminAfter == roleAdminBefore, "Assert 2"; +} + +// Verify correct storage changes for non reverting grantRole +rule grantRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + grantRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on grantRole +rule grantRole_revert(bytes32 role, address account) { + env e; + + bool hasRoleAdminSender = hasRole(getRoleAdmin(role), e.msg.sender); + + grantRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting revokeRole +rule revokeRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + revokeRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert !hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on revokeRole +rule revokeRole_revert(bytes32 role, address account) { + env e; + + bool hasRoleAdminSender = hasRole(getRoleAdmin(role), e.msg.sender); + + revokeRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting renounceRole +rule renounceRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + renounceRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert !hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on renounceRole +rule renounceRole_revert(bytes32 role, address account) { + env e; + + renounceRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = account != e.msg.sender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify revert rules on doCall +rule doCall_revert(address target, bytes data) { + env e; + + mathint targetCodeSize = nativeCodesize[target]; + bool hasRoleControllerSender = hasRole(CONTROLLER(), e.msg.sender); + + doCall@withrevert(e, target, data); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleControllerSender; + bool revert3 = !callSuccess; + bool revert4 = callSuccess && callRetLength == 0 && targetCodeSize == 0; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify revert rules on doCallWithValue +rule doCallWithValue_revert(address target, bytes data, uint256 value) { + env e; + + mathint balance = nativeBalances[currentContract] + e.msg.value; + mathint targetCodeSize = nativeCodesize[target]; + require nativeBalances[currentContract] >= 0 && targetCodeSize >= 0; + bool hasRoleControllerSender = hasRole(CONTROLLER(), e.msg.sender); + + doCallWithValue@withrevert(e, target, data, value); + + bool revert1 = !hasRoleControllerSender; + bool revert2 = value > balance; + bool revert3 = !callSuccess; + bool revert4 = callSuccess && callRetLength == 0 && targetCodeSize == 0; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify revert rules on doDelegateCall +rule doDelegateCall_revert(address target, bytes data) { + env e; + + mathint balance = nativeBalances[currentContract] + e.msg.value; + mathint targetCodeSize = nativeCodesize[target]; + bool hasRoleControllerSender = hasRole(CONTROLLER(), e.msg.sender); + + doDelegateCall@withrevert(e, target, data); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleControllerSender; + bool revert3 = !delegateCallSuccess; + bool revert4 = delegateCallSuccess && delegateCallRetLength == 0 && targetCodeSize == 0; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} diff --git a/Makefile b/Makefile index 6f14d6e..fe882c2 100644 --- a/Makefile +++ b/Makefile @@ -2,3 +2,4 @@ PATH := ~/.solc-select/artifacts/:~/.solc-select/artifacts/solc-0.8.21:$(PATH) certora-rate-limits :; PATH=${PATH} certoraRun RateLimits.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) certora-mainnet-controller :; PATH=${PATH} certoraRun MainnetController.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) certora-foreign-controller :; PATH=${PATH} certoraRun ForeignController.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-alm-proxy :; PATH=${PATH} certoraRun AlmProxy.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)