Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts

Understand

An effective way to maximize code coverage in software tests is through dynamic symbolic execution$-$a technique that uses constraint solving to systematically explore a program's state space.

• We introduce an open-source dynamic symbolic execution framework called Manticore for analyzing binaries and Ethereum smart contracts.
• Manticore's flexible architecture allows it to support both traditional and exotic execution environments, and its API allows users to customize their analysis.
• Here, we discuss Manticore's architecture and demonstrate the capabilities we have used to find bugs and verify the correctness of code for our commercial clients.