Find Highs Before External Auditors Using Invariant Fuzz Testing

Many high severity findings found during private audits by external auditors could have been found by the protocol developers themselves using invariant fuzz testing prior to engaging external auditors. While this doesn’t require developing an “attacker mindset” or other auditor-specific skills, it does require learning to think in invariants which is a useful skill for both protocol developers and smart contract auditors.

Given the fees that “Tier 1” external audit firms charge per week, having the invariant tests done in-house prior to external audit is also more cost-effective. This is especially the case as protocol developers already have full context of important protocol & contract properties so can more rapidly write the invariants.

Thinking In Invariants

The primary skill developers need to acquire is learning to think in invariants. I have previously presented a simple framework for this which:

uses Chimera to write one codebase that works across Echidna, Medusa & Foundry fuzzers while enabling easy cloud fuzzing using Recon
breaks the contract lifecycle into at least 3 phases: construction/initialization, regular functioning and an optional end state
categorizes invariants into 2 basic categories: “black box” which can be gleaned from the protocol design and documentation, and “white box” which are based upon the smart contract’s internal implementation code

Invariants can further be classified into the following types:

Relationships between inter-related storage locations, eg:
- the sum of all values in a mapping X must equal Y stored elsewhere in storage (regular, white box)
- all addresses present in EnumerableSet X must also exist as keys in mapping Y (regular, white box)
Monetary value held by contract/protocol and solvency requirements, eg:
- Once token/reward/yield distribution is complete the contract should have 0 balance (end state, black box)
- contract should always have enough tokens to cover liabilities (regular, black box)
Logical invariants that prevent invalid states, eg:
- account with active borrow can’t exit market where they borrowed from (regular, black box)
- protocol should never enter a state where borrower can be liquidated but can’t repay (regular, black box)
Denial of Service (DoS) from unexpected errors, eg:
- liquidation should never revert with unexpected errors such as access array out of bounds, under/overflow etc (regular, white box)

Handlers Vs No Handlers

Invariant fuzzers can use “handler” functions which wrap underlying functions from the target contract, satisfying preconditions to prevent trivial reverts. Alternatively fuzzers can also use no handlers which lets the fuzzer explore freely. The trade-offs between these choices are:

when using no handlers, if the search space is too large the fuzzer may not have enough time to find invariant-breaking sequences and there may be many wasted runs due to trivial reverts
using handlers eliminates wasted runs due to trivial reverts increasing the fuzz efficiency but also restricts the search space so may miss some invariant-breaking sequences

In general most developers will want to use handlers in order to improve the efficiency of their fuzz runs by satisfying basic preconditions, while being mindful not to overly-constrain the fuzz inputs.

Example 1 - Flash Loan Denial Of Service

Specification: there are 2 contracts Receiver and Lender. Receiver has a function executeFlashLoan that calls Lender::flashLoan to take a flash loan, and the important invariant is that Receiver should always be able to take a flash loan if Lender has sufficient tokens available. Simply from this specification without even looking at the code we could write a (regular, black box) invariant like this:

function invariant_receiver_can_take_flash_loan() public returns (bool result) {
    receiver.executeFlashLoan(10);
    result = true;
}

By examining the implementation of Lender::flashLoan we can write an even more specific (regular, white box) invariant based on the knowledge of how that function works:

function invariant_pool_bal_equal_token_pool_bal() public view returns(bool result) {
    result = pool.poolBalance() == token.balanceOf(address(pool));
}

Generally fuzzers are more easily able to break the second more specific white box invariant and it is harder for them to break the first more generic black box invariant. In this case Foundry, Echidna & Medusa can all break both invariants.

Neither of these invariants took any special auditor-specific skills to write; the protocol developer could easily write such invariants as part of the protocol’s test suite.

While this was not a real codebase as it was taken from Damn Vulnerable DeFi Unstoppable challenge, all of the following simplified examples will be from my private audit findings on real codebases while working with Cyfrin.

Example 2 - Reward Distribution Stuck

Specification: a Proposal contract is deployed by a DAO with some ETH to be distributed if the proposal succeeds:

Proposal is active until voting has finished or the proposal has timed out
While active, eligible voters can vote for or against
if quorum is reached the ETH should be distributed between the for voters
otherwise the ETH should be refunded to the proposal creator

Without even looking at the implementation we can write a black box invariant that covers both the regular functioning and the end state:

function property_proposal_complete_all_rewards_distributed() public returns(bool) {
    uint256 proposalBalance = address(prop).balance;

    // only visible when invariant fails
    emit ProposalBalance(proposalBalance);

    return(
        // either proposal is active and contract balance > 0
        (prop.isActive() && proposalBalance > 0) ||

        // or proposal is not active and contract balance == 0
        (!prop.isActive() && proposalBalance == 0)
    );
}

This invariant uncovered a High severity issue that resulted in tokens being permanently stuck in the contract.

Example 3 - Voting Power Destruction

Specification: a VotingNft contract:

allows users to deposit ETH collateral against their NFT to give it DAO voting power
NFTs can be created by the owner until the “power calculation start time”
Once power calculation begins all NFTs start with max voting power which declines over time for NFTs which have not been backed by deposited ETH
NFT voting power which has declined can never be increased; depositing the required ETH collateral simply prevents any future decrease

Purely from this specification we can write an (initialization, black box) invariant to verify that when power calculation begins, the total voting power of all NFTs is equal to the max voting power multiplied by the number of created NFTs:

function property_total_power_eq_init_max_power_calc_start() public view returns(bool result) {
    result = votingNft.getTotalPower() == initMaxNftPower;
}

This very simple invariant uncovered two serious issues:

a Critical asymmetry vulnerability which a permission-less attacker could exploit to permanently set every NFT’s voting power to 0
a High vulnerability that allowed a permission-less attacker to dramatically lower the total voting power to almost 0 while maintaining individual NFT voting power, massively increasing the voting power of any NFT holder

Example 4 - Token Sale Drain

Specification: a TokenSale contract:

allows a DAO to sell its governance sellToken for another buyToken
the token sale is only for allowed users and each user can only buy up to a max per-user limit to prevent concentration of voting power
in our simplified version we assume an exchange rate of 1:1 and that sellToken always has decimals greater or equal to buyToken

Using only the specification we can create two (regular, black box) invariants. The first invariant verifies that the number of tokens bought matches the number of tokens sold (due to the simplified 1:1 exchange):

function invariant_tokens_bought_eq_tokens_sold() public view returns(bool result) {
    uint256 soldAmount = tokenSale.getSellTokenSoldAmount();
    uint256 boughtBal  = buyToken.balanceOf(address(this));

    // scale up `boughtBal` by the precision difference
    // SELL_DECIMALS >= BUY_DECIMALS
    boughtBal *= 10 ** (SELL_DECIMALS - BUY_DECIMALS);

    result = (boughtBal == soldAmount);
}

The second invariant verifies that a user can only buy up to the maximum sellToken amount allowed per user:

function invariant_max_token_buy_per_user() public view returns(bool result) {
    for(uint256 i; i<buyers.length; ++i) {
        address buyer = buyers[i];

        if(sellToken.balanceOf(buyer) > MAX_TOKENS_PER_BUYER) {
            return false;
        }
    }

    result = true;
}

These two simple invariants uncovered:

a Critical rounding down to zero vulnerability found by my teammate which allowed a user to get free tokens
a High vulnerability which allowed a user to bypass the per-user max buy token limit, buying all the tokens and hence gaining dominant voting power

Example 5 - Vesting Points Increase

Specification: a Vesting contract allocates points to users which can be used to redeem tokens once their vesting period has been served. The contract implements an initialization invariant in the constructor ensuring that all points are allocated:

require(totalPoints == TOTAL_POINTS, "Not enough points");

Users can transfer their points to another address but apart from this users have no way to increase or decrease their allocated points, hence the sum of individual user points should always remain equal to the initial total allocated.

From the specification we can write a (regular, black box) invariant to verify that the sum of all user points always remains equal to the initial total allocated points:

function property_users_points_sum_eq_total_points() public view returns(bool result) {
    uint24 totalPoints;

    // sum up all user points using `recipients` ghost variable
    for(uint256 i; i<recipients.length; i++) {
        (uint24 points, , ) = vesting.allocations(recipients[i]);

        totalPoints += points;
    }

    // true if invariant held, false otherwise
    if(totalPoints == TOTAL_POINTS) result = true;

    // note: Solidity always initializes to default values
    // so no need to explicitly set result = false as false
    // is the default value for bool
}

This invariant exposed a High severity vulnerability which allowed users to give themselves an infinite number of points and hence drain the token allocation.

Example 6 - Vesting Preclaim Abuse

Specification: a VestingExt contract contains the same functionality as the previous Vesting contract plus an additional feature which lets users preclaim part of their token allocation, allowing users to get a limited amount of tokens before their vesting period is served.

Using only the specification we can create a (regular, black box) invariant which verifies the total preclaimed points is always less than or equal to the maximum preclaimable points (which is just the number of users multiplied by the maximum preclaim point amount per user):

function property_total_preclaimed_lt_eq_max_preclaimable() public view returns(bool result) {
    result = totalPreclaimed <= MAX_PRECLAIMABLE;
}

This invariant discovered a Medium severity vulnerability which allowed users to preclaim their entire token allocation and in the case of the code under audit, rapidly gain more voting power in the DAO than they should be able to.

Example 7 - Operator Registry Corruption

Specification: an OperatorRegistry contract allows users to register as operators and receive an operatorId where the first operatorId = 1 and subsequent ids are incremented.

The contract storage has multiple inter-related data structures which use both the user’s address and operatorId as keys in mappings to reference one another, enabling lookup of operator data by either address or operatorId. Users can also update their address.

From this specification we can write a (regular, black box) invariant that verifies the data integrity of these inter-related data structures by ensuring that every operatorId is related to a unique address:

EnumerableSet.AddressSet foundAddresses;

function property_operator_ids_have_unique_addresses() public returns(bool result) {
    // first remove old found from ghost storage
    uint256 oldFoundLength = foundAddresses.length();
    if(oldFoundLength > 0) {
        address[] memory values = foundAddresses.values();

        for(uint256 i; i<oldFoundLength; i++) {
            foundAddresses.remove(values[i]);
        }
    }

    // then iterate over every current operator, fetch its address
    // and attempt to add it to the found set. If the add fails it is
    // a duplicate breaking the invariant
    uint128 numOperators = operatorRegistry.numOperators();
    if(numOperators > 0) {
        // operator ids start at 1
        for(uint128 operatorId = 1; operatorId <= numOperators; operatorId++) {
            if(!foundAddresses.add(operatorRegistry.operatorIdToAddress(operatorId))) {
                return false;
            }
        }
    }

    result = true;
}

This invariant uncovered a Low severity issue found by my teammate where two different operatorIds could point to the same user address & associated data, corrupting the inter-related data structure relationships. This was a Low severity issue in our audit as the function which triggered the corruption was permissioned and the impact was limited but this could easily have Medium or High severity in other codebases depending on how the corruption could be triggered and exploited.

Example 8 - Liquidate Denial Of Service

Specification: a LiquidateDos contract allows traders to enter multiple markets and have one open position in each market. Traders can also be liquidated:

all open positions are accounted when determining if a trader is liquidatable
if liquidated, all open positions are closed for the trader being liquidated
liquidation should never fail with unexpected errors

Using this specification we can write a (regular, white box) invariant that verifies the liquidate function doesn’t revert with unexpected errors. This invariant is white box as it requires us to know the specific implementation details of liquidate in order to know which errors are expected.

When implementing DoS invariant fuzz tests there are two approaches:

run Echidna and Medusa in assertion mode, and have assertions in the fuzz handler - but this won’t work with Foundry
have a bool ghost variable which is set in the fuzz handler then wrap an invariant around it - this works with all 3 fuzzers

Here is the handler and invariant using the second implementation:

// TargetFunctions fuzz handler
function handler_liquidate(uint8 victimIndex) external {
    address victim = _getRandomAddress(victimIndex);

    try liquidateDos.liquidate(victim) {
        // update ghost variables
        delete userActiveMarketsCount[victim];

        for(uint8 marketId = liquidateDos.MIN_MARKET_ID();
            marketId <= liquidateDos.MAX_MARKET_ID();
            marketId++) {
            delete userActiveMarkets[victim][marketId];
        }
    }
    catch(bytes memory err) {
        bytes4[] memory allowedErrors = new bytes4[](2);
        allowedErrors[0] = ILiquidateDos.LiquidationsDisabled.selector;
        allowedErrors[1] = ILiquidateDos.LiquidateUserNotInAnyMarkets.selector;

        if(_isUnexpectedError(bytes4(err), allowedErrors)) {
            liquidateUnexpectedError = true;
        }
    }
}

// returns whether error was unexpected
function _isUnexpectedError(
    bytes4 errorSelector,
    bytes4[] memory allowedErrors
) internal pure returns(bool isUnexpectedError) {
    for (uint256 i; i < allowedErrors.length; i++) {
        if (errorSelector == allowedErrors[i]) {
            return false;
        }
    }

    isUnexpectedError = true;
}

// Properties invariant
function property_liquidate_no_unexpected_error() public view returns(bool result) {
    result = !liquidateUnexpectedError;
}

This invariant uncovered a Critical severity vulnerability which a trader could weaponize to make themselves impossible to liquidate.

Example 9 - Stability Pool Drain

Specification: a StabilityPool contract which:

allows users to deposit debtToken which is used to pay down bad debt during liquidations
in exchange debtToken depositors receive a share of collateralToken rewards from collateral seized during liquidations
contains quite complicated logic to calculate the reward share debtToken depositors should receive
must always remain solvent; the pool should always have sufficient collateralToken to pay out rewards owed to debtToken depositors

A (regular, black box) invariant which naturally flows from the specification is to verify the pool’s solvency:

function property_stability_pool_solvent() public view returns(bool result) {
    uint256 totalClaimableRewards;

    // sum total claimable rewards for each possible user
    for(uint8 i; i<ADDRESS_POOL_LENGTH; i++) {
        address user = addressPool[i];

        totalClaimableRewards += stabilityPool.getDepositorCollateralGain(user);
    }

    // pool is solvent if the total claimable rewards are
    // lte its collateral token balance
    if(totalClaimableRewards <= collateralToken.balanceOf(address(stabilityPool)))
        result = true;
}

This simple invariant uncovered a Critical vulnerability in the original protocol from which the code I was auditing was forked. The vulnerability had been introduced in a “small fix” and laid dormant in the codebase for 1 year; it allowed a debtToken depositor to completely drain all collateralTokens from the StabilityPool.

The simplicity of this invariant serves to illustrate the great power of invariant fuzz testing: without understanding the complicated reward calculation code, we can write a simple black box invariant which the fuzzer will break finding an extremely valuable Critical exploit.

Example 10 - Collateral Priority Corruption

Specification: a Priority contract used in multi-collateral lending protocols:

defines a liquidation priority order for collaterals
when a liquidation occurs, the riskiest collaterals are liquidated first such that the borrower’s remaining collateral basket is more stable post-liquidation
allows collaterals to be added and removed; adding always puts the new collateral at the end of the priority queue while removing preserves the existing order minus the removed element

From the specification we can write a (regular, black box) invariant to verify the collateral order is always correct. To simplify the implementation in our fuzz test we use 4 collaterals, update the expected order in the fuzz handlers then compare the expected order to the actual in the invariant:

// TargetFunctions fuzz handlers update ghost variable expected order
function handler_addCollateral(uint8 collateralId) external {
    collateralId = uint8(between(collateralId,
                                 priority.MIN_COLLATERAL_ID(),
                                 priority.MAX_COLLATERAL_ID()));

    priority.addCollateral(collateralId);

    // update ghost variables with expected order
    if(priority0 == 0) priority0 = collateralId;
    else if(priority1 == 0) priority1 = collateralId;
    else if(priority2 == 0) priority2 = collateralId;
    else priority3 = collateralId;
}

function handler_removeCollateral(uint8 collateralId) external {
    collateralId = uint8(between(collateralId,
                                 priority.MIN_COLLATERAL_ID(),
                                 priority.MAX_COLLATERAL_ID()));

    priority.removeCollateral(collateralId);

    // update ghost variables with expected order
    if(priority0 == collateralId) {
        priority0 = priority1;
        priority1 = priority2;
        priority2 = priority3;
    }
    else if(priority1 == collateralId) {
        priority1 = priority2;
        priority2 = priority3;
    }
    else if(priority2 == collateralId) {
        priority2 = priority3;
    }

    delete priority3;
}

// Properties invariant
function property_priority_order_correct() public view returns(bool result) {
    if(priority0 != 0) {
        if(priority.getCollateralAtPriority(0) != priority0) return false;
    }
    if(priority1 != 0) {
        if(priority.getCollateralAtPriority(1) != priority1) return false;
    }
    if(priority2 != 0) {
        if(priority.getCollateralAtPriority(2) != priority2) return false;
    }
    if(priority3 != 0) {
        if(priority.getCollateralAtPriority(3) != priority3) return false;
    }

    result = true;
}

This invariant uncovered a High vulnerability that corrupted the collateral priority order resulting in incorrect collateral being prioritized for liquidation, which results in traders being left with an unhealthier collateral basket post-liquidation increasing the likelihood of future liquidations.

Conclusion

We have reviewed 9 simplified examples from my private audits on real codebases where invariant fuzz testing could have been used “in-house” by protocol developers to detect and fix important vulnerabilities prior to engaging external auditors.

Only 1 of these invariants was white box meaning that to write it required understanding of smart contract internal implementation details. The other 8 were all black box so could be deduced simply from the protocol or contract specification. All 9 invariants were relatively simple to write and implement.

Protocol developers and smart contract auditors can significantly improve the security of their protocols by learning to think in invariants and implementing invariant fuzz tests as part of their work.

Additional Resources

EVM Fuzzing Resources

Find Highs Before External Auditors Using Invariant Fuzz Testing

Comments (2)

Deep Dives

Writing Multi-Fuzzer Invariant Tests Using Chimera

More from this blog

Using Claude To Evolve Specialist AI Smart Contract Auditors

The Yieldoor Gas Optimizoor

DeFi Liquidation Vulnerabilities

Find Highs Before External Auditors Using Certora Formal Verification

Thinking In Invariants

Handlers Vs No Handlers

Example 1 - Flash Loan Denial Of Service

Example 2 - Reward Distribution Stuck

Example 3 - Voting Power Destruction

Example 4 - Token Sale Drain

Example 5 - Vesting Points Increase

Example 6 - Vesting Preclaim Abuse

Example 7 - Operator Registry Corruption

Example 8 - Liquidate Denial Of Service

Example 9 - Stability Pool Drain

Example 10 - Collateral Priority Corruption

Conclusion

Additional Resources

Command Palette

Comments (2)

Deep Dives

Writing Multi-Fuzzer Invariant Tests Using Chimera

More from this blog

Thinking In Invariants

Handlers Vs No Handlers

Example 1 - Flash Loan Denial Of Service

Example 2 - Reward Distribution Stuck

Example 3 - Voting Power Destruction

Example 4 - Token Sale Drain

Example 5 - Vesting Points Increase

Example 6 - Vesting Preclaim Abuse

Example 7 - Operator Registry Corruption

Example 8 - Liquidate Denial Of Service

Example 9 - Stability Pool Drain

Example 10 - Collateral Priority Corruption

Conclusion

Additional Resources