From ff6b69caed52885e51a5e0ffd08a978642028455 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 1 Aug 2025 17:33:35 +0200 Subject: [PATCH] Added mutations to config file --- certora/confs/Vault.conf | 30 +++++++++++++++++-- .../001_accumulateFlows_off_by_one.patch | 1 + .../002_flowOut_rate_calculation.patch | 1 + .../004_isSolventAt_boundary_condition.patch | 1 + .../005_flowIn_future_timestamp.patch | 1 + .../017_accountId_encoding_corruption.patch | 1 + .../Funds/003_status_boundary_condition.patch | 1 + ...duration_calculation_order_inversion.patch | 1 + .../015_transfer_authorization_bypass.patch | 1 + .../Vault/016_pause_functions_deleted.patch | 1 + .../Vault/020_withdraw_pause_bypass.patch | 1 + .../Vault/021_deposit_pause_bypass.patch | 1 + .../Vault/022_transfer_pause_bypass.patch | 1 + .../Vault/023_flow_pause_bypass.patch | 1 + .../Vault/024_lock_pause_bypass.patch | 1 + .../Vault/025_extendLock_pause_bypass.patch | 1 + .../Vault/026_designate_pause_bypass.patch | 1 + .../027_burnDesignated_pause_bypass.patch | 1 + .../Vault/028_burnAccount_pause_bypass.patch | 1 + .../Vault/029_freezeFund_pause_bypass.patch | 1 + ...ng_whenNotPaused_withdrawByRecipient.patch | 1 + .../031_pause_access_control_bypass.patch | 1 + .../032_unpause_access_control_bypass.patch | 1 + .../033_withdrawByRecipient_auth_bypass.patch | 1 + .../VaultBase/006_flow_prelock_bypass.patch | 1 + .../007_checkAccountInvariant_bypass.patch | 1 + .../008_deposit_storage_corruption.patch | 1 + .../009_transfer_balance_check_removal.patch | 1 + .../010_burnAccount_logic_inversion.patch | 1 + .../011_withdraw_reentrancy_ordering.patch | 1 + .../012_withdraw_unsafe_transfer.patch | 1 + .../013_deposit_unsafe_transferFrom.patch | 1 + .../014_all_unsafe_token_transfers.patch | 1 + .../035_withdraw_account_not_deleted.patch | 1 + .../036_burnAccount_not_deleted.patch | 1 + .../037_burnDesignated_no_decrement.patch | 1 + 36 files changed, 62 insertions(+), 3 deletions(-) create mode 120000 certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch create mode 120000 certora/mutations/Accounts/002_flowOut_rate_calculation.patch create mode 120000 certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch create mode 120000 certora/mutations/Accounts/005_flowIn_future_timestamp.patch create mode 120000 certora/mutations/Accounts/017_accountId_encoding_corruption.patch create mode 120000 certora/mutations/Funds/003_status_boundary_condition.patch create mode 120000 certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch create mode 120000 certora/mutations/Vault/015_transfer_authorization_bypass.patch create mode 120000 certora/mutations/Vault/016_pause_functions_deleted.patch create mode 120000 certora/mutations/Vault/020_withdraw_pause_bypass.patch create mode 120000 certora/mutations/Vault/021_deposit_pause_bypass.patch create mode 120000 certora/mutations/Vault/022_transfer_pause_bypass.patch create mode 120000 certora/mutations/Vault/023_flow_pause_bypass.patch create mode 120000 certora/mutations/Vault/024_lock_pause_bypass.patch create mode 120000 certora/mutations/Vault/025_extendLock_pause_bypass.patch create mode 120000 certora/mutations/Vault/026_designate_pause_bypass.patch create mode 120000 certora/mutations/Vault/027_burnDesignated_pause_bypass.patch create mode 120000 certora/mutations/Vault/028_burnAccount_pause_bypass.patch create mode 120000 certora/mutations/Vault/029_freezeFund_pause_bypass.patch create mode 120000 certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch create mode 120000 certora/mutations/Vault/031_pause_access_control_bypass.patch create mode 120000 certora/mutations/Vault/032_unpause_access_control_bypass.patch create mode 120000 certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch create mode 120000 certora/mutations/VaultBase/006_flow_prelock_bypass.patch create mode 120000 certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch create mode 120000 certora/mutations/VaultBase/008_deposit_storage_corruption.patch create mode 120000 certora/mutations/VaultBase/009_transfer_balance_check_removal.patch create mode 120000 certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch create mode 120000 certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch create mode 120000 certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch create mode 120000 certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch create mode 120000 certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch create mode 120000 certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch create mode 120000 certora/mutations/VaultBase/036_burnAccount_not_deleted.patch create mode 120000 certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch diff --git a/certora/confs/Vault.conf b/certora/confs/Vault.conf index 4cb4bcb..d86f19f 100644 --- a/certora/confs/Vault.conf +++ b/certora/confs/Vault.conf @@ -8,14 +8,38 @@ "VaultHarness:_token=ERC20A", ], "packages": [ - "@openzeppelin/=node_modules/@openzeppelin", + "@openzeppelin/=node_modules/@openzeppelin/", ], - "msg": "Verifying Vault", + //"msg": "Verifying Vault", "multi_assert_check": true, "rule_sanity": "basic", "verify": "VaultHarness:certora/specs/Vault.spec", "loop_iter": "3", "build_cache": true, "solc": "solc8.28", - "prover_version": "master" // remove with next Certora release + "prover_version": "master", // remove with next Certora release + "mutations": { + "manual_mutants": [ + { + "file_to_mutate": "contracts/Vault.sol", + "mutants_location": "certora/mutations/Vault" + }, + { + "file_to_mutate": "contracts/Timestamps.sol", + "mutants_location": "certora/mutations/Timestamps" + }, + { + "file_to_mutate": "contracts/vault/Accounts.sol", + "mutants_location": "certora/mutations/Accounts" + }, + { + "file_to_mutate": "contracts/vault/Funds.sol", + "mutants_location": "certora/mutations/Funds" + }, + { + "file_to_mutate": "contracts/vault/VaultBase.sol", + "mutants_location": "certora/mutations/VaultBase" + } + ] + } } diff --git a/certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch b/certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch new file mode 120000 index 0000000..54ca445 --- /dev/null +++ b/certora/mutations/Accounts/001_accumulateFlows_off_by_one.patch @@ -0,0 +1 @@ +../001_accumulateFlows_off_by_one.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/002_flowOut_rate_calculation.patch b/certora/mutations/Accounts/002_flowOut_rate_calculation.patch new file mode 120000 index 0000000..544c078 --- /dev/null +++ b/certora/mutations/Accounts/002_flowOut_rate_calculation.patch @@ -0,0 +1 @@ +../002_flowOut_rate_calculation.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch b/certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch new file mode 120000 index 0000000..c15bd62 --- /dev/null +++ b/certora/mutations/Accounts/004_isSolventAt_boundary_condition.patch @@ -0,0 +1 @@ +../004_isSolventAt_boundary_condition.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/005_flowIn_future_timestamp.patch b/certora/mutations/Accounts/005_flowIn_future_timestamp.patch new file mode 120000 index 0000000..faa53e1 --- /dev/null +++ b/certora/mutations/Accounts/005_flowIn_future_timestamp.patch @@ -0,0 +1 @@ +../005_flowIn_future_timestamp.patch \ No newline at end of file diff --git a/certora/mutations/Accounts/017_accountId_encoding_corruption.patch b/certora/mutations/Accounts/017_accountId_encoding_corruption.patch new file mode 120000 index 0000000..cbc374d --- /dev/null +++ b/certora/mutations/Accounts/017_accountId_encoding_corruption.patch @@ -0,0 +1 @@ +../017_accountId_encoding_corruption.patch \ No newline at end of file diff --git a/certora/mutations/Funds/003_status_boundary_condition.patch b/certora/mutations/Funds/003_status_boundary_condition.patch new file mode 120000 index 0000000..9c4390e --- /dev/null +++ b/certora/mutations/Funds/003_status_boundary_condition.patch @@ -0,0 +1 @@ +../003_status_boundary_condition.patch \ No newline at end of file diff --git a/certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch b/certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch new file mode 120000 index 0000000..14cc89a --- /dev/null +++ b/certora/mutations/Timestamps/018_duration_calculation_order_inversion.patch @@ -0,0 +1 @@ +../018_duration_calculation_order_inversion.patch \ No newline at end of file diff --git a/certora/mutations/Vault/015_transfer_authorization_bypass.patch b/certora/mutations/Vault/015_transfer_authorization_bypass.patch new file mode 120000 index 0000000..1d43500 --- /dev/null +++ b/certora/mutations/Vault/015_transfer_authorization_bypass.patch @@ -0,0 +1 @@ +../015_transfer_authorization_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/016_pause_functions_deleted.patch b/certora/mutations/Vault/016_pause_functions_deleted.patch new file mode 120000 index 0000000..9ec9fc7 --- /dev/null +++ b/certora/mutations/Vault/016_pause_functions_deleted.patch @@ -0,0 +1 @@ +../016_pause_functions_deleted.patch \ No newline at end of file diff --git a/certora/mutations/Vault/020_withdraw_pause_bypass.patch b/certora/mutations/Vault/020_withdraw_pause_bypass.patch new file mode 120000 index 0000000..8fd710f --- /dev/null +++ b/certora/mutations/Vault/020_withdraw_pause_bypass.patch @@ -0,0 +1 @@ +../020_withdraw_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/021_deposit_pause_bypass.patch b/certora/mutations/Vault/021_deposit_pause_bypass.patch new file mode 120000 index 0000000..e843aed --- /dev/null +++ b/certora/mutations/Vault/021_deposit_pause_bypass.patch @@ -0,0 +1 @@ +../021_deposit_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/022_transfer_pause_bypass.patch b/certora/mutations/Vault/022_transfer_pause_bypass.patch new file mode 120000 index 0000000..be96903 --- /dev/null +++ b/certora/mutations/Vault/022_transfer_pause_bypass.patch @@ -0,0 +1 @@ +../022_transfer_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/023_flow_pause_bypass.patch b/certora/mutations/Vault/023_flow_pause_bypass.patch new file mode 120000 index 0000000..666ad2b --- /dev/null +++ b/certora/mutations/Vault/023_flow_pause_bypass.patch @@ -0,0 +1 @@ +../023_flow_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/024_lock_pause_bypass.patch b/certora/mutations/Vault/024_lock_pause_bypass.patch new file mode 120000 index 0000000..ce642ba --- /dev/null +++ b/certora/mutations/Vault/024_lock_pause_bypass.patch @@ -0,0 +1 @@ +../024_lock_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/025_extendLock_pause_bypass.patch b/certora/mutations/Vault/025_extendLock_pause_bypass.patch new file mode 120000 index 0000000..855a17a --- /dev/null +++ b/certora/mutations/Vault/025_extendLock_pause_bypass.patch @@ -0,0 +1 @@ +../025_extendLock_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/026_designate_pause_bypass.patch b/certora/mutations/Vault/026_designate_pause_bypass.patch new file mode 120000 index 0000000..9691134 --- /dev/null +++ b/certora/mutations/Vault/026_designate_pause_bypass.patch @@ -0,0 +1 @@ +../026_designate_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/027_burnDesignated_pause_bypass.patch b/certora/mutations/Vault/027_burnDesignated_pause_bypass.patch new file mode 120000 index 0000000..d7c9a37 --- /dev/null +++ b/certora/mutations/Vault/027_burnDesignated_pause_bypass.patch @@ -0,0 +1 @@ +../027_burnDesignated_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/028_burnAccount_pause_bypass.patch b/certora/mutations/Vault/028_burnAccount_pause_bypass.patch new file mode 120000 index 0000000..a84b025 --- /dev/null +++ b/certora/mutations/Vault/028_burnAccount_pause_bypass.patch @@ -0,0 +1 @@ +../028_burnAccount_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/029_freezeFund_pause_bypass.patch b/certora/mutations/Vault/029_freezeFund_pause_bypass.patch new file mode 120000 index 0000000..93d2574 --- /dev/null +++ b/certora/mutations/Vault/029_freezeFund_pause_bypass.patch @@ -0,0 +1 @@ +../029_freezeFund_pause_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch b/certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch new file mode 120000 index 0000000..f962414 --- /dev/null +++ b/certora/mutations/Vault/030_add_missing_whenNotPaused_withdrawByRecipient.patch @@ -0,0 +1 @@ +../030_add_missing_whenNotPaused_withdrawByRecipient.patch \ No newline at end of file diff --git a/certora/mutations/Vault/031_pause_access_control_bypass.patch b/certora/mutations/Vault/031_pause_access_control_bypass.patch new file mode 120000 index 0000000..7e2845e --- /dev/null +++ b/certora/mutations/Vault/031_pause_access_control_bypass.patch @@ -0,0 +1 @@ +../031_pause_access_control_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/032_unpause_access_control_bypass.patch b/certora/mutations/Vault/032_unpause_access_control_bypass.patch new file mode 120000 index 0000000..cd222ed --- /dev/null +++ b/certora/mutations/Vault/032_unpause_access_control_bypass.patch @@ -0,0 +1 @@ +../032_unpause_access_control_bypass.patch \ No newline at end of file diff --git a/certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch b/certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch new file mode 120000 index 0000000..b836cc1 --- /dev/null +++ b/certora/mutations/Vault/033_withdrawByRecipient_auth_bypass.patch @@ -0,0 +1 @@ +../033_withdrawByRecipient_auth_bypass.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/006_flow_prelock_bypass.patch b/certora/mutations/VaultBase/006_flow_prelock_bypass.patch new file mode 120000 index 0000000..cbad95a --- /dev/null +++ b/certora/mutations/VaultBase/006_flow_prelock_bypass.patch @@ -0,0 +1 @@ +../006_flow_prelock_bypass.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch b/certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch new file mode 120000 index 0000000..ba56833 --- /dev/null +++ b/certora/mutations/VaultBase/007_checkAccountInvariant_bypass.patch @@ -0,0 +1 @@ +../007_checkAccountInvariant_bypass.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/008_deposit_storage_corruption.patch b/certora/mutations/VaultBase/008_deposit_storage_corruption.patch new file mode 120000 index 0000000..7bf533d --- /dev/null +++ b/certora/mutations/VaultBase/008_deposit_storage_corruption.patch @@ -0,0 +1 @@ +../008_deposit_storage_corruption.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/009_transfer_balance_check_removal.patch b/certora/mutations/VaultBase/009_transfer_balance_check_removal.patch new file mode 120000 index 0000000..72391f7 --- /dev/null +++ b/certora/mutations/VaultBase/009_transfer_balance_check_removal.patch @@ -0,0 +1 @@ +../009_transfer_balance_check_removal.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch b/certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch new file mode 120000 index 0000000..3d1dc34 --- /dev/null +++ b/certora/mutations/VaultBase/010_burnAccount_logic_inversion.patch @@ -0,0 +1 @@ +../010_burnAccount_logic_inversion.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch b/certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch new file mode 120000 index 0000000..585f2bf --- /dev/null +++ b/certora/mutations/VaultBase/011_withdraw_reentrancy_ordering.patch @@ -0,0 +1 @@ +../011_withdraw_reentrancy_ordering.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch b/certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch new file mode 120000 index 0000000..3a51b46 --- /dev/null +++ b/certora/mutations/VaultBase/012_withdraw_unsafe_transfer.patch @@ -0,0 +1 @@ +../012_withdraw_unsafe_transfer.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch b/certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch new file mode 120000 index 0000000..4ecfe39 --- /dev/null +++ b/certora/mutations/VaultBase/013_deposit_unsafe_transferFrom.patch @@ -0,0 +1 @@ +../013_deposit_unsafe_transferFrom.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch b/certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch new file mode 120000 index 0000000..faccde9 --- /dev/null +++ b/certora/mutations/VaultBase/014_all_unsafe_token_transfers.patch @@ -0,0 +1 @@ +../014_all_unsafe_token_transfers.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch b/certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch new file mode 120000 index 0000000..ece025c --- /dev/null +++ b/certora/mutations/VaultBase/035_withdraw_account_not_deleted.patch @@ -0,0 +1 @@ +../035_withdraw_account_not_deleted.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/036_burnAccount_not_deleted.patch b/certora/mutations/VaultBase/036_burnAccount_not_deleted.patch new file mode 120000 index 0000000..84f4792 --- /dev/null +++ b/certora/mutations/VaultBase/036_burnAccount_not_deleted.patch @@ -0,0 +1 @@ +../036_burnAccount_not_deleted.patch \ No newline at end of file diff --git a/certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch b/certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch new file mode 120000 index 0000000..8fba259 --- /dev/null +++ b/certora/mutations/VaultBase/037_burnDesignated_no_decrement.patch @@ -0,0 +1 @@ +../037_burnDesignated_no_decrement.patch \ No newline at end of file