一句话：提出开源动态符号执行框架 Manticore，支持二进制与以太坊智能合约分析，并允许用户自定义分析流程。
动态符号执行通过约束求解系统探索程序状态空间，是提升软件测试代码覆盖率的有效手段。本文介绍开源动态符号执行框架 Manticore，面向二进制与以太坊智能合约分析。其架构灵活，可支持传统及特殊执行环境，并通过 API 允许用户自定义分析流程。作者讨论 Manticore 的架构，并展示其在商业客户场景中发现漏洞与验证代码正确性的能力，强调该框架的可用性与可扩展性，为二进制和智能合约分析提供实践工具。
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.
@inproceedings{paperbot5244,
title = {Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts},
author = {Mark Mossberg and Felipe Manzano and Eric Hennenfent and Alex Groce and Gustavo Grieco and Josselin Feist and Trent Brunson and Artem Dinaburg},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00133}
}