From d2ca1ae5b189ccaed3fdda574caff7436772d269 Mon Sep 17 00:00:00 2001 From: zanderbyte-certora Date: Tue, 29 Jul 2025 20:09:27 +0300 Subject: [PATCH] add more mutations --- .../002_flowOut_rate_calculation.patch | 13 ++++++ .../003_status_boundary_condition.patch | 13 ++++++ .../004_isSolventAt_boundary_condition.patch | 13 ++++++ .../005_flowIn_future_timestamp.patch | 13 ++++++ .../mutations/006_flow_prelock_bypass.patch | 13 ++++++ .../007_checkAccountInvariant_bypass.patch | 13 ++++++ .../008_deposit_storage_corruption.patch | 13 ++++++ .../009_transfer_balance_check_removal.patch | 13 ++++++ .../010_burnAccount_logic_inversion.patch | 13 ++++++ .../011_withdraw_reentrancy_ordering.patch | 17 ++++++++ .../012_withdraw_unsafe_transfer.patch | 13 ++++++ .../013_deposit_unsafe_transferFrom.patch | 13 ++++++ .../014_all_unsafe_token_transfers.patch | 40 +++++++++++++++++++ .../015_transfer_authorization_bypass.patch | 14 +++++++ .../016_pause_functions_deleted.patch | 18 +++++++++ 15 files changed, 232 insertions(+) create mode 100644 certora/mutations/002_flowOut_rate_calculation.patch create mode 100644 certora/mutations/003_status_boundary_condition.patch create mode 100644 certora/mutations/004_isSolventAt_boundary_condition.patch create mode 100644 certora/mutations/005_flowIn_future_timestamp.patch create mode 100644 certora/mutations/006_flow_prelock_bypass.patch create mode 100644 certora/mutations/007_checkAccountInvariant_bypass.patch create mode 100644 certora/mutations/008_deposit_storage_corruption.patch create mode 100644 certora/mutations/009_transfer_balance_check_removal.patch create mode 100644 certora/mutations/010_burnAccount_logic_inversion.patch create mode 100644 certora/mutations/011_withdraw_reentrancy_ordering.patch create mode 100644 certora/mutations/012_withdraw_unsafe_transfer.patch create mode 100644 certora/mutations/013_deposit_unsafe_transferFrom.patch create mode 100644 certora/mutations/014_all_unsafe_token_transfers.patch create mode 100644 certora/mutations/015_transfer_authorization_bypass.patch create mode 100644 certora/mutations/016_pause_functions_deleted.patch diff --git a/certora/mutations/002_flowOut_rate_calculation.patch b/certora/mutations/002_flowOut_rate_calculation.patch new file mode 100644 index 0000000..3bf368d --- /dev/null +++ b/certora/mutations/002_flowOut_rate_calculation.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/Accounts.sol b/contracts/vault/Accounts.sol +index 3066e7d..7ddae11 100644 +--- a/contracts/vault/Accounts.sol ++++ b/contracts/vault/Accounts.sol +@@ -102,7 +102,7 @@ library Accounts { + if (rate <= account.flow.incoming) { + account.flow.incoming = account.flow.incoming - rate; + } else { +- account.flow.outgoing = account.flow.outgoing + rate; ++ account.flow.outgoing = account.flow.outgoing + rate + TokensPerSecond.wrap(1); + account.flow.outgoing = account.flow.outgoing - account.flow.incoming; + account.flow.incoming = TokensPerSecond.wrap(0); + } diff --git a/certora/mutations/003_status_boundary_condition.patch b/certora/mutations/003_status_boundary_condition.patch new file mode 100644 index 0000000..a079092 --- /dev/null +++ b/certora/mutations/003_status_boundary_condition.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/Funds.sol b/contracts/vault/Funds.sol +index 471c2d9..1b0e7b9 100644 +--- a/contracts/vault/Funds.sol ++++ b/contracts/vault/Funds.sol +@@ -37,7 +37,7 @@ enum FundStatus { + + library Funds { + function status(Fund memory fund) internal view returns (FundStatus) { +- if (Timestamps.currentTime() < fund.lockExpiry) { ++ if (Timestamps.currentTime() <= fund.lockExpiry) { + if (fund.frozenAt != Timestamp.wrap(0)) { + return FundStatus.Frozen; + } diff --git a/certora/mutations/004_isSolventAt_boundary_condition.patch b/certora/mutations/004_isSolventAt_boundary_condition.patch new file mode 100644 index 0000000..011a7bb --- /dev/null +++ b/certora/mutations/004_isSolventAt_boundary_condition.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/Accounts.sol b/contracts/vault/Accounts.sol +index 3066e7d..c4db427 100644 +--- a/contracts/vault/Accounts.sol ++++ b/contracts/vault/Accounts.sol +@@ -69,7 +69,7 @@ library Accounts { + ) internal pure returns (bool) { + Duration duration = account.flow.updated.until(timestamp); + uint128 outgoing = account.flow.outgoing.accumulate(duration); +- return outgoing <= account.balance.available; ++ return outgoing < account.balance.available; + } + + /// Updates the available and designated balances by accumulating the diff --git a/certora/mutations/005_flowIn_future_timestamp.patch b/certora/mutations/005_flowIn_future_timestamp.patch new file mode 100644 index 0000000..457efc3 --- /dev/null +++ b/certora/mutations/005_flowIn_future_timestamp.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/Accounts.sol b/contracts/vault/Accounts.sol +index 3066e7d..1d2ff07 100644 +--- a/contracts/vault/Accounts.sol ++++ b/contracts/vault/Accounts.sol +@@ -89,7 +89,7 @@ library Accounts { + /// Starts an incoming flow of tokens at the specified rate. If there already + /// is a flow of incoming tokens, then its rate is increased accordingly. + function flowIn(Account memory account, TokensPerSecond rate) internal view { +- account.accumulateFlows(Timestamps.currentTime()); ++ account.accumulateFlows(Timestamps.currentTime().add(Duration.wrap(1))); + account.flow.incoming = account.flow.incoming + rate; + } + diff --git a/certora/mutations/006_flow_prelock_bypass.patch b/certora/mutations/006_flow_prelock_bypass.patch new file mode 100644 index 0000000..828b0c2 --- /dev/null +++ b/certora/mutations/006_flow_prelock_bypass.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol +index be21481..22deafc 100644 +--- a/contracts/vault/VaultBase.sol ++++ b/contracts/vault/VaultBase.sol +@@ -189,7 +189,7 @@ abstract contract VaultBase { + TokensPerSecond rate + ) internal { + Fund memory fund = _funds[controller][fundId]; +- require(fund.status() == FundStatus.Locked, VaultFundNotLocked()); ++ require(fund.status() == FundStatus.Locked || fund.status() == FundStatus.Inactive, VaultFundNotLocked()); + + Account memory sender = _accounts[controller][fundId][from]; + sender.flowOut(rate); diff --git a/certora/mutations/007_checkAccountInvariant_bypass.patch b/certora/mutations/007_checkAccountInvariant_bypass.patch new file mode 100644 index 0000000..968d578 --- /dev/null +++ b/certora/mutations/007_checkAccountInvariant_bypass.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol +index be21481..c90a675 100644 +--- a/contracts/vault/VaultBase.sol ++++ b/contracts/vault/VaultBase.sol +@@ -268,7 +268,7 @@ abstract contract VaultBase { + Account memory account, + Fund memory fund + ) private pure { +- require(account.isSolventAt(fund.lockMaximum), VaultInsufficientBalance()); ++ // require(account.isSolventAt(fund.lockMaximum), VaultInsufficientBalance()); + } + + error VaultInsufficientBalance(); diff --git a/certora/mutations/008_deposit_storage_corruption.patch b/certora/mutations/008_deposit_storage_corruption.patch new file mode 100644 index 0000000..072d94d --- /dev/null +++ b/certora/mutations/008_deposit_storage_corruption.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol +index be21481..9e22028 100644 +--- a/contracts/vault/VaultBase.sol ++++ b/contracts/vault/VaultBase.sol +@@ -130,7 +130,7 @@ abstract contract VaultBase { + Fund storage fund = _funds[controller][fundId]; + require(fund.status() == FundStatus.Locked, VaultFundNotLocked()); + +- Account storage account = _accounts[controller][fundId][accountId]; ++ Account memory account = _accounts[controller][fundId][accountId]; + + account.balance.available += amount; + diff --git a/certora/mutations/009_transfer_balance_check_removal.patch b/certora/mutations/009_transfer_balance_check_removal.patch new file mode 100644 index 0000000..0fbf5d1 --- /dev/null +++ b/certora/mutations/009_transfer_balance_check_removal.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol +index be21481..94fca9a 100644 +--- a/contracts/vault/VaultBase.sol ++++ b/contracts/vault/VaultBase.sol +@@ -171,7 +171,7 @@ abstract contract VaultBase { + require(fund.status() == FundStatus.Locked, VaultFundNotLocked()); + + Account memory sender = _accounts[controller][fundId][from]; +- require(amount <= sender.balance.available, VaultInsufficientBalance()); ++ // require(amount <= sender.balance.available, VaultInsufficientBalance()); + + sender.balance.available -= amount; + _checkAccountInvariant(sender, fund); diff --git a/certora/mutations/010_burnAccount_logic_inversion.patch b/certora/mutations/010_burnAccount_logic_inversion.patch new file mode 100644 index 0000000..b52e4e2 --- /dev/null +++ b/certora/mutations/010_burnAccount_logic_inversion.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol +index be21481..f22b4ed 100644 +--- a/contracts/vault/VaultBase.sol ++++ b/contracts/vault/VaultBase.sol +@@ -227,7 +227,7 @@ abstract contract VaultBase { + require(fund.status() == FundStatus.Locked, VaultFundNotLocked()); + + Account memory account = _accounts[controller][fundId][accountId]; +- require(account.flow.incoming == account.flow.outgoing, VaultFlowNotZero()); ++ require(account.flow.incoming != account.flow.outgoing, VaultFlowNotZero()); + uint128 amount = account.balance.available + account.balance.designated; + + delete _accounts[controller][fundId][accountId]; diff --git a/certora/mutations/011_withdraw_reentrancy_ordering.patch b/certora/mutations/011_withdraw_reentrancy_ordering.patch new file mode 100644 index 0000000..4b232ec --- /dev/null +++ b/certora/mutations/011_withdraw_reentrancy_ordering.patch @@ -0,0 +1,17 @@ +diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol +index be21481..ddfaad7 100644 +--- a/contracts/vault/VaultBase.sol ++++ b/contracts/vault/VaultBase.sol +@@ -254,10 +254,10 @@ abstract contract VaultBase { + account.accumulateFlows(fund.flowEnd()); + uint128 amount = account.balance.available + account.balance.designated; + +- delete _accounts[controller][fundId][accountId]; +- + (address owner, ) = Accounts.decodeId(accountId); + _token.safeTransfer(owner, amount); ++ ++ delete _accounts[controller][fundId][accountId]; + } + + function _checkLockInvariant(Fund memory fund) private pure { diff --git a/certora/mutations/012_withdraw_unsafe_transfer.patch b/certora/mutations/012_withdraw_unsafe_transfer.patch new file mode 100644 index 0000000..4d7789b --- /dev/null +++ b/certora/mutations/012_withdraw_unsafe_transfer.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol +index be21481..f3eef7d 100644 +--- a/contracts/vault/VaultBase.sol ++++ b/contracts/vault/VaultBase.sol +@@ -257,7 +257,7 @@ abstract contract VaultBase { + delete _accounts[controller][fundId][accountId]; + + (address owner, ) = Accounts.decodeId(accountId); +- _token.safeTransfer(owner, amount); ++ _token.transfer(owner, amount); + } + + function _checkLockInvariant(Fund memory fund) private pure { diff --git a/certora/mutations/013_deposit_unsafe_transferFrom.patch b/certora/mutations/013_deposit_unsafe_transferFrom.patch new file mode 100644 index 0000000..b5a67e6 --- /dev/null +++ b/certora/mutations/013_deposit_unsafe_transferFrom.patch @@ -0,0 +1,13 @@ +diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol +index be21481..30c52fd 100644 +--- a/contracts/vault/VaultBase.sol ++++ b/contracts/vault/VaultBase.sol +@@ -134,7 +134,7 @@ abstract contract VaultBase { + + account.balance.available += amount; + +- _token.safeTransferFrom( ++ _token.transferFrom( + Controller.unwrap(controller), + address(this), + amount diff --git a/certora/mutations/014_all_unsafe_token_transfers.patch b/certora/mutations/014_all_unsafe_token_transfers.patch new file mode 100644 index 0000000..b6916d7 --- /dev/null +++ b/certora/mutations/014_all_unsafe_token_transfers.patch @@ -0,0 +1,40 @@ +diff --git a/contracts/vault/VaultBase.sol b/contracts/vault/VaultBase.sol +index be21481..5efdc8e 100644 +--- a/contracts/vault/VaultBase.sol ++++ b/contracts/vault/VaultBase.sol +@@ -134,7 +134,7 @@ abstract contract VaultBase { + + account.balance.available += amount; + +- _token.safeTransferFrom( ++ _token.transferFrom( + Controller.unwrap(controller), + address(this), + amount +@@ -215,7 +215,7 @@ abstract contract VaultBase { + + account.balance.designated -= amount; + +- _token.safeTransfer(address(0xdead), amount); ++ _token.transfer(address(0xdead), amount); + } + + function _burnAccount( +@@ -232,7 +232,7 @@ abstract contract VaultBase { + + delete _accounts[controller][fundId][accountId]; + +- _token.safeTransfer(address(0xdead), amount); ++ _token.transfer(address(0xdead), amount); + } + + function _freezeFund(Controller controller, FundId fundId) internal { +@@ -257,7 +257,7 @@ abstract contract VaultBase { + delete _accounts[controller][fundId][accountId]; + + (address owner, ) = Accounts.decodeId(accountId); +- _token.safeTransfer(owner, amount); ++ _token.transfer(owner, amount); + } + + function _checkLockInvariant(Fund memory fund) private pure { diff --git a/certora/mutations/015_transfer_authorization_bypass.patch b/certora/mutations/015_transfer_authorization_bypass.patch new file mode 100644 index 0000000..1cba346 --- /dev/null +++ b/certora/mutations/015_transfer_authorization_bypass.patch @@ -0,0 +1,14 @@ +diff --git a/contracts/Vault.sol b/contracts/Vault.sol +index 8433a08..5dd18c8 100644 +--- a/contracts/Vault.sol ++++ b/contracts/Vault.sol +@@ -164,7 +164,8 @@ contract Vault is VaultBase, Pausable, Ownable { + AccountId to, + uint128 amount + ) public whenNotPaused { +- Controller controller = Controller.wrap(msg.sender); ++ (address holder, ) = Accounts.decodeId(from); ++ Controller controller = Controller.wrap(holder); + _transfer(controller, fundId, from, to, amount); + } + diff --git a/certora/mutations/016_pause_functions_deleted.patch b/certora/mutations/016_pause_functions_deleted.patch new file mode 100644 index 0000000..f61fabe --- /dev/null +++ b/certora/mutations/016_pause_functions_deleted.patch @@ -0,0 +1,18 @@ +diff --git a/contracts/Vault.sol b/contracts/Vault.sol +index 8433a08..185ed83 100644 +--- a/contracts/Vault.sol ++++ b/contracts/Vault.sol +@@ -240,13 +240,7 @@ contract Vault is VaultBase, Pausable, Ownable { + _withdraw(controller, fund, accountId); + } + +- function pause() public onlyOwner { +- _pause(); +- } + +- function unpause() public onlyOwner { +- _unpause(); +- } + + error VaultOnlyAccountHolder(); + }