diff --git a/assertions-book/previous-hacks/abracadabra-gmx-v2-exploit.mdx b/assertions-book/previous-hacks/abracadabra-gmx-v2-exploit.mdx index 584ab84..eb4bb18 100644 --- a/assertions-book/previous-hacks/abracadabra-gmx-v2-exploit.mdx +++ b/assertions-book/previous-hacks/abracadabra-gmx-v2-exploit.mdx @@ -56,8 +56,8 @@ contract AbracadabraGmxV2Assertion is Assertion { function triggers() public view override { // Trigger on any call to sendValueInCollateral - triggerRecorder.registerCallTrigger( - this.assertPhantomCollateral.selector, + registerCallTrigger( + this.assertPhantomCollateral.selector, IGmxV2CauldronRouterOrder.sendValueInCollateral.selector ); } diff --git a/assertions-book/previous-hacks/abracadabra-hack-3.mdx b/assertions-book/previous-hacks/abracadabra-hack-3.mdx index 39dff37..7d5e248 100644 --- a/assertions-book/previous-hacks/abracadabra-hack-3.mdx +++ b/assertions-book/previous-hacks/abracadabra-hack-3.mdx @@ -72,7 +72,7 @@ contract AbracadabraCookSolvencyAssertion is Assertion { uint256 constant COLLATERIZATION_RATE_PRECISION = 1e5; function triggers() public view override { - triggerRecorder.registerCallTrigger( + registerCallTrigger( this.assertUserSolvency.selector, ICauldronV4.cook.selector ); diff --git a/assertions-book/previous-hacks/abracadabra-rounding-error.mdx b/assertions-book/previous-hacks/abracadabra-rounding-error.mdx index 113ccef..0885e46 100644 --- a/assertions-book/previous-hacks/abracadabra-rounding-error.mdx +++ b/assertions-book/previous-hacks/abracadabra-rounding-error.mdx @@ -37,12 +37,36 @@ The vulnerability stems from an intricate implementation of a RebaseToken mechan ## Proposed Solution -Assuming the original implementation was well-intentioned but flawed, a simple invariant check could have prevented the attack: +Assuming the original implementation was well-intentioned but flawed, a simple invariant check could have prevented the attack. + +The key invariant is: **when no assets are owed (elastic = 0), there should be no debt shares (base = 0)**. ```solidity -function assertionNoDebtSharesIfNoDebt() public view { - if (elastic == 0) { - require(base == 0, "No debt shares if no debt"); +// SPDX-License-Identifier: MIT +pragma solidity 0.8.28; + +import {Assertion} from "credible-std/Assertion.sol"; + +interface ICauldronV4 { + function totalBorrow() external view returns (uint128 elastic, uint128 base); +} + +contract AbracadabraRebaseInvariantAssertion is Assertion { + function triggers() external view override { + // Trigger on any storage change to the cauldron + registerStorageChangeTrigger(this.assertionNoDebtSharesIfNoDebt.selector); + } + + function assertionNoDebtSharesIfNoDebt() external view { + ICauldronV4 cauldron = ICauldronV4(ph.getAssertionAdopter()); + + ph.forkPostTx(); + (uint128 elastic, uint128 base) = cauldron.totalBorrow(); + + // Core invariant: if no debt exists, no shares should exist + if (elastic == 0) { + require(base == 0, "No debt shares should exist when no debt"); + } } } ``` diff --git a/assertions-book/previous-hacks/bybit-safe-ui.mdx b/assertions-book/previous-hacks/bybit-safe-ui.mdx index f59aa1d..6496872 100644 --- a/assertions-book/previous-hacks/bybit-safe-ui.mdx +++ b/assertions-book/previous-hacks/bybit-safe-ui.mdx @@ -85,7 +85,7 @@ contract SafeAssertion is Assertion { // Define the triggers for the assertions function triggers() public view override { - triggerRecorder.registerStateChangeTrigger(this.implementationAddressChange.selector, 0x0); + registerStorageChangeTrigger(this.implementationAddressChange.selector, bytes32(0x0)); } function implementationAddressChange() external view { diff --git a/assertions-book/previous-hacks/compound-upgrade-bug.mdx b/assertions-book/previous-hacks/compound-upgrade-bug.mdx index 06cf5c1..a7f36fd 100644 --- a/assertions-book/previous-hacks/compound-upgrade-bug.mdx +++ b/assertions-book/previous-hacks/compound-upgrade-bug.mdx @@ -29,26 +29,33 @@ This way even if a bug is introduced, it will be caught by the assertion. The assertion below calculates the maximum possible rate of COMP accrual and checks that a distribution does not exceed this rate. + +The code below is **conceptual pseudo code** to illustrate the invariant that should be enforced. It uses simplified syntax for accessing storage mappings (`compound.compAccrued[supplier]`) that would not compile in actual Solidity. A real implementation would need to use proper getter functions or storage slot calculations via `ph.load()`. + + ```solidity -// Verify that COMP accrual never exceeds the maximum possible rate -function assertionValidCompAccrual() external { - PhEvm.CallInputs[] memory distributions = ph.getCallInputs(address(compound), Comptroller.distributeSupplierComp.selector); +// CONCEPTUAL - Verify that COMP accrual never exceeds the maximum possible rate +function assertionValidCompAccrual() external view { + PhEvm.CallInputs[] memory distributions = ph.getCallInputs( + address(comptroller), + Comptroller.distributeSupplierComp.selector + ); for (uint256 i = 0; i < distributions.length; i++) { - bytes memory data = distributions[i].input; - (address cToken, address supplier) = abi.decode(stripSelector(data), (address, address)); - - // Check COMP accrued before and after distribution - ph.forkPreCallState(); - uint256 preAccrued = compound.compAccrued[supplier]; - CompMarketState storage supplyState = comptroller.compSupplyState[cToken]; - uint supplyIndex = supplyState.index; - uint maxDeltaPerToken = sub_(supplyIndex, comptroller.compInitialIndex); - uint supplierTokens = CToken(cToken).balanceOf(supplier); - uint maxIncrease = mul_(supplierTokens, maxDeltaPerToken); - - ph.forkPostCallState(); - uint256 postAccrued = compound.compAccrued[supplier]; + // Decode call inputs (selector already stripped by cheatcode) + (address cToken, address supplier) = abi.decode(distributions[i].input, (address, address)); + + // Check COMP accrued before distribution + ph.forkPreCall(distributions[i].id); + uint256 preAccrued = comptroller.compAccrued(supplier); + uint256 supplyIndex = comptroller.compSupplyState(cToken).index; + uint256 maxDeltaPerToken = supplyIndex - comptroller.compInitialIndex(); + uint256 supplierTokens = CToken(cToken).balanceOf(supplier); + uint256 maxIncrease = supplierTokens * maxDeltaPerToken; + + // Check COMP accrued after distribution + ph.forkPostCall(distributions[i].id); + uint256 postAccrued = comptroller.compAccrued(supplier); if (postAccrued > preAccrued) { uint256 increase = postAccrued - preAccrued; diff --git a/assertions-book/previous-hacks/cream-finance-2.mdx b/assertions-book/previous-hacks/cream-finance-2.mdx index 7d0bb55..2b14ad7 100644 --- a/assertions-book/previous-hacks/cream-finance-2.mdx +++ b/assertions-book/previous-hacks/cream-finance-2.mdx @@ -19,51 +19,74 @@ One possible solution is to check price deviations from touched assets in the pr This would avoid flashloan price manipulation attacks. ```solidity -function assertion_priceDeviation() public view { - PhEvm.Logs[] memory logs = PhEvm.getLogs(); - bytes32[] memory topics = [ - CTokenInterface.Redeem.selector, - CTokenInterface.Borrow.selector, - CTokenInterface.RepayBorrow.selector, - CTokenInterface.LiquidateBorrow.selector - ]; +uint256 constant MAX_DEVIATION_BPS = 500; // 5% max deviation +function assertion_priceDeviation() external view { + // Get pre-transaction prices first + ph.forkPreTx(); + PhEvm.Log[] memory logs = ph.getLogs(); - address[] memory touchedAssets = new address[]; + // Count relevant logs to size our array + uint256 count = 0; for (uint256 i = 0; i < logs.length; i++) { - - if(logs[i].topics[0] == CTokenInterface.Mint.selector) { - touchedAssets.push(getAssetFromMintLog(logs[i])); - continue; - } - if(logs[i].topics[0] == CTokenInterface.Redeem.selector) { - touchedAssets.push(getAssetFromRedeemLog(logs[i])); - continue; + bytes32 topic = logs[i].topics[0]; + if (topic == CTokenInterface.Mint.selector || + topic == CTokenInterface.Redeem.selector || + topic == CTokenInterface.Borrow.selector || + topic == CTokenInterface.RepayBorrow.selector) { + count++; } - if(logs[i].topics[0] == CTokenInterface.Borrow.selector) { - touchedAssets.push(getAssetFromBorrowLog(logs[i])); - continue; - } - if(logs[i].topics[0] == CTokenInterface.RepayBorrow.selector) { - touchedAssets.push(getAssetFromRepayBorrowLog(logs[i])); + } + + // Collect touched assets and their pre-prices + address[] memory touchedAssets = new address[](count); + uint256[] memory prePrices = new uint256[](count); + uint256 idx = 0; + + for (uint256 i = 0; i < logs.length; i++) { + bytes32 topic = logs[i].topics[0]; + address asset; + + if (topic == CTokenInterface.Mint.selector) { + asset = getAssetFromLog(logs[i]); + } else if (topic == CTokenInterface.Redeem.selector) { + asset = getAssetFromLog(logs[i]); + } else if (topic == CTokenInterface.Borrow.selector) { + asset = getAssetFromLog(logs[i]); + } else if (topic == CTokenInterface.RepayBorrow.selector) { + asset = getAssetFromLog(logs[i]); + } else { continue; } + touchedAssets[idx] = asset; + prePrices[idx] = priceOracle.getPrice(asset); + idx++; } - uint256[] memory postPrices = new uint256[](touchedAssets); + // Get post-transaction prices and compare + ph.forkPostTx(); + for (uint256 i = 0; i < touchedAssets.length; i++) { - postPrices.push(priceOracle.getPrice(touchedAssets[i])); - } + uint256 postPrice = priceOracle.getPrice(touchedAssets[i]); + uint256 prePrice = prePrices[i]; - ph.forkPreTx(); + // Check deviation in both directions + uint256 deviation; + if (postPrice > prePrice) { + deviation = ((postPrice - prePrice) * 10000) / prePrice; + } else { + deviation = ((prePrice - postPrice) * 10000) / prePrice; + } - for (uint256 i = 0; i < touchedAssets.length; i++) { - uint256 prePrice = priceOracle.getPrice(touchedAssets[i]); - require( - postPrice[i] < prePrice * (1 + MAX_DEVIATION_FACTOR) && - postPrice[i] > prePrice * (1 - MAX_DEVIATION_FACTOR), - "Price deviation too high" - ); + require(deviation <= MAX_DEVIATION_BPS, "Price deviation too high"); + } +} + +// Helper to extract asset address from log (implementation depends on log structure) +function getAssetFromLog(PhEvm.Log memory log) internal pure returns (address) { + // Decode asset address from log topics or data + // Implementation depends on the specific event structure + return abi.decode(log.data, (address)); } ``` diff --git a/assertions-book/previous-hacks/euler-finance-donation-hack.mdx b/assertions-book/previous-hacks/euler-finance-donation-hack.mdx index 3e197f2..7c28a41 100644 --- a/assertions-book/previous-hacks/euler-finance-donation-hack.mdx +++ b/assertions-book/previous-hacks/euler-finance-donation-hack.mdx @@ -59,25 +59,30 @@ Attack was carried out for several different assets, including DAI, WETH, and US Proper health checks should be performed on the account that is performing the donation. It is worth noting that the below assertion checks for modifications made by the user in the transaction. The user should never be allowed to make changes to their own collateral or debt that brings their positions under water. -Assuming we can check run assertions on each call in the transaction and that we can get all modified accounts in the transaction, we can implement the following assertion: + + +The code below is **conceptual pseudo code** to illustrate the invariant that should be enforced. The `getModifiedAccounts()` cheatcode does not currently exist. In practice, you would need to identify affected accounts through other means, such as parsing logs with `getLogs()` or tracking call inputs with `getCallInputs()`. + ```solidity -function assertionNoUnsafeDebt() external { +// CONCEPTUAL - getModifiedAccounts() is not a real cheatcode +function assertionNoUnsafeDebt() external view { ph.forkPostTx(); - + // Get all accounts that were modified in this tx + // NOTE: This cheatcode does not exist - this is conceptual address[] memory accounts = ph.getModifiedAccounts(); - + for (uint256 i = 0; i < accounts.length; i++) { address account = accounts[i]; - + // Core invariant: Collateral must always be >= Debt require(euler.healthCheck(account), "Account has more debt than collateral"); } } ``` -This assertion ensures that users don't have more debt than collateral after the transaction. +The key insight is that the **invariant itself is simple**: after any transaction, no account should have more debt than collateral. The challenge is identifying which accounts to check, which in a real implementation might require parsing transaction logs or call inputs. ## Additional Considerations diff --git a/assertions-book/previous-hacks/first-depositor.mdx b/assertions-book/previous-hacks/first-depositor.mdx index 6035d0d..73c1516 100644 --- a/assertions-book/previous-hacks/first-depositor.mdx +++ b/assertions-book/previous-hacks/first-depositor.mdx @@ -61,12 +61,11 @@ function assertionHasMinimumSupply() public view { function assertionExchangeRate() public view { Market market = Market(address(0x1234)); - - PhEvm.CallInputs[] memory inputs = PhEvm.CallInputs(address(cToken),abi.encodeWithSelector(cToken.mint.selector)); + PhEvm.CallInputs[] memory inputs = ph.getCallInputs(address(cToken), cToken.mint.selector); for (uint256 i = 0; i < inputs.length; i++) { PhEvm.CallInputs memory input = inputs[i]; - (address target, uint256 amount) = abi.decode(input.data, (address, uint256)); + (uint256 amount) = abi.decode(input.input, (uint256)); require(amount / market.exchangeRate() > 0, "Did not receive any shares"); } } diff --git a/assertions-book/previous-hacks/hack1-radiant-capital.mdx b/assertions-book/previous-hacks/hack1-radiant-capital.mdx index fc9508c..cefb2a6 100644 --- a/assertions-book/previous-hacks/hack1-radiant-capital.mdx +++ b/assertions-book/previous-hacks/hack1-radiant-capital.mdx @@ -40,42 +40,37 @@ contract LendingPoolAddressesProviderAssertions is Assertion { ILendingPoolAddressesProvider(0x091d52CacE1edc5527C99cDCFA6937C1635330E4); //arbitrum function triggers() external view override { - registerCallTrigger(this.assertionOwnerChange.selector, lendingPoolAddressesProvider.owner.selector); - registerCallTrigger(this.assertionEmergencyAdminChange.selector, lendingPoolAddressesProvider.getEmergencyAdmin.selector); - registerCallTrigger(this.assertionPoolAdminChange.selector, lendingPoolAddressesProvider.getPoolAdmin.selector); + // Trigger on any storage change to catch ownership modifications + registerStorageChangeTrigger(this.assertionOwnerChange.selector); + registerStorageChangeTrigger(this.assertionEmergencyAdminChange.selector); + registerStorageChangeTrigger(this.assertionPoolAdminChange.selector); } // Check if the owner has changed - // return true indicates a valid state -> owner is the same - // return false indicates an invalid state -> owner is different - function assertionOwnerChange() external returns (bool) { + function assertionOwnerChange() external view { ph.forkPreTx(); address prevOwner = lendingPoolAddressesProvider.owner(); ph.forkPostTx(); address newOwner = lendingPoolAddressesProvider.owner(); - return prevOwner == newOwner; + require(prevOwner == newOwner, "Owner has changed"); } // Check if the emergency admin has changed - // return true indicates a valid state -> emergency admin is the same - // return false indicates an invalid state -> emergency admin is different - function assertionEmergencyAdminChange() external returns (bool) { + function assertionEmergencyAdminChange() external view { ph.forkPreTx(); address prevEmergencyAdmin = lendingPoolAddressesProvider.getEmergencyAdmin(); ph.forkPostTx(); address newEmergencyAdmin = lendingPoolAddressesProvider.getEmergencyAdmin(); - return prevEmergencyAdmin == newEmergencyAdmin; + require(prevEmergencyAdmin == newEmergencyAdmin, "Emergency admin has changed"); } // Check if the pool admin has changed - // return true indicates a valid state -> pool admin is the same - // return false indicates an invalid state -> pool admin is different - function assertionPoolAdminChange() external returns (bool) { + function assertionPoolAdminChange() external view { ph.forkPreTx(); address prevPoolAdmin = lendingPoolAddressesProvider.getPoolAdmin(); ph.forkPostTx(); address newPoolAdmin = lendingPoolAddressesProvider.getPoolAdmin(); - return prevPoolAdmin == newPoolAdmin; + require(prevPoolAdmin == newPoolAdmin, "Pool admin has changed"); } } ``` diff --git a/assertions-book/previous-hacks/hack2-vestra-dao.mdx b/assertions-book/previous-hacks/hack2-vestra-dao.mdx index 9d7dcba..c8312a6 100644 --- a/assertions-book/previous-hacks/hack2-vestra-dao.mdx +++ b/assertions-book/previous-hacks/hack2-vestra-dao.mdx @@ -54,16 +54,19 @@ contract VestraDAOHack is Assertion { registerCallTrigger(this.assertionExample.selector, vestraDAO.unStake.selector); } - // Check if the user has already unstaked for a maturity - function assertionExample() external { - ph.forkPostTx(); + // Check that user was actively staked before unstaking + // This prevents double-unstaking by ensuring isActive was true before the call + function assertionExample() external view { PhEvm.CallInputs[] memory unStakes = ph.getCallInputs(address(vestraDAO), vestraDAO.unStake.selector); for (uint256 i = 0; i < unStakes.length; i++) { - uint8 maturity = abi.decode(unStakes[i].input.maturity, (uint8)); + uint8 maturity = abi.decode(unStakes[i].input, (uint8)); address from = unStakes[i].caller; - IVestraDAO.Stake storage user = vestraDAO.stakes[from][maturity]; - require(user.isActive, "User has already unstaked for this maturity"); + + // Check BEFORE the unstake that the stake was active + ph.forkPreCall(unStakes[i].id); + (,,,,,bool wasActive) = vestraDAO.stakes(from, maturity); + require(wasActive, "User was not actively staked for this maturity"); } } } diff --git a/assertions-book/previous-hacks/prev-hacks-index.mdx b/assertions-book/previous-hacks/prev-hacks-index.mdx index 4b0e9ff..e7b9d15 100644 --- a/assertions-book/previous-hacks/prev-hacks-index.mdx +++ b/assertions-book/previous-hacks/prev-hacks-index.mdx @@ -12,18 +12,18 @@ Each analysis includes: ## Access Control & Administrative Vulnerabilities -### [Radiant Capital Hack](/assertions-book/previous-hacks/hack1-radiant-capital) -**Attack Type:** Ownership Takeover -**Loss:** $58M+ USD -**Root Cause:** Attackers gained control of multisig signers and changed ownership of lending pools -**Prevention:** Owner change assertions with proper validation and whitelisting - ### [Bybit - Compromised Safe Wallet UI](/assertions-book/previous-hacks/bybit-safe-ui) **Attack Type:** UI Compromise + Implementation Change **Loss:** $1.4B USD **Root Cause:** Compromised frontend showed fake transactions while changing proxy implementation **Prevention:** Implementation address change assertions and transaction validation +### [Radiant Capital Hack](/assertions-book/previous-hacks/hack1-radiant-capital) +**Attack Type:** Ownership Takeover +**Loss:** $58M+ USD +**Root Cause:** Attackers gained control of multisig signers and changed ownership of lending pools +**Prevention:** Owner change assertions with proper validation and whitelisting + ### [UxLink Multisig Ownership Compromise](/assertions-book/previous-hacks/uxlink-multisig-hack) **Attack Type:** Private Key Compromise + Multisig Manipulation **Loss:** $39.3M USD @@ -32,11 +32,11 @@ Each analysis includes: ## Arithmetic & Calculation Errors -### [Abracadabra Rounding Error Attack](/assertions-book/previous-hacks/abracadabra-rounding-error) -**Attack Type:** Rounding Error Exploitation -**Loss:** $6.5M USD -**Root Cause:** Rounding error in RebaseToken mechanism allowed base value inflation -**Prevention:** Invariant checks ensuring debt shares consistency +### [Balancer V2 Rate Manipulation Exploit](/assertions-book/previous-hacks/balancer-v2-stable-rate-exploit) +**Attack Type:** Rounding Error Accumulation +**Loss:** $120M+ USD +**Root Cause:** Accumulated rounding errors in stable pool invariant calculation manipulated exchange rates +**Prevention:** Rate change bounds assertions detecting drastic pool rate changes within single transactions ### [Bunni XYZ Rounding Error Exploit](/assertions-book/previous-hacks/bunni-xyz-rounding-error) **Attack Type:** Rounding Error + Liquidity Manipulation @@ -44,17 +44,11 @@ Each analysis includes: **Root Cause:** Rounding error in withdrawal mechanism led to disproportionate liquidity decreases **Prevention:** Withdrawal proportionality assertions ensuring balance decreases match share burns -### [Balancer V2 Rate Manipulation Exploit](/assertions-book/previous-hacks/balancer-v2-stable-rate-exploit) -**Attack Type:** Rounding Error Accumulation -**Loss:** $120M+ USD -**Root Cause:** Accumulated rounding errors in stable pool invariant calculation manipulated exchange rates -**Prevention:** Rate change bounds assertions detecting drastic pool rate changes within single transactions - -### [Compound Upgrade Bug](/assertions-book/previous-hacks/compound-upgrade-bug) -**Attack Type:** Logic Error in Upgrade -**Loss:** $280K USD (limited by quick response) -**Root Cause:** One-letter bug (`>` instead of `>=`) in reward calculation -**Prevention:** Maximum reward rate validation assertions +### [Abracadabra Rounding Error Attack](/assertions-book/previous-hacks/abracadabra-rounding-error) +**Attack Type:** Rounding Error Exploitation +**Loss:** $6.5M USD +**Root Cause:** Rounding error in RebaseToken mechanism allowed base value inflation +**Prevention:** Invariant checks ensuring debt shares consistency ### [Vestra DAO Hack](/assertions-book/previous-hacks/hack2-vestra-dao) **Attack Type:** Unchecked State Flag @@ -62,13 +56,19 @@ Each analysis includes: **Root Cause:** Missing validation of `isActive` flag in unstake function **Prevention:** State flag validation assertions +### [Compound Upgrade Bug](/assertions-book/previous-hacks/compound-upgrade-bug) +**Attack Type:** Logic Error in Upgrade +**Loss:** $280K USD (limited by quick response) +**Root Cause:** One-letter bug (`>` instead of `>=`) in reward calculation +**Prevention:** Maximum reward rate validation assertions + ## Oracle & Price Manipulation -### [Cream Finance 2](/assertions-book/previous-hacks/cream-finance-2) -**Attack Type:** Price Manipulation -**Loss:** $130M USD -**Root Cause:** Sudden price manipulation through asset donation to vault -**Prevention:** Price deviation monitoring assertions +### [GMX v1 AUM Manipulation Hack](/assertions-book/previous-hacks/gma-aum-jul25-hack) +**Attack Type:** Reentrancy + AUM Manipulation +**Loss:** $42M USD +**Root Cause:** Reentrancy vulnerability allowed artificial AUM inflation +**Prevention:** AUM manipulation bounds assertions and atomic state consistency ### [KiloEx Price Oracle Manipulation](/assertions-book/previous-hacks/kiloex-price-manipulation-hack) **Attack Type:** Access Control + Price Manipulation @@ -76,28 +76,46 @@ Each analysis includes: **Root Cause:** Lack of access controls in MinimalForwarder allowed price manipulation **Prevention:** Price deviation assertions and access control validation -### [GMX v1 AUM Manipulation Hack](/assertions-book/previous-hacks/gma-aum-jul25-hack) -**Attack Type:** Reentrancy + AUM Manipulation -**Loss:** $42M USD -**Root Cause:** Reentrancy vulnerability allowed artificial AUM inflation -**Prevention:** AUM manipulation bounds assertions and atomic state consistency +### [Vicuna Finance Oracle Manipulation](/assertions-book/previous-hacks/vicuna-finance-hack) +**Attack Type:** LP Token Oracle Manipulation +**Loss:** $700K USD +**Root Cause:** LP tokens priced using simple sum formula instead of fair pricing +**Prevention:** Price deviation assertions monitoring oracle changes per call + +### [Cream Finance 2](/assertions-book/previous-hacks/cream-finance-2) +**Attack Type:** Price Manipulation +**Loss:** $130M USD +**Root Cause:** Sudden price manipulation through asset donation to vault +**Prevention:** Price deviation monitoring assertions ## Protocol Logic Vulnerabilities +### [Abracadabra GMX V2 Cauldron Exploit](/assertions-book/previous-hacks/abracadabra-gmx-v2-exploit) +**Attack Type:** Accounting Bug +**Loss:** $13.4M USD +**Root Cause:** Phantom collateral created when tokens extracted without updating order value +**Prevention:** Collateral tracking assertions ensuring borrowed amounts never exceed actual collateral + +### [Abracadabra CauldronV4 Cook Function Exploit](/assertions-book/previous-hacks/abracadabra-hack-3) +**Attack Type:** Logic Flaw in Action Sequencing +**Loss:** $1.8M USD +**Root Cause:** Action sequence [5, 0] allowed solvency check flag to be set then immediately cleared +**Prevention:** Post-transaction solvency assertions enforcing outcome-based validation + ### [Euler Finance Donation Hack](/assertions-book/previous-hacks/euler-finance-donation-hack) **Attack Type:** Missing Health Check **Loss:** $197M USD **Root Cause:** Donation function lacked health factor validation **Prevention:** Health factor assertions after all state changes -### [First Depositor Bug](/assertions-book/previous-hacks/first-depositor) -**Attack Type:** Share Price Manipulation -**Loss:** Various protocols affected -**Root Cause:** First depositor can manipulate exchange rate through donation -**Prevention:** Minimum supply assertions and exchange rate validation - ### [Visor Finance Unrestricted Mint](/assertions-book/previous-hacks/visor-finance-unrestricted-mint) **Attack Type:** Unrestricted Token Minting **Loss:** Protocol funds **Root Cause:** Anyone could mint reward tokens without proper validation **Prevention:** Collateralization ratio assertions + +### [First Depositor Bug](/assertions-book/previous-hacks/first-depositor) +**Attack Type:** Share Price Manipulation +**Loss:** Various protocols affected +**Root Cause:** First depositor can manipulate exchange rate through donation +**Prevention:** Minimum supply assertions and exchange rate validation diff --git a/assertions-book/previous-hacks/uxlink-multisig-hack.mdx b/assertions-book/previous-hacks/uxlink-multisig-hack.mdx index 5811069..4e16795 100644 --- a/assertions-book/previous-hacks/uxlink-multisig-hack.mdx +++ b/assertions-book/previous-hacks/uxlink-multisig-hack.mdx @@ -40,7 +40,7 @@ Used multisig control to mint unlimited UXLINK tokens, causing a price crash and ## Proposed Solution -Multisig protection assertions could have prevented this attack: +Multisig protection assertions could have prevented this attack by enforcing governance invariants: ```solidity // SPDX-License-Identifier: MIT @@ -51,134 +51,114 @@ import {PhEvm} from "../../lib/credible-std/src/PhEvm.sol"; import {ISafe} from "@safe-global/safe-contracts/contracts/interfaces/ISafe.sol"; contract UxLinkMultisigProtectionAssertion is Assertion { - uint256 constant COOLING_PERIOD = 24 hours; - - mapping(address => uint256) public lastThresholdChange; - mapping(address => uint256) public lastOwnerChange; - mapping(address => mapping(address => bool)) public isOwnerWhitelisted; + // Minimum threshold that must be maintained + uint256 constant MIN_THRESHOLD = 2; + + // Whitelisted addresses that can become owners (set at deployment) + address constant ALLOWED_OWNER_1 = 0x1111111111111111111111111111111111111111; + address constant ALLOWED_OWNER_2 = 0x2222222222222222222222222222222222222222; + address constant ALLOWED_OWNER_3 = 0x3333333333333333333333333333333333333333; function triggers() external view override { - triggerRecorder.registerCallTrigger( + registerCallTrigger( this.assertThresholdProtection.selector, ISafe.changeThreshold.selector ); - - triggerRecorder.registerCallTrigger( + + registerCallTrigger( this.assertOwnerAddition.selector, ISafe.addOwnerWithThreshold.selector ); - - triggerRecorder.registerCallTrigger( + + registerCallTrigger( this.assertOwnerRemoval.selector, ISafe.removeOwner.selector ); } - /// @notice Prevents threshold reduction and ensures minimum threshold of 2 + /// @notice Prevents threshold reduction below minimum function assertThresholdProtection() external view { ISafe safe = ISafe(ph.getAssertionAdopter()); - + PhEvm.CallInputs[] memory calls = ph.getCallInputs( address(safe), ISafe.changeThreshold.selector ); - - uint256 newThreshold = abi.decode(calls[0].input, (uint256)); - uint256 currentThreshold = safe.getThreshold(); - - // Never allow threshold reduction - require(newThreshold >= currentThreshold, "Threshold cannot be lowered"); - - // Prevent rapid threshold changes - uint256 lastChange = lastThresholdChange[address(safe)]; - require( - block.timestamp >= lastChange + COOLING_PERIOD, - "Threshold change too soon after last change" - ); - - // Update timestamp if all checks pass - lastThresholdChange[address(safe)] = block.timestamp; + + for (uint256 i = 0; i < calls.length; i++) { + uint256 newThreshold = abi.decode(calls[i].input, (uint256)); + + // Never allow threshold below minimum + require(newThreshold >= MIN_THRESHOLD, "Threshold cannot go below minimum"); + } } - /// @notice Validates new owner additions and prevents threshold reduction + /// @notice Validates new owner additions against whitelist function assertOwnerAddition() external view { ISafe safe = ISafe(ph.getAssertionAdopter()); - + PhEvm.CallInputs[] memory calls = ph.getCallInputs( address(safe), ISafe.addOwnerWithThreshold.selector ); - - (address newOwner, uint256 threshold) = abi.decode(calls[0].input, (address, uint256)); - uint256 currentThreshold = safe.getThreshold(); - - // Basic validation - require(newOwner != address(0), "Invalid owner address"); - - // Check whitelist - assuming whitelist with future allowed owners - require(isOwnerWhitelisted[address(safe)][newOwner], "New owner not whitelisted"); - - // Never allow threshold reduction - require(threshold >= currentThreshold, "Threshold cannot be lowered"); - - // Prevent rapid owner changes - uint256 lastChange = lastOwnerChange[address(safe)]; - require( - block.timestamp >= lastChange + COOLING_PERIOD, - "Owner addition too soon after last change" - ); - - // Update timestamp if all checks pass - lastOwnerChange[address(safe)] = block.timestamp; - + + for (uint256 i = 0; i < calls.length; i++) { + (address newOwner, uint256 threshold) = abi.decode(calls[i].input, (address, uint256)); + + // Basic validation + require(newOwner != address(0), "Invalid owner address"); + + // Check whitelist + require( + newOwner == ALLOWED_OWNER_1 || + newOwner == ALLOWED_OWNER_2 || + newOwner == ALLOWED_OWNER_3, + "New owner not whitelisted" + ); + + // Never allow threshold below minimum + require(threshold >= MIN_THRESHOLD, "Threshold cannot go below minimum"); + } } - /// @notice Validates owner removals and prevents threshold reduction + /// @notice Validates owner removals don't reduce threshold below minimum function assertOwnerRemoval() external view { ISafe safe = ISafe(ph.getAssertionAdopter()); - + PhEvm.CallInputs[] memory calls = ph.getCallInputs( address(safe), ISafe.removeOwner.selector ); - - (address prevOwner, address ownerToRemove, uint256 threshold) = - abi.decode(calls[0].input, (address, address, uint256)); - uint256 currentThreshold = safe.getThreshold(); - - // Never allow threshold reduction - require(threshold >= currentThreshold, "Threshold cannot be lowered"); - - // Prevent rapid owner changes - uint256 lastChange = lastOwnerChange[address(safe)]; - require( - block.timestamp >= lastChange + COOLING_PERIOD, - "Owner removal too soon after last change" - ); - - // Update timestamp if all checks pass - lastOwnerChange[address(safe)] = block.timestamp; + + for (uint256 i = 0; i < calls.length; i++) { + (, , uint256 threshold) = abi.decode(calls[i].input, (address, address, uint256)); + + // Never allow threshold below minimum + require(threshold >= MIN_THRESHOLD, "Threshold cannot go below minimum"); + } } } ``` + +Assertions cannot track state across transactions (e.g., cooling periods). The original attack used rapid sequential transactions, which would require off-chain monitoring or timelocked governance contracts to fully prevent. However, the assertions above still provide strong protection by enforcing minimum thresholds and owner whitelisting. + + ### How These Assertions Prevent the Attack **What they do:** -1. **Threshold Protection**: Prevents any threshold reduction +1. **Threshold Protection**: Prevents threshold from dropping below a safe minimum (e.g., 2) 2. **Owner Whitelisting**: Only allows pre-approved addresses to become owners -3. **Cooling Periods**: Enforces 24-hour delays between configuration changes -4. **Timestamp Tracking**: Updates last change times to enforce cooling periods -5. **Batch Protection**: Prevents rapid owner additions/removals in sequence +3. **Removal Validation**: Ensures owner removals don't reduce threshold below minimum **How they prevent the attack:** -- **Step 1**: `assertThresholdProtection()` blocks threshold reduction and enforces 24-hour cooling period -- **Step 2**: `assertOwnerAddition()` blocks attacker address (not whitelisted) and enforces cooling period -- **Step 3**: `assertOwnerRemoval()` blocks rapid removal of legitimate owners and enforces cooling period -- **Result**: Prevents rapid reconfiguration and batching that enabled the multisig compromise +- **Step 1**: `assertThresholdProtection()` blocks any attempt to reduce threshold to 1 +- **Step 2**: `assertOwnerAddition()` blocks attacker addresses that aren't whitelisted +- **Step 3**: `assertOwnerRemoval()` ensures threshold stays above minimum even when removing owners +- **Result**: Attacker cannot gain solo control of the multisig -**Key insight**: These assertions enforce multisig governance principles with whitelist validation. They don't prevent private key compromise but prevent compromised keys from rapidly reconfiguring and draining multisigs. +**Key insight**: While these assertions can't prevent private key compromise or enforce time delays between transactions, they establish hard boundaries that attackers cannot cross regardless of how many keys they control. ## Key Takeaway diff --git a/assertions-book/previous-hacks/vicuna-finance-hack.mdx b/assertions-book/previous-hacks/vicuna-finance-hack.mdx index 0847065..7e3df27 100644 --- a/assertions-book/previous-hacks/vicuna-finance-hack.mdx +++ b/assertions-book/previous-hacks/vicuna-finance-hack.mdx @@ -21,13 +21,13 @@ A targeted price deviation check on all calls could have prevented this oracle m ```solidity function assertPriceDeviation() external view { BeetsLP assertionAdopter = BeetsLP(ph.getAssertionAdopter()); - ph.forkTxPre(); + ph.forkPreTx(); uint256 preOraclePrice = oracle.getPrice(token); // Get the price before the transaction // Using swap calls as an example, but any call that affects price should be checked PhEvm.CallInputs[] memory calls = ph.getCallInputs(address(assertionAdopter), assertionAdopter.swap.selector); for (uint256 i = 0; i < calls.length; i++) { - ph.forkCallPost(calls[i].id); + ph.forkPostCall(calls[i].id); uint256 postOraclePrice = oracle.getPrice(token); @@ -43,9 +43,9 @@ function assertPriceDeviation() external view { This assertion function detects oracle price manipulation by monitoring how each call affects prices. **How it works:** -1. **Captures baseline**: Uses `ph.forkTxPre()` to get the oracle price before any calls -2. **Monitors each call**: Iterates through calls (like swaps) that could affect the oracle price -3. **Checks price impact**: Uses `ph.forkCallPost()` to see how each call changed the oracle price +1. **Captures baseline**: Uses `ph.forkPreTx()` to get the oracle price before any calls +2. **Monitors each call**: Iterates through calls (like swaps) that could affect the oracle price +3. **Checks price impact**: Uses `ph.forkPostCall()` to see how each call changed the oracle price 4. **Enforces limits**: Reverts if any single call causes >5% price deviation from the baseline Using Phylax cheatcodes allows checking the oracle price at every call in the transaction, detecting price manipulation as it happens and preventing attacks that rely on temporary price distortions. diff --git a/assertions-book/previous-hacks/visor-finance-unrestricted-mint.mdx b/assertions-book/previous-hacks/visor-finance-unrestricted-mint.mdx index 618e556..3e11b83 100644 --- a/assertions-book/previous-hacks/visor-finance-unrestricted-mint.mdx +++ b/assertions-book/previous-hacks/visor-finance-unrestricted-mint.mdx @@ -33,16 +33,22 @@ The assertion could be triggered by a call to the deposit function. ```solidity function assertion_triggerDeposit_remainsSolvent() public view { - - uint256 postBalanceCollateral = visr.balanceOf(address(adopter)); - uint256 postTotalSupplyRewards = vvisr.totalSupply(); - uint256 postRatio = postBalanceCollateral / postTotalSupplyRewards; + // Get pre-transaction state ph.forkPreTx(); - uint256 preBalanceCollateral = visr.balanceOf(address(adopter)); uint256 preTotalSupplyRewards = vvisr.totalSupply(); - uint256 preRatio = preBalanceCollateral / preTotalSupplyRewards; - require(preRatio == postRatio, "Reward tokens are undercollateralized"); + // Get post-transaction state + ph.forkPostTx(); + uint256 postBalanceCollateral = visr.balanceOf(address(adopter)); + uint256 postTotalSupplyRewards = vvisr.totalSupply(); + + // Compare ratios using cross-multiplication to avoid precision loss + // preBalance / preSupply >= postBalance / postSupply + // => preBalance * postSupply >= postBalance * preSupply + require( + preBalanceCollateral * postTotalSupplyRewards >= postBalanceCollateral * preTotalSupplyRewards, + "Reward tokens are undercollateralized" + ); } ``` diff --git a/docs.json b/docs.json index 41a1d47..15cd10b 100644 --- a/docs.json +++ b/docs.json @@ -145,23 +145,23 @@ "group": "Previous Hacks", "pages": [ "assertions-book/previous-hacks/prev-hacks-index", - "assertions-book/previous-hacks/hack1-radiant-capital", - "assertions-book/previous-hacks/hack2-vestra-dao", - "assertions-book/previous-hacks/compound-upgrade-bug", - "assertions-book/previous-hacks/cream-finance-2", - "assertions-book/previous-hacks/visor-finance-unrestricted-mint", - "assertions-book/previous-hacks/first-depositor", - "assertions-book/previous-hacks/abracadabra-rounding-error", - "assertions-book/previous-hacks/euler-finance-donation-hack", + "assertions-book/previous-hacks/balancer-v2-stable-rate-exploit", "assertions-book/previous-hacks/bybit-safe-ui", - "assertions-book/previous-hacks/kiloex-price-manipulation-hack", "assertions-book/previous-hacks/gma-aum-jul25-hack", "assertions-book/previous-hacks/abracadabra-gmx-v2-exploit", "assertions-book/previous-hacks/abracadabra-hack-3", - "assertions-book/previous-hacks/vicuna-finance-hack", "assertions-book/previous-hacks/bunni-xyz-rounding-error", + "assertions-book/previous-hacks/hack1-radiant-capital", "assertions-book/previous-hacks/uxlink-multisig-hack", - "assertions-book/previous-hacks/balancer-v2-stable-rate-exploit" + "assertions-book/previous-hacks/kiloex-price-manipulation-hack", + "assertions-book/previous-hacks/hack2-vestra-dao", + "assertions-book/previous-hacks/vicuna-finance-hack", + "assertions-book/previous-hacks/euler-finance-donation-hack", + "assertions-book/previous-hacks/abracadabra-rounding-error", + "assertions-book/previous-hacks/visor-finance-unrestricted-mint", + "assertions-book/previous-hacks/first-depositor", + "assertions-book/previous-hacks/compound-upgrade-bug", + "assertions-book/previous-hacks/cream-finance-2" ] }, {