Background and Contribution

Background

Symbolic execution has been extensively researched in a security context, but industry has been slow to adopt the technique: Symbolic execution

  1. Lack of flexible, user-friendly tools.
  2. Existing frameworks are tightly coupled to traditional execution models, which makes symbolic execution research challenging for alternative execution environments, such as the Ethereum platform.

Contribution

Manticore is a symbolic execution framework for analyzing binaries and smart contracts.

Imporvements:

  1. highly flexible
  2. supports both traditional computing environments (x86/64, ARM) and exotic ones, such as the Ethereum platform

Architecture

The primary components are the Core Engine and Native and Ethereum Execution Modules. Secondary components include the Satisfiability Module Theories (SMT-LIB) module, Event System, and API.

manticore Architecture

Core Engine

核心引擎是 Manticore 灵活性的来源。 它实现了一个与平台无关的通用符号执行引擎，该引擎对基础执行模型几乎没有任何假设。该核心引擎根据图 1a 所示的状态生命周期来操作和管理程序状态。

程序状态是抽象对象，代表执行时某个点的程序状态。 这些对象公开了一个执行接口，Core Engine 调用该执行接口来触发程序执行的一个原子单元。对于本机二进制文件和以太坊，这是一条指令。 在执行期间，状态可能会中断并返回给 Core Engine，以表明需要处理生命周期事件。如图 1b 所示，

状态转换

状态生命周期定义了三个状态：就绪，忙碌和已终止以及两个事件：终止和具体化。 核心引擎反复选择就绪状态并执行（将其转换为繁忙）。 正在执行的 “忙碌” 状态可以转换回“就绪”状态，也可以发出生命周期事件供内核处理。

当状态结束时（通常在程序退出或内存访问冲突时）将状态转换为 “已终止” 时，将发生 “Termination” 事件。

“Concretization” 发生在一个状态发出信号，表示一个符号对象应该转换为一个或多个具体的值，受制于该状态的当前约束。对于每个具体值，都会创建一个新的子状态并将其标记为 “就绪”。 当程序计数器寄存器成为符号并具体化为可能的具体值时，就会发生 “Concretization” 最常见的例子，叫做分叉。 这导致为每个新程序路径生成新状态。

可以使用各种策略来自定义状态探索，这些策略实现了针对就绪状态选择和具体化（Ready state selection and Concretization）的各种启发式方法。 核心引擎是为并行性而设计的，并支持用于状态队列处理的多个进程。

Ethereum Execution Modules

因为 the Core Engine 是高度解耦合的，因此 adding Ethereum support did not require substantial architectural changes to Manticore （具体的论文没说）

Ethereum Symbolic Execution

Smart contracts receive input as network transactions consisting of a value and a data buffer. The transaction data buffer contains information about which function should be executed in a contract, and its arguments.

Symbolic execution of smart contracts involves symbolic transactions, where both value and data are symbolic. Symbolic transactions are applied to all Ready states,

Symbolic transactions can be repeatedly executed to generically explore the state space of a contract.

Manticore’s emulated environment for smart contract execution supports an arbitrary number of interacting contracts. It is capable of tracking not only a single contract’s state, but a full Ethereum ”world”

Auxiliary Modules

SMT-LIB module that supplies a custom symbolic expression object model and an SMT solver interface

The Event System decouples Manticore as a whole from external instrumentation-based analyses

Manticore can broadcast various symbolic execution events (e.g. memory reads/writes, state forking, concretization) that can be handled by an event subscriber outside of Manticore, such as an API client.

还有插件系统

ETHEREUM SMART CONTRACT ANALYSIS EVALUATION

Manticore’s Python API allows advanced users to customize their analysis using various forms of instrumentation. Hooking via the API lets users execute callbacks when a certain state is reached.

states can be pruned, custom constraints can be applied, and satisfiability queries can be sent to the solver

ETHEREUM SMART CONTRACT ANALYSIS EVALUATION

evaluated Manticore based on a corpus of 100 Ethereum smart contracts taken directly from the Ethereum blockchain1.

指标: tracks the number of states discovered and coverage of the contract code.

with a timeout of 90 minutes per contract Manticore produced an average coverage of 65.64%,

These assumptions were, however, sufficient for Manticore to achieve greater than 90% code coverage on 25 of the contracts.

Smart Contract Security Assessments

Trail of Bits 公司已经用了很多，详细见一些报告。

报告地址见论文末尾 12-16 测试报告有漏洞类别以及一些详细介绍等

优缺点

优点

  1. 灵活，用户友好（提供 api） 一个与平台无关的通用符号执行引擎
  2. 可扩展，有 Ethereum 测试模块

缺点

  1. 相对 angr 来说，不支持某些 IEEE754 浮点数指令（IEEE 754 floating point instructions），因此在 logic bomb benchmark 中效果不太好

Since angr supports the use of some IEEE 754 floating point instructions thatManticore does not, we expect that Manticore may overtake angr in the future, once it adds such support.

一些介绍

Manticore：符号执行

MANTICORE 简介，智能合约的符号分析工具

现存主流工具

  1. manticore
  2. Securify v2.0
  3. Oyente
  4. Beosin-VaaS
  5. Mythril
  6. EthIR
  7. Zeus
  8. Slither
  9. Osiris 只检测 integer bugs