AtHeartEngineer/staking-reward-streamer
1
0
Fork 0
mirror of https://github.com/vacp2p/staking-reward-streamer.git synced 2026-01-08 23:08:19 -05:00
Code Issues Packages Projects Releases Wiki Activity

test(certora): ensure Karma owneable functions are callable only by the owner

Browse Source
This commit is contained in:
Andrea Franz
2025-03-06 10:16:07 +01:00
parent 7e30c0b718
commit 96865fd84e
1 changed files with 24 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

28
certora/specs/Karma.spec
View File

@@ -1,13 +1,13 @@
using Karma as karma;
methods {
function owner() external returns (address) envfree;
}
// TODO:
// totalDistributorAllocation can only increase
// totalDistributorAllocation == sum of all distributor allocations
// sum of external supply <= total supply
// addRewardDistributor only owner
// removeRewardDistributor only owner
// setReward only owner
// mint only owner
definition isERC20TransferFunction(method f) returns bool = (
f.selector == sig:karma.transfer(address, uint256).selector
@@ -15,6 +15,14 @@ definition isERC20TransferFunction(method f) returns bool = (
|| f.selector == sig:karma.approve(address, uint256).selector
);
definition isOwnableFunction(method f) returns bool = (
f.selector == sig:karma.addRewardDistributor(address).selector
|| f.selector == sig:karma.removeRewardDistributor(address).selector
|| f.selector == sig:karma.setReward(address, uint256, uint256).selector
|| f.selector == sig:karma.mint(address, uint256).selector
);
rule erc20TransferIsDisabled(method f) {
env e;
calldataarg args;
@@ -24,3 +32,15 @@ rule erc20TransferIsDisabled(method f) {
assert isERC20TransferFunction(f) => isReverted;
}
rule ownableFuncsOnlyCallableByOwner(method f) {
env e;
calldataarg args;
bool isOwner = owner() == e.msg.sender;
f@withrevert(e, args);
bool isReverted = lastReverted;
assert isOwnableFunction(f) && !isOwner => isReverted;
}