一場稽核實際怎麼做：工具、測試與威脅建模

// Invariants for a yield vault — properties that must hold after ANY call.
// These are claims; the rest of the audit is an attempt to break them.

// 1. Conservation: shares are only created/destroyed by deposit/withdraw
//      sum(balanceOf[user] for all users) == totalSupply

// 2. Solvency: the vault always physically holds what it owes depositors
//      asset.balanceOf(vault) >= totalDeposited

// 3. Access: only the timelocked admin can pause or change parameters
//      msg.sender == admin  for setFee(), pause(), upgrade()

// 4. Monotonic share price: pricePerShare never decreases
//      except inside a documented, bounded loss event

// 5. No free money: every token leaving the vault is matched by an
//      equal-value token entering, within rounding tolerance

$ slither src/Vault.sol

Reentrancy in Vault.withdraw(uint256) (src/Vault.sol#42-51):
    External calls:
    - (sent,) = msg.sender.call{value: amount}("")  (src/Vault.sol#47)
    State variables written after the call:
    - balances[msg.sender] = 0  (src/Vault.sol#49)   <-- effect AFTER interaction
    Reference: https://github.com/crytic/slither/wiki/Detector-Documentation#reentrancy

Vault.owner (src/Vault.sol#11) is never initialized — defaults to address(0).

INFO:Slither:src/Vault.sol analyzed (1 contract), 2 results found

// Foundry invariant test. forge throws random call sequences at the
// vault (via the Handler) and asserts solvency after every single step.
contract VaultInvariants is StdInvariant, Test {
    Vault   vault;
    Handler handler;        // wraps deposit/withdraw with bounded inputs

    function setUp() public {
        vault   = new Vault(asset);
        handler = new Handler(vault);
        targetContract(address(handler));   // fuzz only through the handler
    }

    // INVARIANT #2: the vault can never owe more than it holds.
    function invariant_neverInsolvent() public view {
        assertGe(asset.balanceOf(address(vault)), vault.totalDeposited());
    }
}

// Echidna (Trail of Bits) writes properties IN Solidity. Any function
// prefixed echidna_ must return true no matter what the fuzzer calls.
contract TokenProps is MyToken {
    // INVARIANT #1: total supply always equals the sum of all balances.
    function echidna_supply_equals_balances() public view returns (bool) {
        return totalSupply() == _sumOfTrackedBalances();
    }
}
// $ echidna test/TokenProps.sol --contract TokenProps
// echidna_supply_equals_balances: PASSED  (50000 calls, 0 failures)

// Certora CVL-style rule (illustrative): prove the solvency invariant
// holds after EVERY public method, for ALL inputs, with no counterexample.
rule neverInsolvent(method f) {
    // assume the invariant holds before the call
    require asset.balanceOf(currentContract) >= totalDeposited();

    env e; calldataarg args;
    f(e, args);                         // f = any function, args = any inputs

    // require it still holds afterward — the prover tries to falsify this
    assert asset.balanceOf(currentContract) >= totalDeposited();
}

[H-01] First-depositor inflation attack lets an attacker steal later deposits

Severity : High  (Impact: High — theft of user funds; Likelihood: Medium)
Target   : Vault.deposit() / convertToShares()   (commit a1b2c3d)

Description
  shares = assets * totalSupply / totalAssets.  When the pool is empty
  (totalSupply == 0) the first depositor mints 1 wei of shares, then sends
  a large amount of the underlying DIRECTLY to the vault (a donation that
  mints no shares). This inflates totalAssets, so the next depositor's
  shares = assets * 1 / totalAssets rounds DOWN to 0 — their assets are
  captured by the attacker's single share.

Proof of concept
  1. attacker.deposit(1 wei)        -> mints 1 share,  totalSupply = 1
  2. asset.transfer(vault, 10e18)   -> donation, no shares minted
  3. victim.deposit(5e18)           -> 5e18 * 1 / (10e18 + 1) = 0 shares
  4. attacker.redeem(1 share)       -> withdraws 15e18 + 1  (victim robbed)

Recommendation
  Use OpenZeppelin ERC4626's decimal-offset / virtual shares, OR seed the
  pool with a permanent dead-shares deposit at deployment, AND revert on
  zero-share mints:  require(shares > 0, "ZERO_SHARES");