Announcing Manticore 0.3.0

Earlier this week, Manticore leapt forward to version 0.3.0. Advances for our symbolic execution engine now include: “fast forwarding” through concrete execution that you don’t care about, support for Linux binaries statically compiled for AArch64, and an interface for selectively solving for interesting test cases. We’ve been working really hard on these and other features over the past quarter, and we’re excited to share what we’ve built.

Executor Refactor

Felipe Manzano completed a major refactor of Manticore’s state machine. It now uses the multiprocessing module, which could make it easier one day to implement distributed symbolic execution. You can read more details about the state machine in the pull request description. Be advised that it does introduce a few small changes to the API, the most important of which are:

• You must now explicitly call the finalize method in order to dump test cases after a run. That means that you can inspect a state before deciding whether to invest the time to solve for a test case.
• The will_start_run callback has been renamed to will_run
• The solver singleton must now be accessed explicitly as Z3Solver.instance()

Unicorn Preloading

Manticore models native instructions in Python, a language that is not known for speed. Instruction throughput is only a tiny fraction of what you’d expect on a concrete CPU, which can be really unfortunate when the code you care about is buried deep within a binary. You might spend several minutes waiting for Manticore to execute a complicated initialization routine before it ever reaches anything of interest.

To handle cases like this, we’ve added a Unicorn emulator plugin that allows Manticore to “fast forward” through concrete execution that you don’t care about. Unicorn is a fast native CPU emulator that leverages QEMU’s JIT engine for better performance. By replacing Manticore’s executor with Unicorn for unimportant initialization routines, we’ve encountered speed improvements of up to 50x. See an example of how to invoke the Unicorn emulator on the pull request.

AArch64 Support

Over the past four months, Nikita Karetnikov added support for Linux binaries statically compiled for AArch64. Since it’s a brand-new architecture, we’ve left in many of the debugging components in order to help us diagnose issues, a decision that may make it a bit slower than other architectures. With the growing popularity of ARMv8 CPUs for platforms ranging from embedded development boards to server farms, we look forward to receiving feedback on this new architecture.

System Call Audit

To provide an accurate symbolic execution environment, Manticore needs symbolic models of all the Linux system calls. Previously, we implemented only a subset of the most common system calls, and Manticore would throw an exception as soon as it encountered an unimplemented call. This is enough to execute many binaries, but there’s room for improvement.

With the 0.3.0 release, we’ve added a dozen new system calls, and added “stubs” to account for the ones we haven’t implemented. Now, instead of throwing an exception when it encounters an unimplemented call, Manticore will attempt to pretend that the call completed successfully. The program may still break afterwards, but we’ve found that this technique is often “good enough” to analyze a variety of problematic binaries. Just be sure to keep your eyes peeled for the “Unimplemented system call” warning message, since further analysis may be unsound if Manticore has ignored an important syscall!

Symbolic EVM Tests

One of the important guarantees that Manticore provides is that when it executes a transaction with a symbol, the result holds for all possible values of that symbol. In order for this to be trustworthy, the symbolic implementation of each instruction needs to be correct. That’s why we’ve extended our continuous integration pipeline to automatically run Manticore against the Frontier version of the Ethereum VM tests on each new commit. This will ensure that throughout further development, you’ll always be able to rely on Manticore to correctly reason about your code.

Black

We believe in clean code, which is why we’ve run Manticore through the black autoformatter. Black deterministically formats your code according to a fairly strict reading of the pycodestyle conventions so that you can focus on the content instead of the formatting. From now on, you should run black -t py36 -l 100 . on your branch before submitting a pull request.

What’s Next?

We believe that security tools are only beneficial if people actually use them, so we want to make Manticore easier for everyone to use. Over the next few months, we have big plans for Manticore’s usability, including improvements to our documentation, updating our examples repository, and conducting a formal usability study. Don’t think we’ll let the code languish, though! Our next release should include support for crytic-compile, making it even easier to analyze smart contracts in Manticore. We’ll continue working towards improved performance and eventual support for EVM Constantinople.

You can download Manticore 0.3.0 from our GitHub, via PyPI, or as a pre-built Docker container.