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

No detectors are run by default. Run Manticore with --detect-all to enable all detectors.

These analyses default to off because each detector will increase the number of solver queries conducted. Enabling all detectors can increase analysis time by 50% or more.

Detector	Description
--detect-overflow	Integer overflows
--detect-invalid	INVALID instructions
--detect-uninitialized-memory	Use of uninitialized memory
--detect-uninitialized-storage	Use of uninitialized storage
--detect-reentrancy	Re-entrancy
--detect-reentrancy-advanced	Re-entrancy (best used by API, not CLI)
--detect-unused-retval	Unused internal transaction return value
--detect-delegatecall	Problematic use of DELEGATECALL
--detect-selfdestruct	Reachable SELFDESTRUCT instructions
--detect-externalcall	Reachable external call or ether leak to sender or arbitrary address
--detect-env-instr	Use of potentially unsafe or manipulable instructions
--detect-race-condition	Transaction race conditions (transaction order dependence)