Ethereum Detectors

Manticore includes built-in "detectors" for certain properties of Ethereum smart contracts. Used in this way, Manticore acts like a linter that reports on these conditions as they are observed while exploring the state space of a smart contract. These detectors may or may not apply to the contract being explored, may falsely detect issues, or may fail to report a true issue. These detectors are a default set of properties that we expect most contracts will share. It is always best to reason about the application-specific properties of your contract, and then build analyses to verify them.

List of Ethereum Detectors

All detectors are run by default. Run Manticore with --exclude detector1,detector2 to exclude particular detectors. You can also exclude all of them by running --exclude-all or list them with --list-detectors.

Note that running with detectors increases analysis time (even by 50% or more).

Detector	What it detects
delegatecall	Problematic uses of DELEGATECALL
overflow	Integer overflows
reentrancy	Reentrancy bug
reentrancy-adv	Reentrancy bug (different method)
env-instr	Use of potentially unsafe/manipulable instructions
ext-call-leak	Reachable external call or ether leak to sender or arbitrary address
suicidal	Reachable selfdestruct instructions
uninitialized-memory	Uninitialized memory usage
uninitialized-storage	Uninitialized storage usage
invalid	Enable INVALID instruction detection
unused-return	Unused internal transaction return values

Writing a new detector

The existing detectors are found in detectors.py.