Manticore 0.2.3

0.2.3 - 2018-12-11

Thanks to our external contributors!

• NeatMonster
• evgeniuz
• stephan-tolksdorf
• yeti-detective
• PetarMI
• hidde-jan
• catenacyber

Added

• Support for ARM THUMB instructions: ADR, ADDW, SUBW, CBZ, TBB, TBH, STMDA, STMDB
• State.solve_minmax() API for querying a BitVec for its min/max values
• New SMTLIB optimization for simplifying redundant concat/extract combinations; helps reduce expression complexity, and speed up queries
• Ethereum: --txpreconstrain CLI flag. Enabling this avoids sending ether to nonpayable functions, primarily avoiding exploration of uninteresting revert states.
• Research memory model (LazySMemory) allowing for symbolic memory indexing to be handled without concretization (opt in, currently for research only)

Changed

• Linux/binary analysis has been moved to manticore.native, manticore.core.cpu has been moved to manticore.native.cpu. Please update your imports.
• The binary analysis dependencies are now not installed by default. They can be installed with pip install manticore[native]. This is to prevent EVM users from installing binary dependencies.
• The symbolic 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 optional
• Manticore CLI run on a smart contract will now use all detectors by default (detectors can be listed with --list-detectors, excluded with --exclude or --exclude-all)
• Misusing the ManticoreEVM API, for example by using old keyword arguments that are not available since some versions (like ManticoreEVM(verbosity=5)) will now raise an exception instead of not applying the argument at all.

Fixed

• Ethereum: Fixed CLI timeout support
• Numerous EVM correctness fixes for Frontier fork
• Fixed handling of default storage and memory in EVM (reading from previously unused cell will return a zero now)
• ARM THUMB mode, Linux syscall emulation fixes
• Creation of multiple contracts with symbolic arguments (ManticoreEVM.solidity_create_contract with args=None fired more than once failed before)

Removed

• Manticore.evm static method

Manticore 0.2.2

0.2.2 - 2018-10-30

Thanks to our external contributors!

• charliecjung
• redyoshi49q
• yeti-detective
• Srinivas11789
• stephan-tolksdorf
• catenacyber

Added

• New API for generating a testcase only if a certain condition can be true in the state. Useful for conveniently
  checking an invariant in a state, and (ManticoreEVM.generate_testcase(..., only_if=)) generating a testcase if it
  can be violated.
• New 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.
• Emit generated transaction data in human readable format (JSON)
• Warning messages if number of passed arguments to a Solidity function is inconsistent with the number declared
• CLI support for the ReentrancyAdvancedDetector
• Colored CLI output
• Configuration system. Allows configuration options to be specified in a config file. New configurations are available,
  notably including solver parameters such as solver timeout, and memory limits.
• Support for some unimplemented x86 XMM instructions
• Customizable symbolic stdin input buffer size
• Support for Etheno
• RaceConditionDetector that can be used to detect transaction order dependencies bugs

Changed

• Improve the DetectExternalCallAndLeak detector and reduce false positives
• Numerous improvements and changes to the SolidityMetadata API
• Ethereum contract addresses are no longer random, but are deterministically calculated according to the Yellow Paper
• Manticore no longer supports contracts with symbolic addresses creating new contracts. This is a consequence of
  supporting determinstic contrat address calculation. There are plans for reenabling this capability in a future release.

Deprecated

• Several SolidityMetadata APIs: .get_hash(), .functions, .hashes

Fixed

• Numerous fixes and enhancements to the Ethereum ABI implementation
• Better handling of overloaded functions in SolidityMetadata, and other bug fixes
• Fixes for the FilterFunctions plugin
• Fixes for symbolic SHA3 handling
• Many EVM correctness/consensus fixes
• Numerous spelling errors

Manticore 0.2.1.1

0.2.1.1 - 2018-09-01

Manticore has been relicensed to AGPLv3. Please contact us if you're looking for an exception to these terms.

Thanks to our external contributors!

• s0b0lev
• redyoshi49q

Added

• Full suite of Ethereum detectors
  • Selfdestruct (--detect-selfdestruct): Warns if a selfdestruct instruction is reachable by the user
  • External Call (--detect-externalcall): Warns if there is a call to the user, or a user controlled address with ether.
  • Reentrancy (--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).
  • Delegatecall (--detect-delegatecall): Warns if there is a delegatecall to a user controlled address, or to a user controlled function.
  • Environmental Instructions (--detect-env): Warns if certain instructions are used that can be potentially manipulated. Instructions: BLOCKHASH, COINBASE, TIMESTAMP, NUMBER, DIFFICULTY, GASLIMIT, ORIGIN, GASPRICE.
• New Ethereum command line flags
  • --no-testcases: Do not generate testcases for discovered states
  • --txnoether: Do not make the transaction value symbolic in executed transactions
• SMTLIB: Advanced functionality for expression migration. Expressions from arbitrary constraint sets can be mixed to create arbitrary constraints, expressions are transparently migrated from constraint set to another, avoiding SMT naming collisions.

Changed

• Command line interface uses a new reentrancy detector based on detection of user controlled call addresses

Fixed

• Ethereum: Support for overloaded solidity functions
• Ethereum: Significantly improved ability to create symbolic variables and constraints at the global level
• Ethereum: Improved gas support
• State serialization improvements and fixes

Manticore 0.2.0

0.2.0 - 2018-08-10

In 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!

• ianklatzco
• devtty1er
• catenacyber

Added

• Ethereum: More flexibility for Solidity compilation toolchains
• Ethereum: Detectors for unused return value, reentrancy
• Ethereum: Support for Solidity bytesM and bytes types
• Ethereum: Beta API for preconstraining inputs (ManticoreEVM.constrain)
• Improved performance for smtlib module
• Ability to transparently operate on bytearray and symbolic buffer (ArrayProxy) types (e.g: concatenate, slice)

Changed

• Codebase has been entirely ported to Python 3.6+
• Ethereum: ManticoreEVM.make_symbolic_value() can be size adjustable
• Ethereum: Ethereum ABI (manticore.ethereum.ABI) API refactor, including real Solidity prototype parser
• Ethereum: Improved APIs for accessing transaction history
• Ethereum: Significant internal refactor

Fixed

• Linux: Bugs related to handling of closed files
• Ethereum: Handling of symbolic callers/addresses
• Ethereum: Handling of gas handling on CALL instructions
• Various smtlib/expression fixes

Removed

• Support for Python 2
• EVM disassembler/assembler module (EVMAsm) has been removed and separately released as pyevmasm
• Experimental support for Binary Ninja IL emulation

Manticore 0.1.10

0.1.10 - 2018-06-22

Thanks to our external contributors!

• khorben
• catenacyber
• dwhjames
• matiasb
• reaperhulk
• lazzarello

Added

• ARM: New instructions to better support Raspberry Pi binaries (UTXH, UQSUB8)
• Linux: Can use --env and LD_LIBRARY_PATH to specify alternate ELF interpreter locations for dynamic binaries
• Linux: Partial chroot(2) and fork(2) models
• Initial support for NetBSD hosts
• Ethereum: --avoid-constant cli argument to enable heuristics to avoid unnecessary exploration of constant functions

Changed

• Ethereum detectors are now opt-in, via cli flags: --detect-overflow, --detect-invalid, --detect-uninitialized-memory, --detect-uninitialized-storage, --detect-all
• Ethereum: Complete internal refactor.
  • Model memory using smtlib arrays to better support symbolic indexing
  • Numerous internal API improvements
  • Better symbolic gas support
  • More advanced overflow detection heuristics
  • Account names, scripts can assign names to accounts or contracts
  • Better ABI serializer/deserializer for canonical types, supports tuples/structs and recursive dynamic types
  • State list iterations improvements, modifications to state persist
  • Symbolic caller, address, value and data in transactions

Fixed

• Linux: Generate concretized file content for symbolic files
• Linux: Fixes in various syscall models (brk, stat*), and miscellaneous fixes
• Ethereum: Inaccurate transaction history in some cases

Manticore 0.1.9

Thanks to our external contributors!

• khorben
• arunjohnkuruvilla
• cclauss
• dwhjames
• catenacyber
• disconnect3d

Added

• Ethereum: --txnocoverage cli argument to suppress coverage based analysis halting criteria
• Ethereum: Support added for more Solidity features (imports, uint/int types, function types)

Fixed

• Numerous Ethereum ABI fixes
• Linux and x86/64 emulation fixes
• Solver performance issue

Manticore 0.1.8

Thanks to our external contributors!

• khorben
• disconnect3d
• arunjohnkuruvilla
• mroll

Added

• Ethereum: --txaccount cli argument to control caller of transaction
• Ethereum: Per state execution trace files in workspace

Fixed

• Linux: --data cli argument to specify concrete stdin
• Numerous Ethereum fixes and stability improvements
• Fixes for native cpu emulation

Manticore 0.1.7

This release brings EVM, performance, Linux emulation, and API improvements, along with numerous bug fixes. Thanks again to our external contributors!

• jean
• disconnect3d
• arunjohnkuruvilla
• alexanderholman
• Srinivas11789

Added

• Documentation on symbolic input
• "force" keyword argument in cpu.write_bytes/read_bytes etc.
• Linux syscalls: getrandom(), openat()

Fixed

• Improved ARMv7 Thumb support
• Numerous EVM bug fixes and improvements (transaction generation, SHA3 handling, instruction tracing, int overflow detection)
• Improved x86/64 emulation performance

Manticore 0.1.6

This release brings improved Ethereum support, performance improvements, and numerous bug fixes. Thanks to our external contributors!

• cole-lightfighter
• arunjohnkuruvilla
• Srinivas11789
• sidhant-gupta-004
• roachspray
• dbogs425
• HighW4y2H3ll
• chowdaryd

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.