Manticore

Thanks to our external contributors!

- [catenacyber](https://github.com/trailofbits/manticore/commits?author=catenacyber)
- [binaryflesh](https://github.com/trailofbits/manticore/commits?author=binaryflesh)

Major Changes
Executor Refactor ([1385](https://github.com/trailofbits/manticore/pull/1385))
We've completed a major refactor of the core executor that reorganizes Manticore's state machine to be more amenable toward use with the multiprocesssing module. This refactor introduces some small API changes:
* One must explicitly call the `finalize` method to dump test cases from a run
* The `will_start_run` event has been renamed to `will_run`
* The `solver` module requires explicitly accessing the Z3Solver singleton. `from manticore.core.smtlib import solver` becomes:
python
from manticore.core.smtlib.solver import Z3Solver
solver = Z3Solver.instance()

* `manticore.running_states` has been renamed to `manticore._busy_states`
For more information about changes to the state machine, see [the diagram in core/manticore.py](https://github.com/trailofbits/manticore/blob/451965f03a5e0d6766e499bf3246e4796b35638f/manticore/core/manticore.py#L132-L239)

Blacken ([1438](https://github.com/trailofbits/manticore/pull/1438))
We've run the [`black`](https://black.readthedocs.io/en/stable/index.html) autoformatter on the master branch of Manticore, and added a check for compliance to our CI. To ensure your code is properly formatted, run `black -t py36 -l 100 .` in your Manticore directory before committing.

Support for statically-linked AArch64 binaries ([1424](https://github.com/trailofbits/manticore/pull/1424))
Contractor [nkaretnikov](https://github.com/trailofbits/manticore/commits?author=nkaretnikov) spent several months adding support for AArch64 on Linux. As this is a brand new architecture, we've left in most of the debugging assertions, which may slow it down slightly.
We look forward to getting feedback on this architecture so we can eventually remove the debugging assertions.


Ethereum

* Added Symbolic EVM Tests for the Frontier fork. Note that we don't support any other forks (i.e. Constantinople) yet. ([1431](https://github.com/trailofbits/manticore/pull/1431), [#1441](https://github.com/trailofbits/manticore/pull/1441))
* **[fixed API]** Fixed relative paths for .sol files ([1393](https://github.com/trailofbits/manticore/pull/1393))
* **[fixed API]** Support dynamic parameters in constructors ([1414](https://github.com/trailofbits/manticore/pull/1414))
* Fixed detector failure when PC is symbolic ([1395](https://github.com/trailofbits/manticore/pull/1395))
* Transfers from etherless contracts no longer report STOP ([1392](https://github.com/trailofbits/manticore/pull/1392))

Native

* Added stubs for missing system calls & downgraded most missing calls from exceptions to warnings ([1384](https://github.com/trailofbits/manticore/pull/1384))
* Fixed DECREE magic pages ([1413](https://github.com/trailofbits/manticore/pull/1413))
* Store x86 registers in a set instead of a list ([1415](https://github.com/trailofbits/manticore/pull/1415))
* Fix register boundary check for non-x86 architectures ([1429](https://github.com/trailofbits/manticore/pull/1429))
* Support `movhps` on x86 ([1444](https://github.com/trailofbits/manticore/pull/1444))

Other

* Only publish events when there is at least one subscriber ([1388](https://github.com/trailofbits/manticore/pull/1388))
* Added sandshrew example ([1396](https://github.com/trailofbits/manticore/pull/1396))
* Updated Unicorn to track latest master ([1440](https://github.com/trailofbits/manticore/pull/1440))
* **[fixed API]** Now respects coverage file argument ([1442](https://github.com/trailofbits/manticore/pull/1442))

Thanks to our external contributors!

- [werew](https://github.com/trailofbits/manticore/commits?author=werew)
- [NicolaiSoeborg](https://github.com/trailofbits/manticore/commits?author=NicolaiSoeborg)
- [Joool](https://github.com/trailofbits/manticore/commits?author=Joool)

Manticore 0.2.5 added Unicorn preloading for quickly performing concrete emulation of native binaries until a target address is reached. In the EVM engine, apart from some fixes, this release added support for creating contracts from Truffle JSON artifacts (see json_create_contract).

Full changelog below.

Ethereum

* **[added API]** `json_create_contract` - support creating EVM contracts from Truffle JSON artifacts ([1376](https://github.com/trailofbits/manticore/pull/1376))
* **[changed API]** Moved default gas value to config module ([1346](https://github.com/trailofbits/manticore/pull/1346))
* **[fixed API]** Fixed account creation with a code field ([1371](https://github.com/trailofbits/manticore/pull/1371))
* **[fixed API]** Fixed an incorrect attribute in `last_return` ([1341](https://github.com/trailofbits/manticore/pull/1341))
* **[refactor]** Inlined get_possible solutions function as it's only used once ([1372](https://github.com/trailofbits/manticore/pull/1372))
* Fixed `_check_jumpdest` when run with detectors - this bug could lead to not detecting an int overflow due to tainting made by another detector ([1347](https://github.com/trailofbits/manticore/pull/1347))
* Made findings print addresses in hex ([1339](https://github.com/trailofbits/manticore/pull/1339))

Native

* **[added API]** Added Unicorn preloading, for quickly performing concrete emulation until a target address is reached. ([1356](https://github.com/trailofbits/manticore/pull/1356))
* Fixed incorrect return value in `sys_lseek` ([1355](https://github.com/trailofbits/manticore/pull/1355))
* Added check for missing native packages ([1367](https://github.com/trailofbits/manticore/pull/1367))

Other

* **[added API]** Added context managers for the config module, allowing for temporary configurations ([1345](https://github.com/trailofbits/manticore/pull/1345))
* Updated Capstone to 4.0.1 ([1312](https://github.com/trailofbits/manticore/pull/1312))
* Embedded parsetab.py so users no longer need to generate it ([1383](https://github.com/trailofbits/manticore/pull/1383))

Ethereum

* **[added API]** Fixed VerboseTrace plugin ([1305](https://github.com/trailofbits/manticore/pull/1305)) and added VerboseTraceStdout plugin ([#1305](https://github.com/trailofbits/manticore/pull/1305)): those can be used to track EVM execution (`m.regiser_plugin(VerboseTraceStdout())`)
* **[changed API]** Made gas calculation faithfulness configurable: this way, you can choose whether you respect or ignore gas calculations with `--evm.oog <opt>` (see `--help`); also, the gas calculations has been decoupled into its own methods ([1279](https://github.com/trailofbits/manticore/pull/1279))
* **[changed API]** Changed default gas to 3000000 when creating contract ([1332](https://github.com/trailofbits/manticore/pull/1332))
* **[changed API]** Launching manticore from cli will display all registered plugins ([1301](https://github.com/trailofbits/manticore/pull/1301))
* Fixed a bug where it wasn't possible to call contract's function when its name started with an underscore ([1306](https://github.com/trailofbits/manticore/pull/1306))
* Fixed `Transaction.is_human` usage and changed it to a property ([1323](https://github.com/trailofbits/manticore/pull/1323))
* Fixed `make_symbolic_address` not preconstraining the symbolic address to be within all already-known addresses ([1318](https://github.com/trailofbits/manticore/pull/1318))
* Fixed bug where a terminated state became a running one if `m.running_states` or `m.terminated_states` were generated ([1326](https://github.com/trailofbits/manticore/pull/1326))

Native

* **[added API]** Added symbol resolution feature, so it is possible to grab a symbol address by using `m.resolve(symbol)` ([1302](https://github.com/trailofbits/manticore/pull/1302))
* **[changed API]** The `stdin_size` CLI argument has been moved to config constant and so has to be passed using `--native.stdin_size` instead of `--stdin_size` ([1337](https://github.com/trailofbits/manticore/pull/1337))
* Speeded up Armv7 execution a bit ([1313](https://github.com/trailofbits/manticore/pull/1313))
* Fixed `sys_arch_prctl` syscall when wrong `code` value was passed and raise a NotImplementedError instead of asserting for not supported code values ([1319](https://github.com/trailofbits/manticore/pull/1319))

Other

* We speed up Manticore engine by 5-10% via solver optimizations ([1334](https://github.com/trailofbits/manticore/pull/1334))
* **[changed API]** Fixed missing CLI arguments that came from config constants - note that `timeout` has to be passed using `core.timeout` now ([1337](https://github.com/trailofbits/manticore/pull/1337))
* We now explicitly require Python>=3.6 when using CLI or when importing Manticore ([1331](https://github.com/trailofbits/manticore/pull/1331))
* `__main__` now fetches manticore version from installed modules ([1310](https://github.com/trailofbits/manticore/pull/1310))
* Refactored some of the codebase (events [1314](https://github.com/trailofbits/manticore/pull/1314), solver [#1334](https://github.com/trailofbits/manticore/pull/1334), tests [#1308](https://github.com/trailofbits/manticore/pull/1308), py2->py3 [#1307](https://github.com/trailofbits/manticore/pull/1307), state/platform [#1320](https://github.com/trailofbits/manticore/pull/1320), evm stuff [#1329](https://github.com/trailofbits/manticore/pull/1329))
* Some other fixes and minor changes

Thanks to our external contributors!

- [NeatMonster](https://github.com/NeatMonster)
- [evgeniuz](https://github.com/evgeniuz)
- [stephan-tolksdorf](https://github.com/stephan-tolksdorf)
- [yeti-detective](https://github.com/yeti-detective)
- [PetarMI](https://github.com/PetarMI)
- [hidde-jan](https://github.com/hidde-jan)
- [catenacyber](https://github.com/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 <detectors> 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

Thanks to our external contributors!

- [charliecjung](https://github.com/charliecjung)
- [redyoshi49q](https://github.com/redyoshi49q)
- [yeti-detective](https://github.com/yeti-detective)
- [Srinivas11789](https://github.com/srinivas11789)
- [stephan-tolksdorf](https://github.com/stephan-tolksdorf)
- [catenacyber](https://github.com/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](https://github.com/trailofbits/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