From 70b092ab00caa7a87d2ee5b6708d001b513042a4 Mon Sep 17 00:00:00 2001 From: r4bbit <445106+0x-r4bbit@users.noreply.github.com> Date: Wed, 13 Mar 2024 12:36:58 +0100 Subject: [PATCH] chore(StakeManagerProcessAccount.spec): add specs for processAccount This primarily adds a rule that ensures that, when an account's `balance` changes, `_processAccount()` must have been called as well. There's very few exceptions where an account's `balance` can change without the need of `_processAccount()` but those functions have been deliberately excluded from the rule. --- certora/confs/StakeManagerProcess.conf | 19 ++++ certora/specs/StakeManagerProcessAccount.spec | 86 +++++++++++++++++++ package.json | 3 +- 3 files changed, 107 insertions(+), 1 deletion(-) create mode 100644 certora/confs/StakeManagerProcess.conf create mode 100644 certora/specs/StakeManagerProcessAccount.spec diff --git a/certora/confs/StakeManagerProcess.conf b/certora/confs/StakeManagerProcess.conf new file mode 100644 index 0000000..35cede7 --- /dev/null +++ b/certora/confs/StakeManagerProcess.conf @@ -0,0 +1,19 @@ +{ + "files": + ["contracts/StakeManager.sol", + "certora/helpers/ERC20A.sol" + ], + "link" : [ + "StakeManager:stakedToken=ERC20A" + ], + "msg": "Verifying StakeManager ProcessAccount", + "rule_sanity": "basic", + "verify": "StakeManager:certora/specs/StakeManagerProcessAccount.spec", + "optimistic_loop": true, + "loop_iter": "3", + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts" + ] +} + + diff --git a/certora/specs/StakeManagerProcessAccount.spec b/certora/specs/StakeManagerProcessAccount.spec new file mode 100644 index 0000000..ea129fd --- /dev/null +++ b/certora/specs/StakeManagerProcessAccount.spec @@ -0,0 +1,86 @@ +using ERC20A as staked; +methods { + function staked.balanceOf(address) external returns (uint256) envfree; + function totalSupplyBalance() external returns (uint256) envfree; + function accounts(address) external returns(address, uint256, uint256, uint256, uint256, uint256, uint256) envfree; + + function _processAccount(StakeManager.Account storage account, uint256 _limitEpoch) internal with(env e) => markAccountProccessed(e.msg.sender, _limitEpoch); + function _.migrationInitialize(uint256,uint256,uint256,uint256) external => NONDET; +} + +// keeps track of the last epoch an account was processed +ghost mapping (address => mathint) accountProcessed; +// balance changed in an epoch that was processed +ghost mapping (address => mathint) balanceChangedInEpoch; + +function markAccountProccessed(address account, uint256 _limitEpoch) { + accountProcessed[account] = to_mathint(_limitEpoch); +} + +function getAccountLockUntil(address addr) returns uint256 { + uint256 lockUntil; + _, _, _, _, _, lockUntil, _ = accounts(addr); + + return lockUntil; +} + +hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE { + balanceChangedInEpoch[addr] = accountProcessed[addr]; +} + +definition requiresPreviousManager(method f) returns bool = ( + f.selector == sig:migrationInitialize(uint256,uint256,uint256,uint256).selector || + f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector || + f.selector == sig:increaseMPFromMigration(uint256).selector + ); + +definition requiresNextManager(method f) returns bool = ( + f.selector == sig:migrateTo(bool).selector || + f.selector == sig:transferNonPending().selector + ); + +/* + If a balance of an account has changed, the account should have been processed up to the `currentEpoch`. + This is filtering out most of migration related functions, as those will be vacuous. + + Verified on two mutations: + https://prover.certora.com/output/40726/68668bbb7b6e49828da8521c3425a20b/?anonymousKey=015fce76d5d66ef40de8342b75fda4cff1dfdd57 + https://prover.certora.com/output/40726/055d52bc67154e3fbea330fd7d68d36d/?anonymousKey=73030555b4cefe429d4eed6718b9a7e5be3a22c8 +*/ +rule checkAccountProcessedBeforeStoring(method f) filtered { + f -> !requiresPreviousManager(f) && !requiresNextManager(f) +} { + address account; + + mathint lastChanged = balanceChangedInEpoch[account]; + env e; + calldataarg args; + + require currentContract.migration == 0; + + // If the account's `lockUntil` == 0, then the account will be initialized + // with the current epoch and no processing is required. + require getAccountLockUntil(account) > 0; + + f(e,args); + + assert balanceChangedInEpoch[account] != lastChanged => + balanceChangedInEpoch[account] == to_mathint(currentContract.currentEpoch); + +} + +/* +Below is a rule that finds all methods that change an account's balance. +This is just for debugging purposes and not meant to be a production rule. +Hence it is commented out. +*/ +/* +rule whoChangeERC20Balance( method f ) filtered { f -> f.contract != staked } +{ + address user; + uint256 before = staked.balanceOf(user); + calldataarg args; + env e; + f(e,args); + assert before == staked.balanceOf(user); +} */ diff --git a/package.json b/package.json index 5438b24..c16b614 100644 --- a/package.json +++ b/package.json @@ -21,7 +21,7 @@ "scripts": { "clean": "rm -rf cache out", "lint": "pnpm lint:sol && pnpm prettier:check", - "verify": "pnpm verify:stake_vault && pnpm verify:stake_manager && pnpm verify:stake_manager_start_migration", + "verify": "pnpm verify:stake_vault && pnpm verify:stake_manager && pnpm verify:stake_manager_start_migration && pnpm verify:stake_manager_process", "lint:sol": "forge fmt --check && pnpm solhint {script,src,test,certora}/**/*.sol", "prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore", "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore", @@ -29,6 +29,7 @@ "verify:stake_vault": "certoraRun certora/confs/StakeVault.conf", "verify:stake_manager": "certoraRun certora/confs/StakeManager.conf", "verify:stake_manager_start_migration": "certoraRun certora/confs/StakeManagerStartMigration.conf", + "verify:stake_manager_process": "certoraRun certora/confs/StakeManagerProcess.conf", "release": "commit-and-tag-version" } }