Symbolic execution is one of the major frontiers of software security research. Academics have demonstrated its theoretical value for years.
But until now, anyone who wanted to use a symbolic execution tool needed domain expertise about the tool’s internals first. What’s more, these tools just started from the beginning of the program; there was no way to focus in on interesting areas of code.
We thought that wasted security researchers’ time and made the power of symbolic execution inaccessible. So we created Manticore, a simple, open-source dynamic binary analysis tool that takes advantage of symbolic execution. It’s pure Python with minimal dependencies that can operate on x86, x64, and ARM binaries and Ethereum smart contracts. We have developed and integrated customized versions into our clients’ unique environments.
After completing the core tool, we created an expressive and scriptable Python API for custom analyses and application-specific optimizations. Anyone with experience in exploitation or reversing can use the API to create specialized binary analysis tools, and answer a range of questions, such as:
- “What is a program input that will cause execution of this code?”
- “Can the program reach code X at runtime?”
- “At point X in execution, is it possible for variable Y to be a specified value?”
- “Is user input ever used as a parameter to libc function X?”
- “How many times does the program execute function X?”
- “How many instructions does the program execute if given input X?”
Parts of Manticore underpinned our symbolic execution capabilities in the Cyber Grand Challenge.
Bridge the gap between academic theory and your current security research. Start using Manticore now, or commission us to port it to another architecture that you use.