solmate-invariants

This repository contains over 100 invariants implemented in medusa during a workshop held by TrailOfBits. More information about the workshop can be found here.

The goal was to find injected bugs in following three contracts, which are adapted directly from solmate:

• ERC20Burn - A standard ERC-20 token with burn functionality.
• FixedPointMathLib - Arithmetic library with operations for fixed-point numbers.
• SignedWadMath - Signed integer 18 decimal fixed point arithmetic library.

The invariants for each contract are defined in separate test files:

• ERC20Test.sol
• FixedPointMathLibTest.sol
• SignedWadMathTest.sol

Running medusa

First, follow the instructions stated here to setup medusa and solc.

To start fuzzing, run the following command:

medusa fuzz --target tests/submission.sol --deployment-order ERC20Test,FixedPointMathLibTest,SignedWadMathTest

Finding a bug in solmate

During the workshop, an edge case was discovered in the wadMul() function of solmate's SignedWadMath library. Specific details of the bug can be found here.

The invariant that found the bug is in SolmateBugTest.sol. To run the test, use the following command:

medusa fuzz --target tests/SolmateBugTest.sol  --deployment-order SolmateBugTest

medusa will instantly flag out an example where the invariant is violated.

References

Some useful references while writing invariants:

• Pre-built properties by TrailOfBits
• WETH invariant testing by @horsefacts