Certora-GMX Formal Verification
Findings & Analysis Report

2024-02-13

Table of contents

Overview

About C4

Code4rena (C4) is an open organization consisting of security researchers, auditors, developers, and individuals with domain expertise in smart contracts.

A C4 formal verification competition is an event in partnership with Certora in which community participants, referred to as Wardens, use formal verification tools to mathematically prove the correctness of a program or system in exhange for a bounty provided by sponsoring projects.

During the formal verification competition outlined in this document, Wardens utilized the Certora Prover (verification tool) to conduct formal verification of the GMX smart contract system. The formal verification competition took place between August 7—August 28 2023.

Wardens

39 Wardens contributed reports to the GMX Formal Verification competition:

  1. neumo
  2. 0xpoolboy
  3. alexzoid
  4. jokr
  5. twicek
  6. PPrieditis
  7. dev1644
  8. fyang1024
  9. zapaz
  10. Junnon
  11. gumgumzum
  12. Kenshin
  13. alexxander
  14. BenRai
  15. OrbitalWarden
  16. 0xmichalis
  17. n33k
  18. vittdav
  19. 0xrex
  20. peritoflores
  21. Nikki
  22. 7ashraf
  23. jessicapointing
  24. 0xlemon
  25. sh1v
  26. jrcarlos2000
  27. yjrwkk
  28. merlin
  29. sashik_eth
  30. carrotsmuggler
  31. 0xvj
  32. topmark
  33. Kral01
  34. vipe0x
  35. specenforcer
  36. shirochan
  37. Sentry0x
  38. hack3r-0m
  39. ex9

This competition was judged by Certora.

Final report assembled by Certora and liveactionllama.

Summary

Mutations were used to evaluate the quality of the specification. The mutants are described below and are available here. Additionally, the top specifications have been added to the C4 competition repo and some specific properties have been included in this report as good examples. The final results for all participants can be found here.

Mutations

Bank

Bank1.sol: Transfer out no longer reverts when receiver == address(this).

DataStore

DataStore1.sol: Input validation for applyDeltaToUint removed.

DataStore2.sol: Input validation for applyDeltaToUint mutated.

DataStore3.sol: setInt ignores input variable value and sets specified int to 1 instead.

DataStore4.sol: applyDeltaToInt ignores calculated variable nextInt and sets int value to 2.

DataStoreBug0.sol: Memory variable definition hardcoded instead of using input variable.

DataStoreBug1.sol: setAddress sets the wrong address.

DataStoreBug1Participation.sol: Input validation for applyDeltaToUint mutated.

Oracle

Oracle1.sol: Sorting validation’s boolean operator mutated in _validatePrices.

Oracle2.sol: Timestamp validation in _getPriceFeedPrice mutated.

OracleBug2Participation.sol: < changed to <= when checking prices in _getPriceFeedPrice.

OracleBug3.sol: Clear price of token at index 0 instead of looping in clearAllPrices.

OracleBug4.sol: Remove onlyController modifier from setPrices.

OracleBug5.sol: Change > to >= when checking stablePrice in _setPricesFromPriceFeeds.

OracleBug6.so: Change boolean operators during return value calculation in _setPricesFromPriceFeeds.

OracleBug7.sol: Remove call to validateUniqueAndSetIndex from _getSigners.

OracleStore

OracleStore1.sol: Don’t add signers in addSigner.

OracleStore2.sol: Delete event setup in removeSigner.

RoleStore

RoleStore1.sol: Make onlyRoleAdmin always revert.

RoleStore2.sol: Always grant ROUTER_PLUGIN role in grantRole.

RoleStore3.sol: Remove role removal from _revokeRole.

RoleStore4.sol: Mutate revert check to check for CONTROLLER role instead of ROLE_ADMIN.

RoleStore5.sol: Mutate revert check to check for TIMELOCK_ADMIN role instead of TIMELOCK_MULTISIG.

StrictBank

StrictBank1.sol: Remove functionality from syncTokenBalance.

StrictBank2.sol: Remove functionality from _recordTransferIn.

StrictBank3.sol: Modify functionality in _afterTransferOut.

StrictBankBug0Participation.sol: Replace = with += in syncTokenBalance.

StrictBankBug2.sol: Make _recordTransferIn always return 0.

Notable Properties

DataStore

Only CONTROLLER can modify state

Author: alexzoid

rule onlyControllerCouldModifyState(env e, method f, calldataarg args) {

    bool isController = hasRoleControllerHarness(e.msg.sender);

    storage before = lastStorage;

    f(e, args);

    storage after = lastStorage;

    assert(before[currentContract] != after[currentContract] => isController);
}

Oracle

Any token with non-zero price must be contained in tokensWithPrices

Author: 0xpoolboy

invariant tokensWithPricesIsUpToDate(address token)
    getPrimaryPricesMin(token) != 0 => tokenWithPricesContains(token)
    {
        preserved {
            requireInvariant tokensWithPricesSetInvariant;
        }
    }

Only CONTROLLER could modify state

Author: alexzoid

rule onlyControllerCouldModifyState(env e, method f, calldataarg args) filtered {
    f -> !PURE_VIEW_FUNCTIONS(f) && !HARNESS_FUNCTIONS(f)
} {
    bool isController = hasRoleControllerHarness(e.msg.sender);

    storage before = lastStorage;

    f(e, args);

    storage after = lastStorage;

    assert(before[currentContract] != after[currentContract] => isController);
}

Minimum primary price must be less than or equal than max price after any function call except setPrimaryPrice

Author: neumo

rule minAlwaysLTEMax(method f) filtered {
    f -> notHarnessCall(f) &&
    f.selector != sig:setPrimaryPrice(address, Price.Props).selector
} {

    address token;
    uint256 minPre;
    uint256 maxPre;
    uint256 minPost;
    uint256 maxPost;

    env e;
    calldataarg args;

    minPre, maxPre = primaryPrices(e, token);

    currentContract.f(e, args);

    minPost, maxPost = primaryPrices(e, token);

    assert (minPost != minPre || maxPost != maxPre) => maxPost >= minPost;
}

RoleStore

Any users with a role (marked in roleCache) must be included in roleMembers for the relevant role

Author: 0xpoolboy

invariant roleCacheUpToDate(address account, bytes32 roleKey)
    hasRole(account, roleKey) <=> hasRoleFromRoleMembers(account, roleKey)
    {
        preserved {
            requireInvariant roleMembersInvariant();
        }
    }

If anyone owns a role, that role is contained in EnumerableSet.Bytes32Set roles

Author: 0xpoolboy

invariant validRoles(address account, bytes32 roleKey)
    hasRole(account, roleKey) => isRoleKey(roleKey);

There must be at least one ROLE_ADMIN

Author: 0xpoolboy

invariant ThereMustBeAtLeastOneRoleAdmin()
    getRoleMemberCount(ROLE_ADMIN()) > 0;

StrictBank

The WNT address is the only one that can send ether to the contract

Author: neumo

rule balanceCanOnlyIncreaseIfCallerIsWnt(method f) filtered {
    f -> notHarnessCall(f)
} {

    env e;

    address wnt = getWntAddress(e);
    uint256 balancePre = getETHBalance(e, currentContract);

    calldataarg args;
    f(e, args);

    uint256 balancePost = getETHBalance(e, currentContract);

    assert balancePost > balancePre => e.msg.sender == wnt;
}

recordTransferIn must update token balances

Author: alexzoid

invariant recordTransferInTokenBalanceGreater(address token) 
    ghostTokenBalances[token] >= ghostTokenBalancesPrev[token] 
    filtered {
    f -> f.selector == sig:recordTransferIn(address).selector 
    }

Disclosures

C4 is an open organization governed by participants in the community.

C4 Competitions incentivize the discovery of exploits, vulnerabilities, and bugs in smart contracts. Security researchers are rewarded at an increasing rate for finding higher-risk issues. Competition submissions are judged by a knowledgeable security researcher and solidity developer and disclosed to sponsoring developers.

C4 does not provide any guarantee or warranty regarding the security of this project. All smart contract software should be used at the sole risk and responsibility of users.