A guide to smart contract security tools

We are going to use three distinctive testing and program analysis techniques:

• Static analysis with Slither. All the paths of the program are approximated and analyzed at the same time, through different program presentations (e.g., control-flow-graph)
• Fuzzing with Echidna (or Medusa (opens in a new tab), a newer fuzzer from the same team). The code is executed with a pseudo-random generation of transactions. The fuzzer will try to find a sequence of transactions to violate a given property.
• Symbolic execution with hevm (opens in a new tab). A formal verification technique, which translates each execution path to a mathematical formula, on which on top constraints can be checked. hevm can run Foundry tests symbolically, and Echidna uses it for its verification testing mode (opens in a new tab).

Each technique has advantages and pitfalls, and will be useful in specific cases:

* if all the paths are explored without timeout

Slither analyzes contracts within seconds, however, static analysis might lead to false alarms and will be less suitable for complex checks (e.g., arithmetic checks). Run Slither via the CLI for push-button access to built-in detectors or via the API for user-defined checks.

Echidna needs to run for several minutes and will only produce true positives. Echidna checks user-provided security properties, written in Solidity. It might miss bugs since it is based on random exploration.

Symbolic execution with hevm performs the "heaviest weight" analysis. Like Echidna, it checks user-provided properties. It will need more time to run, and complex code can make it time out or return an inconclusive result, but when it completes it can prove the validity of a property and will not report false alarms. The Solidity compiler's built-in SMTChecker (opens in a new tab) is another formal verification option for checking assert statements.

Suggested workflow

Start with Slither's built-in detectors to ensure that no simple bugs are present now or will be introduced later. Use Slither to check properties related to inheritance, variable dependencies, and structural issues. As the codebase grows, use Echidna to test more complex properties of the state machine. Revisit Slither to develop custom checks for protections unavailable from Solidity, like protecting against a function being overridden. Finally, use symbolic execution to perform targeted verification of critical security properties, e.g., arithmetic operations.

• Use Slither's CLI to catch common issues
• Use Echidna to test high-level security properties of your contract
• Use Slither to write custom static checks
• Use hevm once you want in-depth assurance of critical security properties

A note on unit tests. Unit tests are necessary to build high-quality software. However, these techniques are not the best suited to find security flaws. They are typically used to test positive behaviors of code (i.e., the code works as expected in the normal context), while security flaws tend to reside in edge cases that the developers did not consider. In our study of dozens of smart contract security reviews, unit test coverage had no effect on the number or severity of security flaws (opens in a new tab) we found in our client's code.

Determining Security Properties

To effectively test and verify your code, you must identify the areas that need attention. As your resources spent on security are limited, scoping the weak or high-value parts of your codebase is important to optimize your effort. Threat modeling can help. Consider reviewing:

• Rapid Risk Assessments (opens in a new tab) (our preferred approach when time is short)
• Guide to Data-Centric System Threat Modeling (opens in a new tab) (aka NIST 800-154)
• Shostack threat modeling (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• Use of Assertions (opens in a new tab)

Components

Knowing what you want to check will also help you to select the right tool.

The broad areas that are frequently relevant for smart contracts include:

• State machine. Most contracts can be represented as a state machine. Consider checking that (1) No invalid state can be reached, (2) if a state is valid that it can be reached, and (3) no state traps the contract.

  • Echidna (or Medusa) is the tool to favor to test state-machine specifications. hevm can then verify the most critical transitions.

• Access controls. If your system has privileged users (e.g., an owner, controllers, ...) you must ensure that (1) each user can only perform the authorized actions and (2) no user can block actions from a more privileged user.

  • Slither, Echidna and hevm can check for correct access controls. For example, Slither can check that only whitelisted functions lack the onlyOwner modifier. Echidna and hevm are useful for more complex access control, such as a permission given only if the contract reaches a given state.

• Arithmetic operations. Checking the soundness of the arithmetic operations is critical. Since Solidity 0.8.0, arithmetic is checked by default (opens in a new tab) and reverts on overflow/underflow, but you must still review every unchecked block and consider other arithmetic flaws, including rounding issues, precision loss and flaws that trap the contract.

  • Symbolic execution with hevm is the best choice here. Echidna can be used if the arithmetic is out-of-scope of the SMT solver.

• Inheritance correctness. Solidity contracts rely heavily on multiple inheritance. Mistakes such as a shadowing function missing a super call and misinterpreted c3 linearization order can easily be introduced.

  • Slither is the tool to ensure detection of these issues.

• External interactions. Contracts interact with each other, and some external contracts should not be trusted. For example, if your contract relies on external oracles, will it remain secure if half the available oracles are compromised?

  • Echidna and hevm are the best choice for testing external interactions with your contracts. Use mock contracts to stand in for the external contracts you do not trust.

• Standard conformance. Ethereum standards (e.g., ERC20) have a history of flaws in their design. Be aware of the limitations of the standard you are building on.

  • Slither, Echidna, and hevm will help you to detect deviations from a given standard.

Tool selection cheatsheet

Other areas will need to be checked depending on your goals, but these coarse-grained areas of focus are a good start for any smart contract system.

Our public audits contain examples of verified or tested properties. Consider reading the Automated Testing and Verification sections of the following reports to review real-world security properties:

• 0x (opens in a new tab)
• Balancer (opens in a new tab)