Source-linked AI summary
Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts
Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, Artem Dinaburg
TL;DR
Dynamic symbolic execution can systematically explore program states, but adoption is limited by inflexible, user-unfriendly tools and traditional execution assumptions. Manticore provides an open-source, customizable framework for binaries and Ethereum smart contracts, achieving comparable binary performance and approximately 66% average smart-contract coverage.
Problem
Industry adoption of symbolic execution is limited by scarce user-friendly tools and frameworks tightly coupled to traditional execution models.
Method
Manticore combines a platform-agnostic Core Engine with execution modules, command-line interfaces, and an API for customized binary and smart-contract analyses.
Results
Manticore performs comparably to standard tools for regular binaries and achieves 66% average code coverage with default smart-contract analysis.
Takeaways & Limitations
Manticore provides a flexible, open-source framework for testing programs and conducting symbolic-execution research across traditional and alternative platforms.
Abstract
from arXiv · showhide
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.
I. INTRODUCTION
Manticore addresses limited adoption and inflexible execution assumptions by providing a user-friendly symbolic execution framework spanning binaries and smart contracts.
- Dynamic symbolic execution explores program state spaces and generates inputs satisfying path constraints, producing reproducible identified violations.
- Existing tools’ limited flexibility hindered industry adoption and made alternative environments such as Ethereum difficult to support.
- Manticore analyzes both binaries and smart contracts as a symbolic execution framework.
- Manticore’s architecture supports traditional environments and exotic platforms such as Ethereum.
- Its architecture includes a Core Engine, Native and Ethereum Execution Modules, SMT-LIB module, Event System, and API.
A. Core Engine
The Core Engine provides a platform-agnostic execution layer that manages program states through a defined lifecycle and supports customizable exploration policies and parallel processing.
- Core Engine: The Core Engine implements a generic symbolic execution engine that makes few assumptions about the underlying execution model.
- State management: Program states expose an execution interface, allowing the engine to invoke one atomic execution unit and handle lifecycle events.
- State Life Cycle: States cycle among Ready, Busy, and Terminated through execution, termination, and concretization events.
- State Life Cycle: Concretization converts symbolic objects into constrained concrete values, creating a Ready child state for each value; forking commonly occurs on symbolic program counters.
- Exploration: Exploration policies customize Ready-state selection and concretization, while the engine supports multiple processes for state-queue processing.
B. Native Execution Module
The Native Execution Module abstracts hardware and operating-system behavior so the Core Engine can symbolically execute supported binary environments.
- The module implements the Core Engine’s execution interface through symbolic emulation of the CPU, memory, and operating-system interfaces.
- Its CPU emulator follows ISA specifications directly and represents concrete and symbolic computations with expression trees.
- The virtual address space supports memory operations and alternative symbolic-memory policies, including fully symbolic and concretized models.
3) Operating System Emulation:
Manticore models operating-system and Ethereum execution environments, using concrete system-call forwarding for binaries and symbolic transactions for contract exploration.
- Operating System Emulation: The operating-system emulation supports Linux and DECREE interfaces, including syscalls, process address spaces, and binary loading.
- Operating System Emulation: Because few syscalls can be modeled symbolically, Manticore concretizes syscall arguments and forwards calls to the real operating system.
- Ethereum Execution: Smart contracts run on the Ethereum Virtual Machine and differ from traditional execution through features including gas costs and persistent memory.
- Ethereum Execution: Contracts receive transactions containing a value and data buffer that identifies the function and supplies its arguments.
- Ethereum Execution: Symbolic transactions apply symbolic values and data to Ready states, enabling repeated transaction execution to explore contract state spaces.
- Ethereum Execution: The emulated Ethereum environment tracks complete worlds with interacting contracts and supports symbolic indexing and SHA3 execution.
D. Auxiliary Modules
Manticore’s auxiliary modules separate solver interaction from instrumentation, enabling interchangeable solvers and modular event-based analyses.
- D. Auxiliary Modules: The SMT-LIB module provides symbolic expressions and a solver interface, allowing different solvers to be exchanged seamlessly.Manticore communicates with solvers through the SMT-LIB language.
- D. Auxiliary Modules: The Event System broadcasts symbolic execution events to external subscribers such as API clients.Events include memory accesses, state forking, and concretization, supporting modular plugins.
III. USAGE
Manticore offers command-line and Python interfaces for configuring symbolic inputs, inspecting execution states, generating reproducible tests, and customizing analyses. Its binary evaluation shows performance close to angr, including three additional solved logic bombs, while DeepState integration helps where angr failed.
- III. USAGE: Manticore’s command-line interface accepts symbolic and concrete arguments, prefixes stdin with concrete bytes, and allocates analysis resources.The output directory contains generated inputs and information about discovered states.
- III. USAGE: Generated stdin files can be piped into the program to trigger their corresponding concrete execution states.This connects symbolic exploration outputs to concrete reproduction.
- III. USAGE: The Python API supports callbacks at selected addresses, with access to and control over registers, memory, and operating-system state.Users can read, write, symbolize, or concretize emulated state through hooks.
- III. USAGE: 63 logic bombs were evaluated under a 300-second timeout against angr, Triton, and KLEE.The suite covers symbolic-reasoning and path-explosion challenges.
- III. USAGE: Manticore performed almost as effectively as angr and solved three logic bombs that angr could not handle.Triton and KLEE performed relatively poorly on this benchmark; Manticore lacks some IEEE 754 floating-point support.
- III. USAGE: Manticore is fully integrated into DeepState, where it proved useful in cases where angr failed to produce useful results.The passage reports this outcome in the context of parameterized unit testing.
V. ETHEREUM SMART CONTRACT ANALYSIS EVALUATION
Manticore was evaluated on 100 Ethereum contracts by repeatedly executing symbolic transactions and tracking discovered states and code coverage. Coverage averaged 65.64%, with results spanning 0% to 100%, while four contracts failed during account creation because of incorrect world-state assumptions.
- V. ETHEREUM SMART CONTRACT ANALYSIS EVALUATION: 100 Ethereum smart contracts were analyzed by repeatedly executing symbolic transactions and tracking discovered states and code coverage.The contracts came directly from the Ethereum blockchain.
- V. ETHEREUM SMART CONTRACT ANALYSIS EVALUATION: 65.64% average code coverage was achieved, with an approximately equal median and a range from 0% to 100%.The evaluation used a 90-minute timeout per contract.
- V. ETHEREUM SMART CONTRACT ANALYSIS EVALUATION: 207.71 was the mean total number of symbolic states reached, compared with a median of 52.The difference indicates outliers where substantially more states were discovered.
- V. ETHEREUM SMART CONTRACT ANALYSIS EVALUATION: Four contracts failed during account creation because the analysis script made incorrect assumptions about the expected world state.The reported evaluation results used Table II and the associated coverage figure.
A. Smart Contract Security Assessments
Manticore has been used in Trail of Bits client engagements to discover bugs and verify code invariants in real-world smart contracts.
- A. Smart Contract Security Assessments: Manticore supported bug discovery and code-invariant verification across multiple Trail of Bits client engagements.The cited assessment reports provide additional detail on applying Manticore to real-world smart contracts.
VI. RELATED WORK
Symbolic execution tools span established binary-analysis frameworks and newer Ethereum-focused systems. Manticore is distinguished among Ethereum tools by supporting multiple execution environments rather than being purpose-built solely for Ethereum.
- Established symbolic execution tools include KLEE, angr, Triton, binsec, and miasm, with angr providing extensive binary-analysis functionality.
- Ethereum symbolic execution is less widely explored, with Mythril, VerX, and KEVM among the existing tools.
- Manticore is unique among the cited Ethereum tools because it was not purpose-built for Ethereum.The paper notes that the other listed tools, like Manticore, have also supported commercial software audits.
VII. CONCLUSION
Manticore is presented as a dynamic symbolic execution framework with user-friendly interfaces and an architecture spanning traditional binaries and Ethereum. Its evaluation reports comparable binary performance and 66% average code coverage for default smart-contract analysis.
- Manticore combines user-friendly interfaces with a flexible architecture supporting traditional binaries and the Ethereum platform.
- The Core Engine decouples symbolic execution logic from execution-environment details, enabling support for diverse platforms.
- Manticore performs comparably to another standard symbolic execution tool for regular binaries.
- 66% average code coverage is achieved with a default smart-contract analysis.