Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts
This provides a user-friendly tool for software testers and security analysts to improve code coverage and bug detection, though it appears incremental as it builds on existing symbolic execution techniques.
The authors tackled the problem of maximizing code coverage in software tests by introducing Manticore, an open-source dynamic symbolic execution framework for analyzing binaries and Ethereum smart contracts, which has been used to find bugs and verify code correctness for commercial clients.
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.