Why would I use Trail of Bits' Manticore over SMTChecker, which is baked in the Solidity compiler?
asked Jul 18, 2020 at 11:34
Add a comment
|
1 Answer
tl;dr: you should use both (and more) :)
Different FV/static analysis tools often have different features and pros/cons which might complement each other and give you better coverage.
In this case, for example, Manticore targets EVM bytecode whereas SMTChecker targets Solidity code.
- Targeting Solidity is better for high level properties, contract invariants and reasoning about state variables directly. The SMTChecker is good at contract invariants, can handle loops and gives counterexamples for properties (bugs) on a readable Solidity level (all automated), but will often fail at proving low level properties, bitwise operations, inline assembly, and low level data manipulation.
- Tools that target EVM bytecode are usually the other way around. I cannot speak for Manticore exactly, but hevm is an example of that pattern. One big feature of tools for EVM bytecode is that they analyze exactly what will be deployed, and therefore do not need to trust the compiler (like the SMTChecker does), but rather verify the compiler's work. One example of that is that EVM bytecode contains ABI encoding/decoding code, which is often verified for specific contracts by these tools. Tools that analyze Solidity don't have that and need to assume that the encoding is correct when a function is entered. In that sense proofs provided by EVM bytecode tools are stronger.
Besides the fundamental symbolic encoding/proof techniques, each tool has their own set of features which might be useful or not for your case. Here's a list of a bunch more tools that I try to keep updated: https://github.com/leonardoalt/ethereum_formal_verification_overview
