diff --git a/fv/harnesses/ERC4626Harness.sol b/fv/harnesses/ERC4626Harness.sol new file mode 100644 index 00000000000..2781fd4d625 --- /dev/null +++ b/fv/harnesses/ERC4626Harness.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.24; + +import {ERC4626, ERC20, IERC20} from "../patched/token/ERC20/extensions/ERC4626.sol"; + +contract ERC4626Harness is ERC4626 { + constructor(IERC20 asset_, string memory name_, string memory symbol_) ERC20(name_, symbol_) ERC4626(asset_) {} + + /// @dev Not part of ERC-4626. Models an asset donation: an external actor sending assets to the vault without + /// minting shares. Present so parametric rules and invariants range over it. + function donate(uint256 assets) public { + _transferIn(_msgSender(), assets); + } +} diff --git a/fv/harnesses/ERC4626OffsetHarness.sol b/fv/harnesses/ERC4626OffsetHarness.sol new file mode 100644 index 00000000000..89ee4a0da91 --- /dev/null +++ b/fv/harnesses/ERC4626OffsetHarness.sol @@ -0,0 +1,42 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.24; + +import {ERC4626, ERC20, IERC20} from "../patched/token/ERC20/extensions/ERC4626.sol"; + +/// @dev ERC4626Harness with the decimals offset left symbolic instead of pinned to zero. The offset +/// is an immutable the prover treats as an unconstrained constant, so rules verified here hold for +/// every offset a deployment could choose, not just the default. +contract ERC4626OffsetHarness is ERC4626 { + uint8 private immutable _offset; + + constructor( + IERC20 asset_, + string memory name_, + string memory symbol_, + uint8 offset_ + ) ERC20(name_, symbol_) ERC4626(asset_) { + _offset = offset_; + } + + function _decimalsOffset() internal view override returns (uint8) { + return _offset; + } + + /// @dev Exposed so rules can constrain the offset and state the range they hold over. + function decimalsOffset() public view returns (uint8) { + return _offset; + } + + /// @dev The virtual share supply, 10**offset. Exposed so rules can state bounds in terms of the + /// quantity the conversions actually use, rather than re-deriving the exponentiation in CVL. + function virtualShares() public view returns (uint256) { + return 10 ** _decimalsOffset(); + } + + /// @dev Not part of ERC-4626. Models an asset donation: an external actor sending assets to the + /// vault without minting shares. Present so parametric rules and invariants range over it. + function donate(uint256 assets) public { + _transferIn(_msgSender(), assets); + } +} diff --git a/fv/specs/ERC4626.conf b/fv/specs/ERC4626.conf new file mode 100644 index 00000000000..abcff5f6c6b --- /dev/null +++ b/fv/specs/ERC4626.conf @@ -0,0 +1,24 @@ +{ + "build_cache": true, + "exclude_rule": [ + "depositIsNotSplittable", + "withdrawIsNotSplittable", + "holdingBackAcrossDonationDoesNotPay" + ], + "files": [ + "fv/harnesses/ERC4626Harness.sol" + ], + "global_timeout": 600, + "msg": "ERC4626 tier 1: everything but the anti-splitting rules", + "optimistic_loop": true, + "packages": [ + "@openzeppelin/contracts=fv/patched" + ], + "parametric_contracts": [ + "ERC4626Harness" + ], + "process": "emv", + "rule_sanity": "basic", + "url_visibility": "public", + "verify": "ERC4626Harness:fv/specs/ERC4626.spec" +} diff --git a/fv/specs/ERC4626.spec b/fv/specs/ERC4626.spec new file mode 100644 index 00000000000..dd2e473c953 --- /dev/null +++ b/fv/specs/ERC4626.spec @@ -0,0 +1,430 @@ +// Two configs verify this file. ERC4626_split.conf takes depositIsNotSplittable, which needs tuned +// solver settings for nonlinear share math; ERC4626.conf excludes the three anti-splitting rules and +// runs everything else, so a rule added here runs without being named anywhere. The other two +// anti-splitting rules are excluded from both and carry a note of their own. +// +// Every config sets rule_sanity, so no rule here needs a hand-written reachability guard. +// +// P1 (solvency) lives in ERC4626Offset.spec, where the decimals offset is symbolic. + +import "ERC4626Base.spec"; +import "helpers/erc20-supply.spec"; + +// Checks that every contract function has at least one non-reverting path. A function that always +// reverts makes every rule calling it vacuous, with no `require` involved. +use builtin rule sanity; + +// Proves the imported sum-of-balances invariant here, rather than only assuming it. +use invariant totalSupplyIsSumOfBalances; + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P2: round trips never create value, and per-operation leakage is at most one unit │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// The no-free-money half. Both directions of a round trip are stated on the preview functions, so +/// this holds for every state rather than only the ones a deposit could reach. +rule roundTripNeverCreatesValue(uint256 assets) { + require sane(); + + // Deposit then redeem never returns more than was put in. + assert previewRedeem(previewDeposit(assets)) <= assets; + // Withdraw then re-mint never costs less than was taken out. + assert previewMint(previewWithdraw(assets)) >= assets; +} + +/// The tightness half. Bounding leakage at one unit catches a preview override whose rounding +/// direction is transposed, which ERC4626 warns about: overrides to the deposit or withdraw +/// mechanism must be reflected in the preview functions. +/// +/// previewWithdraw and previewDeposit are the same conversion at Ceil and Floor, as are previewMint +/// and previewRedeem, so each gap is a ceil-minus-floor and lands in {0, 1}. +rule roundingGapIsAtMostOne(uint256 assets, uint256 shares) { + require sane(); + + mathint depositGap = previewWithdraw(assets) - previewDeposit(assets); + mathint mintGap = previewMint(shares) - previewRedeem(shares); + + assert depositGap >= 0 && depositGap <= 1; + assert mintGap >= 0 && mintGap <= 1; +} + +/// Witnesses that the bounds above are reachable. Mandatory: `assert gap <= 1` is trivially true of +/// a gap that is always zero, and rule_sanity cannot flag it because the assertion is reached. Kept +/// as separate rules so neither witness can be weakened by sharing a path with the other. +rule depositGapCanBeOne(uint256 assets) { + require sane(); + satisfy previewWithdraw(assets) - previewDeposit(assets) == 1; +} + +rule mintGapCanBeOne(uint256 shares) { + require sane(); + satisfy previewMint(shares) - previewRedeem(shares) == 1; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P3: the max/preview boundary - what the limits promise, the operations honour │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// maxWithdraw floors on the way out while previewWithdraw ceils on the way back, so it is not +/// obvious the round trip stays inside the owner's share balance. It does: m = floor(b(A+1)/(T+K)) +/// gives m(T+K)/(A+1) <= b, and b is an integer, so ceil(m(T+K)/(A+1)) <= b. That is what keeps +/// withdraw(maxWithdraw(o)) from reverting on the burn, which is why the third assertion carries +/// the weight of P3. +rule maxBoundaryIsConsistent(address owner) { + require sane(); + requireInvariant totalSupplyIsSumOfBalances(); + + assert maxRedeem(owner) == balanceOf(owner); + assert maxWithdraw(owner) == previewRedeem(maxRedeem(owner)); + assert previewWithdraw(maxWithdraw(owner)) <= balanceOf(owner); +} + +/// Liveness: the advertised limit is actually reachable. No invariant catches this - a max() that +/// over-promises leaves every value rule green while the operation reverts. +/// +/// Both rules fix owner == msg.sender, so no allowance is spent and the claim is narrowed to +/// self-withdrawals; the allowance path belongs to the conservation rules. msg.sender must be +/// nonzero because burning from the zero address reverts regardless of amount. +/// +/// noVirtualOverflow is stated on both, though only redeem needs it to pass: withdraw reaches the +/// same state through maxWithdraw, whose own revert prunes the path before the assertion. Assuming +/// it explicitly keeps the two rules covering the same states. +rule redeemMaxNeverReverts(env e, address receiver) { + require sane(); + require nonpayable(e); + require nonzerosender(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address owner = e.msg.sender; + redeem@withrevert(e, maxRedeem(owner), receiver, owner); + assert !lastReverted; +} + +rule withdrawMaxNeverReverts(env e, address receiver) { + require sane(); + require nonpayable(e); + require nonzerosender(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address owner = e.msg.sender; + withdraw@withrevert(e, maxWithdraw(owner), receiver, owner); + assert !lastReverted; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P4: splitting an operation into steps never beats doing it in one │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Three details carry this rule. The observable is the credited share balance rather than the +/// return value, which is what catches "returned the right number, booked the wrong one". The +/// inequality direction is derived from the rounding mode: previewDeposit floors, so a credit rounds +/// down and the one-shot call must not pay out less than the split. And the combined amount uses +/// assert_uint256, not require_uint256, so an overflowing sum fails the rule instead of being +/// assumed away - that boundary is where a splitting attack would live. +/// +/// Both histories start from the same snapshot, so the receiver's pre-existing balance cancels and +/// comparing absolute balances is sound. +rule depositIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require receiver != 0 && e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + storage init = lastStorage; + + deposit(e, x, receiver); + deposit(e, y, receiver); + mathint split = balanceOf(receiver); + + deposit(e, assert_uint256(x + y), receiver) at init; + mathint combined = balanceOf(receiver); + + assert combined >= split; // credit rounds down => one step favours the depositor + satisfy combined > split; // ... and it actually bites somewhere +} + +/// The mirror. previewWithdraw ceils, so shares burned round up and two burns overcharge by more +/// than one: the split must never burn fewer shares than the one-shot. Burning more leaves less, so +/// in terms of the remaining balance the direction is the same as deposit. +/// +/// NOT PROVED: times out (3003s) and is excluded from every config. Holds under exhaustive +/// small-value and large random sampling; the `satisfy` alone verifies in 9s. Re-attempt with: +/// certoraRun fv/specs/ERC4626_split.conf --rule withdrawIsNotSplittable --global_timeout 3600 --smt_timeout 1500 +/// https://prover.certora.com/output/1392759/b8f698631bf44d2692643a24910ab356?anonymousKey=4665bdc5b6546cb042145a333d271d06c89e44a4 +rule withdrawIsNotSplittable(env e, uint256 x, uint256 y, address receiver) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require nonzerosender(e); + require receiver != 0 && receiver != currentContract && e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + address owner = e.msg.sender; + storage init = lastStorage; + + withdraw(e, x, receiver, owner); + withdraw(e, y, receiver, owner); + mathint split = balanceOf(owner); + + withdraw(e, assert_uint256(x + y), receiver, owner) at init; + mathint combined = balanceOf(owner); + + assert combined >= split; + satisfy combined > split; +} + +/// The variant only a donation model can express. Both histories spend the same x + y + d assets; +/// only the ordering differs. +/// +/// The baseline is depositing up front, not depositing after the donation: entering before a +/// donation is cheaper than entering after one by an unbounded margin, which is what a donation +/// means rather than a flaw. The claim is that holding part of a deposit back across a donation +/// never gains shares over committing it all at once. +/// +/// NOT PROVED: times out (1504s) and is excluded from every config. Holds under exhaustive +/// small-value and large random sampling; the share math alone verifies in ~1s, so the cost is +/// replaying five calls. Re-attempt with: +/// certoraRun fv/specs/ERC4626_split.conf --rule holdingBackAcrossDonationDoesNotPay --global_timeout 3600 --smt_timeout 1500 +/// https://prover.certora.com/output/1392759/b8f698631bf44d2692643a24910ab356?anonymousKey=4665bdc5b6546cb042145a333d271d06c89e44a4 +rule holdingBackAcrossDonationDoesNotPay(env e, uint256 x, uint256 y, uint256 d, address receiver) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + require receiver != 0 && e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + storage init = lastStorage; + + deposit(e, x, receiver); + donate(e, d); + deposit(e, y, receiver); + mathint heldBack = balanceOf(receiver); + + deposit(e, assert_uint256(x + y), receiver) at init; + donate(e, d); + mathint upfront = balanceOf(receiver); + + assert heldBack <= upfront; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P5: no method can lower the exchange rate │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Deposits round shares minted down and withdrawals round shares burned up, so in every direction +/// the rounding residue stays with the vault and the price per share can only rise or hold. +/// +/// Ranges over the harness method set, which includes donate(); see ERC4626Base.spec for why. +rule rateNeverDecreases(env e, method f) filtered { f -> !f.isView } { + require sane(); + require noVirtualOverflow(); + require e.msg.sender != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + mathint before = convertToAssets(ONE_SHARE()); + + calldataarg args; + f(e, args); + + assert to_mathint(convertToAssets(ONE_SHARE())) >= before; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P6: an asset inflow never reduces what an existing holder can redeem │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// An inflow raises totalAssets and leaves totalSupply alone, so the conversion's denominator is +/// untouched and its numerator only grows. +/// +/// Stated on the ghost rather than on donate() so it covers an inflow arriving by any means: a raw +/// transfer from an address that never touches the vault, yield accrual, a rebase up. donate() +/// itself is covered by rateNeverDecreases. +rule assetInflowNeverHarmsHolders(uint256 d, address holder) { + require sane(); + require noVirtualOverflow(); + require holder != currentContract; + requireInvariant totalSupplyIsSumOfBalances(); + + address token = asset(); + // The post-state must convert too, or the second probe reverts and prunes the path invisibly. + require to_mathint(totalAssets()) + to_mathint(d) < max_uint256; + + mathint before = previewRedeem(balanceOf(holder)); + + balanceByToken[token][currentContract] = + require_uint256(balanceByToken[token][currentContract] + d); + + assert to_mathint(previewRedeem(balanceOf(holder))) >= before; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Conservation and isolation: the state-changers move exactly what they claim, and nothing else │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Supporting machinery rather than a headline property. The value properties all assume the +/// operations move the right amounts between the right parties; without these they can pass for the +/// wrong reason. +/// +/// `other` is a free rule parameter, so the prover quantifies over it universally. That is what +/// makes the isolation assertions meaningful with no disequality assumption and with no way to go +/// vacuous - a fresh symbol pinned by a `require` would give neither. +/// +/// Every preview is read before the operation. Read afterwards it would be a different number, +/// since the operation moves both sides of the conversion. +rule depositConserves(env e, uint256 assets, address receiver, address other) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address caller = e.msg.sender; + address token = asset(); + require caller != currentContract && receiver != 0; + + mathint expectedShares = previewDeposit(assets); + mathint supplyBefore = totalSupply(); + mathint receiverSharesBefore = balanceOf(receiver); + mathint vaultAssetsBefore = balanceByToken[token][currentContract]; + mathint callerAssetsBefore = balanceByToken[token][caller]; + mathint otherSharesBefore = balanceOf(other); + mathint otherAssetsBefore = balanceByToken[token][other]; + + uint256 shares = deposit(e, assets, receiver); + + // effects: shares credited match the preview, assets moved match the request + assert to_mathint(shares) == expectedShares; + assert to_mathint(totalSupply()) == supplyBefore + shares; + assert to_mathint(balanceOf(receiver)) == receiverSharesBefore + shares; + assert balanceByToken[token][currentContract] == vaultAssetsBefore + assets; + assert balanceByToken[token][caller] == callerAssetsBefore - assets; + + // isolation: nobody else moved + assert balanceOf(other) != otherSharesBefore => other == receiver; + assert balanceByToken[token][other] != otherAssetsBefore + => (other == caller || other == currentContract); +} + +rule mintConserves(env e, uint256 shares, address receiver, address other) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address caller = e.msg.sender; + address token = asset(); + require caller != currentContract && receiver != 0; + + mathint expectedAssets = previewMint(shares); + mathint supplyBefore = totalSupply(); + mathint receiverSharesBefore = balanceOf(receiver); + mathint vaultAssetsBefore = balanceByToken[token][currentContract]; + mathint callerAssetsBefore = balanceByToken[token][caller]; + mathint otherSharesBefore = balanceOf(other); + mathint otherAssetsBefore = balanceByToken[token][other]; + + uint256 assets = mint(e, shares, receiver); + + assert to_mathint(assets) == expectedAssets; + assert to_mathint(totalSupply()) == supplyBefore + shares; + assert to_mathint(balanceOf(receiver)) == receiverSharesBefore + shares; + assert balanceByToken[token][currentContract] == vaultAssetsBefore + assets; + assert balanceByToken[token][caller] == callerAssetsBefore - assets; + + assert balanceOf(other) != otherSharesBefore => other == receiver; + assert balanceByToken[token][other] != otherAssetsBefore + => (other == caller || other == currentContract); +} + +/// Covers the third-party allowance path that the P3 liveness rules deliberately scoped out. +rule withdrawConserves(env e, uint256 assets, address receiver, address owner, address other) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address caller = e.msg.sender; + address token = asset(); + require caller != currentContract && receiver != 0 && receiver != currentContract; + + mathint expectedShares = previewWithdraw(assets); + mathint supplyBefore = totalSupply(); + mathint ownerSharesBefore = balanceOf(owner); + mathint vaultAssetsBefore = balanceByToken[token][currentContract]; + mathint recvAssetsBefore = balanceByToken[token][receiver]; + mathint allowanceBefore = allowance(owner, caller); + mathint otherSharesBefore = balanceOf(other); + mathint otherAssetsBefore = balanceByToken[token][other]; + + uint256 shares = withdraw(e, assets, receiver, owner); + + assert to_mathint(shares) == expectedShares; + assert to_mathint(totalSupply()) == supplyBefore - shares; + assert to_mathint(balanceOf(owner)) == ownerSharesBefore - shares; + assert balanceByToken[token][currentContract] == vaultAssetsBefore - assets; + assert balanceByToken[token][receiver] == recvAssetsBefore + assets; + + // A third-party caller spends allowance; the owner acting for themselves does not. Infinite + // approval is left untouched, by ERC20 design. + assert caller != owner && allowanceBefore < to_mathint(max_uint256) + => to_mathint(allowance(owner, caller)) == allowanceBefore - shares; + assert caller != owner && allowanceBefore == to_mathint(max_uint256) + => to_mathint(allowance(owner, caller)) == allowanceBefore; + assert caller == owner => to_mathint(allowance(owner, caller)) == allowanceBefore; + + assert balanceOf(other) != otherSharesBefore => other == owner; + assert balanceByToken[token][other] != otherAssetsBefore + => (other == receiver || other == currentContract); +} + +rule redeemConserves(env e, uint256 shares, address receiver, address owner, address other) { + require sane(); + require nonpayable(e); + require noVirtualOverflow(); + requireInvariant totalSupplyIsSumOfBalances(); + + address caller = e.msg.sender; + address token = asset(); + require caller != currentContract && receiver != 0 && receiver != currentContract; + + mathint expectedAssets = previewRedeem(shares); + mathint supplyBefore = totalSupply(); + mathint ownerSharesBefore = balanceOf(owner); + mathint vaultAssetsBefore = balanceByToken[token][currentContract]; + mathint recvAssetsBefore = balanceByToken[token][receiver]; + mathint allowanceBefore = allowance(owner, caller); + mathint otherSharesBefore = balanceOf(other); + mathint otherAssetsBefore = balanceByToken[token][other]; + + uint256 assets = redeem(e, shares, receiver, owner); + + assert to_mathint(assets) == expectedAssets; + assert to_mathint(totalSupply()) == supplyBefore - shares; + assert to_mathint(balanceOf(owner)) == ownerSharesBefore - shares; + assert balanceByToken[token][currentContract] == vaultAssetsBefore - assets; + assert balanceByToken[token][receiver] == recvAssetsBefore + assets; + + assert caller != owner && allowanceBefore < to_mathint(max_uint256) + => to_mathint(allowance(owner, caller)) == allowanceBefore - shares; + assert caller != owner && allowanceBefore == to_mathint(max_uint256) + => to_mathint(allowance(owner, caller)) == allowanceBefore; + assert caller == owner => to_mathint(allowance(owner, caller)) == allowanceBefore; + + assert balanceOf(other) != otherSharesBefore => other == owner; + assert balanceByToken[token][other] != otherAssetsBefore + => (other == receiver || other == currentContract); +} diff --git a/fv/specs/ERC4626Base.spec b/fv/specs/ERC4626Base.spec new file mode 100644 index 00000000000..ca57d509100 --- /dev/null +++ b/fv/specs/ERC4626Base.spec @@ -0,0 +1,76 @@ +// Shared base for the ERC4626 suite: the summary layer plus the scope definitions. Every summary +// the suite relies on is declared here, so what is assumed here is assumed by every config. +// +// ASSUMED, NOT PROVED. Every rule in this suite is conditional on all of the following: +// - Math.mulDiv is replaced by a closed form, so rules are conditional on that form matching the +// implementation in both value and revert domain. Only the 4-argument overload is bound; it is +// the only one ERC4626 calls. +// - The underlying asset has no contract in the scene. Its balances and allowances are ghost +// state, which under-approximates real tokens: no fee-on-transfer, no rebase-down, no ERC-777 +// reentrancy. +// - _decimalsOffset() is 0 in ERC4626Harness, so nothing verified against it generalizes to a +// larger offset. ERC4626Offset.spec proves solvency and the donation attack against a harness +// whose offset is symbolic; every other result in the suite is a zero-offset result. +// - optimistic_loop is set on every config, so loops are assumed to terminate within the bound. +// +// Parametric rules range over the harness, which adds a non-production donate() and deliberately +// exposes no share mint or burn. Both are part of the claim: a raw asset inflow is the inflation +// attack's vector and no parametric rule over the production contract can reach it, while an +// unbacked mint would falsify rate monotonicity. +// +// Rules that are not proved at all are marked NOT PROVED where they are declared, with the command +// to re-attempt them. + +import "helpers/helpers.spec"; +import "helpers/math-cvl.spec"; +import "helpers/erc20-cvl.spec"; + +methods { + // ---- shares token (the vault itself) ---- + function totalSupply() external returns (uint256) envfree; + function balanceOf(address) external returns (uint256) envfree; + function allowance(address,address) external returns (uint256) envfree; + + // ---- vault views ---- + function asset() external returns (address) envfree; + function totalAssets() external returns (uint256) envfree; + function convertToShares(uint256) external returns (uint256) envfree; + function convertToAssets(uint256) external returns (uint256) envfree; + function maxDeposit(address) external returns (uint256) envfree; + function maxMint(address) external returns (uint256) envfree; + function maxWithdraw(address) external returns (uint256) envfree; + function maxRedeem(address) external returns (uint256) envfree; + function previewDeposit(uint256) external returns (uint256) envfree; + function previewMint(uint256) external returns (uint256) envfree; + function previewWithdraw(uint256) external returns (uint256) envfree; + function previewRedeem(uint256) external returns (uint256) envfree; + + // ---- summaries ---- + // Trusted, not proved. ERC4626 only calls this overload, so summarizing it bypasses Math + // entirely; the 3-arg overload is left unbound because it would never fire. + function _.mulDiv(uint256 x, uint256 y, uint256 d, Math.Rounding r) internal + => mulDivCVL(x, y, d, r) expect uint256; + + // Asset token, modelled as ghost state. See erc20-cvl.spec for what this leaves out. + function _.safeTransfer(address token, address to, uint256 v) internal + => safeTransferCVL(token, executingContract, to, v) expect void; + function _.safeTransferFrom(address token, address from, address to, uint256 v) internal + => safeTransferFromCVL(token, executingContract, from, to, v) expect void; + function _.balanceOf(address account) external + => balanceByToken[calledContract][account] expect uint256; + + // Constructor-only. Feeds _underlyingDecimals, which only decimals() reads and no rule here does. + function _.tryGetDecimals(address token) internal + => tryGetDecimalsCVL() expect (bool, uint8); +} + +/// Scope assumptions, applied by every rule. A vault whose asset is itself, or the zero address, is +/// not a configuration this suite reasons about. +definition sane() returns bool = asset() != currentContract && asset() != 0; + +/// The virtual-asset design computes totalAssets() + 1 and totalSupply() + 10**offset, so a vault +/// holding the entire uint256 range reverts in every conversion. Value rules prune that state on +/// their own, because the preview call they compare against is the thing that reverts. Liveness +/// rules cannot rely on that and must exclude it by name. +definition noVirtualOverflow() returns bool = + totalAssets() < max_uint256 && totalSupply() < max_uint256; diff --git a/fv/specs/ERC4626Donation.conf b/fv/specs/ERC4626Donation.conf new file mode 100644 index 00000000000..e80179f58f0 --- /dev/null +++ b/fv/specs/ERC4626Donation.conf @@ -0,0 +1,23 @@ +{ + "build_cache": true, + "files": [ + "fv/harnesses/ERC4626Harness.sol" + ], + "global_timeout": 1800, + "msg": "ERC4626 tier 3: donation attack non-profitability", + "optimistic_loop": true, + "packages": [ + "@openzeppelin/contracts=fv/patched" + ], + "parametric_contracts": [ + "ERC4626Harness" + ], + "process": "emv", + "prover_args": [ + "-smt_useLIA false -smt_useNIA true -splitParallel true -dontStopAtFirstSplitTimeout true -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "rule_sanity": "basic", + "smt_timeout": "1200", + "url_visibility": "public", + "verify": "ERC4626Harness:fv/specs/ERC4626Donation.spec" +} diff --git a/fv/specs/ERC4626Donation.spec b/fv/specs/ERC4626Donation.spec new file mode 100644 index 00000000000..73a1bd44750 --- /dev/null +++ b/fv/specs/ERC4626Donation.spec @@ -0,0 +1,52 @@ +// Kept out of ERC4626.spec so its tuned solver settings do not slow the tier-1 sweep. +// +// Verified by two configs: ERC4626Donation.conf against the zero-offset harness and +// ERC4626OffsetDonation.conf against the symbolic-offset one. Nothing here mentions the offset. + +import "ERC4626Base.spec"; +import "helpers/erc20-supply.spec"; + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P7: the donation attack is not profitable against a fresh vault │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// The inflation attack: enter, inflate the share price with a donation, let a victim deposit at the +/// manipulated rate, exit. Asserting the attacker's asset balance never rises across the sequence +/// captures "never profits" in one assertion, with no separate accounting of what they paid. +/// +/// Scoped to a vault that starts empty: that is what the virtual-shares mitigation claims, and the +/// only scope in which the claim is true. An arbitrary (totalSupply, totalAssets) start admits states +/// that are already manipulated - one share outstanding against a large asset balance - where an +/// attacker profits without donating anything. ERC4626 documents that empty and nearly-empty vaults +/// are the hazard and directs deployers to seed them. +/// +/// Because totalSupply starts at zero, the attacker starts with no shares, so redeeming their whole +/// balance redeems only what this sequence minted. +rule donationAttackNeverProfits(env eAtt, env eVic, uint256 a1, uint256 d, uint256 a2) { + require sane(); + require nonpayable(eAtt) && nonpayable(eVic); + require noVirtualOverflow(); + // Proved by ERC4626.conf for the zero-offset harness and ERC4626Offset.conf for the offset one. + requireInvariant totalSupplyIsSumOfBalances(); + + address attacker = eAtt.msg.sender; + address victim = eVic.msg.sender; + address token = asset(); + require attacker != victim; + require attacker != currentContract && victim != currentContract; + require attacker != 0 && victim != 0; + + // A fresh vault: no shares outstanding and no assets held. + require totalSupply() == 0 && totalAssets() == 0; + + mathint attackerAssetsBefore = balanceByToken[token][attacker]; + + deposit(eAtt, a1, attacker); // attacker enters + donate(eAtt, d); // inflate the rate + deposit(eVic, a2, victim); // victim deposits at the new rate + redeem(eAtt, balanceOf(attacker), attacker, attacker); // attacker exits fully + + assert balanceByToken[token][attacker] <= attackerAssetsBefore; +} diff --git a/fv/specs/ERC4626Offset.conf b/fv/specs/ERC4626Offset.conf new file mode 100644 index 00000000000..eb5018ca2d8 --- /dev/null +++ b/fv/specs/ERC4626Offset.conf @@ -0,0 +1,19 @@ +{ + "build_cache": true, + "files": [ + "fv/harnesses/ERC4626OffsetHarness.sol" + ], + "global_timeout": 600, + "msg": "ERC4626 tier 4: symbolic decimals offset", + "optimistic_loop": true, + "packages": [ + "@openzeppelin/contracts=fv/patched" + ], + "parametric_contracts": [ + "ERC4626OffsetHarness" + ], + "process": "emv", + "rule_sanity": "basic", + "url_visibility": "public", + "verify": "ERC4626OffsetHarness:fv/specs/ERC4626Offset.spec" +} diff --git a/fv/specs/ERC4626Offset.spec b/fv/specs/ERC4626Offset.spec new file mode 100644 index 00000000000..5624654d8fa --- /dev/null +++ b/fv/specs/ERC4626Offset.spec @@ -0,0 +1,86 @@ +// Tier 4: the decimals offset left symbolic. +// +// Every other spec in this suite runs against a harness whose _decimalsOffset() is 0, so K = 1 in +// both conversion denominators and nothing proved there generalizes. Here the offset is an +// immutable the prover leaves unconstrained, so K = 10**offset is a symbolic exponentiation. No rule +// abstracts it behind a ghost or needs the offset bounded, so this tier carries no assumption the +// rest of the suite does not. +// +// Offsets from 78 up make 10**offset overflow uint256, so every conversion reverts and the prover +// prunes those paths. The rules here are claims about offsets 0 through 77. +// +// The donation attack is also re-proved at a symbolic offset: ERC4626OffsetDonation.conf points the +// unchanged ERC4626Donation.spec at this file's harness. + +import "ERC4626Base.spec"; +import "helpers/erc20-supply.spec"; + +// ERC4626OffsetDonation.conf assumes this invariant, so it is proved here for the offset harness. +// Its Sload hook bounds every balance read; no rule below reads one. +use invariant totalSupplyIsSumOfBalances; + +methods { + function decimalsOffset() external returns (uint8) envfree; + function virtualShares() external returns (uint256) envfree; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Vacuity guard: the offset is genuinely symbolic, and a live vault is reachable at a nonzero one │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// rule_sanity cannot catch this: every rule below is satisfiable at offset 0 alone, which would +/// make the tier a restatement of what the zero-offset harness already proves. +rule offsetIsGenuinelySymbolic(uint256 shares) { + require sane(); + require decimalsOffset() > 0; + require totalSupply() > 0 && totalAssets() > 0; + satisfy previewRedeem(shares) > 0; +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ P1: the vault is never over-committed - every outstanding share is redeemable simultaneously │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// Holds in every state, with no assumption about how that state was reached, so this is stated as a +/// rule rather than an invariant: quantifying over all sane states is stronger than quantifying over +/// reachable ones. +/// +/// With K = 10^offset >= 1, previewRedeem(T) = floor(T(A+1)/(T+K)), and floor(x) <= A iff x < A+1, +/// so the obligation reduces to T(A+1) < (A+1)(T+K), i.e. 0 < (A+1)K. True for all T, A and K >= 1 +/// with no relationship between T and A, which is why induction is unnecessary. The bound is not +/// trivially tight: equality (T = A = 0) and strict inequality are both reachable. +/// +/// Proved here rather than on the zero-offset harness because the argument is offset-independent +/// only on paper; this is the harness on which the prover checks it for every K. +rule vaultNeverOvercommitted() { + require sane(); + assert previewRedeem(totalSupply()) <= totalAssets(); +} + +/* +┌────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ What the offset is FOR: it prices the inflation attack, and only a symbolic offset can say so │ +└────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +/// ERC4626 does not claim the virtual shares prevent the inflation attack; it claims they make it +/// "orders of magnitude more expensive than it is profitable". That is a claim about a quantity, and +/// it is invisible to any rule that pins the quantity to 1. +/// +/// A victim is only robbed if their deposit rounds to zero shares, and +/// previewDeposit(a) = floor(a(T+K)/(A+1)) is zero only when a(T+K) < A+1. With K = 10^offset and +/// T >= 0 that forces A >= a*K: for a deposit of a to mint nothing, the vault must already hold at +/// least a * 10^offset assets, so the attack costs 10^offset times what it takes from the victim. +/// +/// The bound is tight (A = a*K is reachable) and degrades to the trivially true A >= a at offset 0. +/// It is violated by a mutation that drops the offset from the share conversion. +rule inflationCostScalesWithOffset(uint256 assets) { + require sane(); + require assets > 0; + require previewDeposit(assets) == 0; + assert to_mathint(totalAssets()) >= to_mathint(assets) * to_mathint(virtualShares()); +} diff --git a/fv/specs/ERC4626OffsetDonation.conf b/fv/specs/ERC4626OffsetDonation.conf new file mode 100644 index 00000000000..c2849c91c7a --- /dev/null +++ b/fv/specs/ERC4626OffsetDonation.conf @@ -0,0 +1,23 @@ +{ + "build_cache": true, + "files": [ + "fv/harnesses/ERC4626OffsetHarness.sol" + ], + "global_timeout": 1800, + "msg": "ERC4626 tier 4: donation attack at a symbolic decimals offset", + "optimistic_loop": true, + "packages": [ + "@openzeppelin/contracts=fv/patched" + ], + "parametric_contracts": [ + "ERC4626OffsetHarness" + ], + "process": "emv", + "prover_args": [ + "-smt_useLIA false -smt_useNIA true -splitParallel true -dontStopAtFirstSplitTimeout true -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "rule_sanity": "basic", + "smt_timeout": "1200", + "url_visibility": "public", + "verify": "ERC4626OffsetHarness:fv/specs/ERC4626Donation.spec" +} diff --git a/fv/specs/ERC4626_split.conf b/fv/specs/ERC4626_split.conf new file mode 100644 index 00000000000..8fd78e2baed --- /dev/null +++ b/fv/specs/ERC4626_split.conf @@ -0,0 +1,26 @@ +{ + "build_cache": true, + "files": [ + "fv/harnesses/ERC4626Harness.sol" + ], + "global_timeout": 900, + "independent_satisfy": true, + "msg": "ERC4626 anti-splitting shard: nonlinear share math, splitting off, seed race", + "optimistic_loop": true, + "packages": [ + "@openzeppelin/contracts=fv/patched" + ], + "parametric_contracts": [ + "ERC4626Harness" + ], + "process": "emv", + "prover_args": [ + "-destructiveOptimizations twostage -backendStrategy singleRace -smt_useLIA false -smt_useNIA true -depth 0 -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "rule": [ + "depositIsNotSplittable" + ], + "rule_sanity": "basic", + "url_visibility": "public", + "verify": "ERC4626Harness:fv/specs/ERC4626.spec" +} diff --git a/fv/specs/helpers/erc20-cvl.spec b/fv/specs/helpers/erc20-cvl.spec new file mode 100644 index 00000000000..fd0565f87e0 --- /dev/null +++ b/fv/specs/helpers/erc20-cvl.spec @@ -0,0 +1,34 @@ +// Ghost-backed model of the underlying asset token. Definitions only - no methods block. +// +// The asset has no contract in the scene, so its balances live entirely in ghost state. This +// under-approximates real tokens: no fee-on-transfer, no rebase-down, no ERC-777 reentrancy. + +/// token => account => balance +ghost mapping(address => mapping(address => uint256)) balanceByToken; +/// token => owner => spender => allowance +ghost mapping(address => mapping(address => mapping(address => uint256))) allowanceByToken; + +function revertOn(bool b) { if (b) { revert(); } } + +/// SafeERC20 reverts on failure, so these model a revert rather than a false return. +/// require_uint256 on the credit side neglects overflow of the receiving balance; the vault's own +/// balance is bounded by the solvency invariant. Revisit if a counterexample ever turns on it. +function safeTransferCVL(address token, address from, address to, uint256 amount) { + revertOn(balanceByToken[token][from] < amount); + balanceByToken[token][from] = require_uint256(balanceByToken[token][from] - amount); + balanceByToken[token][to] = require_uint256(balanceByToken[token][to] + amount); +} + +function safeTransferFromCVL(address token, address spender, address from, address to, uint256 amount) { + revertOn(allowanceByToken[token][from][spender] < amount); + safeTransferCVL(token, from, to, amount); + allowanceByToken[token][from][spender] = + require_uint256(allowanceByToken[token][from][spender] - amount); +} + +function tryGetDecimalsCVL() returns (bool, uint8) { + return (true, 18); +} + +/// Exchange-rate probe. One share at 18 decimals. +definition ONE_SHARE() returns uint256 = 1000000000000000000; diff --git a/fv/specs/helpers/erc20-supply.spec b/fv/specs/helpers/erc20-supply.spec new file mode 100644 index 00000000000..c20a73de1a3 --- /dev/null +++ b/fv/specs/helpers/erc20-supply.spec @@ -0,0 +1,23 @@ +// Sum-of-balances ghost for the shares token, extracted so several ERC4626 specs can share it. +// +// ERC20.spec keeps its own copy and is deliberately not imported here: its methods block requires +// mint and burn on the verification target, and exposing unbacked share mint on an ERC4626 harness +// would falsify the solvency and rate-monotonicity properties. + +ghost mathint sumOfBalances { + init_state axiom sumOfBalances == 0; +} + +// Bounds a balance by the tracked sum. Without it, explicit casting admits a pre-state where one +// balance exceeds totalSupply and overflows on receipt - reachable only by deploying into a dirty +// address. +hook Sload uint256 balance _balances[KEY address addr] { + require sumOfBalances >= to_mathint(balance); +} + +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) { + sumOfBalances = sumOfBalances - oldValue + newValue; +} + +invariant totalSupplyIsSumOfBalances() + to_mathint(totalSupply()) == sumOfBalances; diff --git a/fv/specs/helpers/math-cvl.spec b/fv/specs/helpers/math-cvl.spec new file mode 100644 index 00000000000..009d7eee4e3 --- /dev/null +++ b/fv/specs/helpers/math-cvl.spec @@ -0,0 +1,28 @@ +// Closed-form model of Math.mulDiv. Definitions only - no methods block, so this file is safe to +// import anywhere. Activation lives in ERC4626Base.spec. +// +// Adapted from Certora's AutoProver summaries for 512-bit mulDiv. Trusted, not proved: rules that +// rely on it are conditional on this matching Math.mulDiv in both value and revert domain. + +function mulDivDownSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 { + mathint result; + if (denominator == 0) revert(); + result = x * y / denominator; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +function mulDivUpSummary(uint256 x, uint256 y, uint256 denominator) returns uint256 { + mathint result; + if (denominator == 0) revert(); + result = (x * y + denominator - 1) / denominator; + if (result >= 2^256) revert(); + return assert_uint256(result); +} + +/// Mirrors Math.unsignedRoundsUp over Math.Rounding { Floor, Ceil, Trunc, Expand }. +definition roundsUpCVL(Math.Rounding r) returns bool = assert_uint8(r) % 2 == 1; + +function mulDivCVL(uint256 x, uint256 y, uint256 d, Math.Rounding rounding) returns uint256 { + return roundsUpCVL(rounding) ? mulDivUpSummary(x, y, d) : mulDivDownSummary(x, y, d); +}