Symbolic execution tool
Thanks to our external contributors!
State.solve_minmax()
API for querying a BitVec for its min/max values--txpreconstrain
CLI flag. Enabling this avoids sending ether to nonpayable functions, primarily avoiding exploration of uninteresting revert states.manticore.native
, manticore.core.cpu
has been moved to manticore.native.cpu
. Please update your imports.pip install manticore[native]
. This is to prevent EVM users from installing binary dependencies.stdin_size
is now a config variable (in main
config group) with a default of 256 (it was like this before).ManticoreEVM.generate_testcase()
'name' parameter is now optionalManticore.evm
static methodThanks to our external contributors!
ManticoreEVM.generate_testcase(..., only_if=)
) generating a testcase if it
can be violated.constrain=
optional parameter for State.solve_one
and State.solve_buffer
. After solving for a symbolic variable,
mutate the state by applying that solution as a constraint. Useful if concretizing a few symbolic variables, and later
concretizations should take into account previously solved for values.ManticoreEVM.human_transactions
top level API. Mirrors ManticoreEVM.transactions
, but does not contain any internal
transactions.RaceConditionDetector
that can be used to detect transaction order dependencies bugs.get_hash()
, .functions
, .hashes
Manticore has been relicensed to AGPLv3. Please contact us if you're looking for an exception to these terms.
Thanks to our external contributors!
--detect-selfdestruct
): Warns if a selfdestruct instruction is reachable by the user--detect-externalcall
): Warns if there is a call to the user, or a user controlled address with ether.--detect-reentrancy
): Warns if there is a change of storage state after a call to the user, or a user controlled address, with >2300 gas. This is an alternate implementation enabled in the CLI. The previous implementation is still available for API use (DetectReentrancyAdvanced
).--detect-delegatecall
): Warns if there is a delegatecall to a user controlled address, or to a user controlled function.--detect-env
): Warns if certain instructions are used that can be potentially manipulated. Instructions: BLOCKHASH, COINBASE, TIMESTAMP, NUMBER, DIFFICULTY, GASLIMIT, ORIGIN, GASPRICE.--no-testcases
: Do not generate testcases for discovered states--txnoether
: Do not make the transaction value symbolic in executed transactionsIn this release, the codebase has been ported to Python 3.6, which is a breaking change for API clients. Beginning with 0.2.0, client programs of Manticore must be compatible with Python 3.6.
Thanks to our external contributors!
bytesM
and bytes
typesManticoreEVM.constrain
)ManticoreEVM.make_symbolic_value()
can be size adjustablemanticore.ethereum.ABI
) API refactor, including real Solidity prototype parserThanks to our external contributors!
--env
and LD_LIBRARY_PATH
to specify alternate ELF interpreter locations for dynamic binaries--avoid-constant
cli argument to enable heuristics to avoid unnecessary exploration of constant functions--detect-overflow
, --detect-invalid
, --detect-uninitialized-memory
, --detect-uninitialized-storage
, --detect-all
Thanks to our external contributors!
--txnocoverage
cli argument to suppress coverage based analysis halting criteriaThanks to our external contributors!
--txaccount
cli argument to control caller of transaction--data
cli argument to specify concrete stdinThis release brings EVM, performance, Linux emulation, and API improvements, along with numerous bug fixes. Thanks again to our external contributors!
cpu.write_bytes/read_bytes
etc.This release brings improved Ethereum support, performance improvements, and numerous bug fixes. Thanks to our external contributors!
A few comments on Ethereum support:
Manticore includes an implementation of a symbolic Ethereum Virtual Machine (EVM), an EVM disassembler/assembler, and a convenient interface for automated compilation and analysis of Solidity. It also integrates with Ethersplay, Trail of Bits’ visual disassembler for EVM bytecode, for analysis visualization. As with binaries, Manticore offers a simple command line interface and a Python API for analysis of EVM bytecode. See a demo: https://asciinema.org/a/154012
EVM features in Manticore are under active development and bounties are available for feature enhancements and bugfixes. Join us on the Empire Hacking Slack in #ethereum to discuss using or hacking on these EVM features with the developers.