一句话：提出并行分叉符号执行框架 Park，通过多进程加速智能合约漏洞检测，最高取得约 7 倍加速。
智能合约符号执行漏洞检测需要遍历所有路径，现有工具耗时过高，检测精度受时间限制。本文提出 Park，首个面向智能合约的通用并行分叉符号执行框架。其核心是在符号执行过程中使用多个进程，利用多核 CPU 提升效率；具体包括基于 fork 操作的动态分叉算法、面向并行化中 SMT 性能损失的自适应进程限制与调整算法，以及基于共享内存的全局变量重建方法。作者将 Park 实现为插件并应用于 Oyente 和 Mythril。第三方数据集实验表明，Park-Oyente 与 Park-Mythril 相比原工具最高分别获得 6.84 倍和 7.06 倍加速。
Symbolic detection has been widely used to detect vulnerabilities in smart contracts. Unfortunately, as reported, existing symbolic tools cost too much time, since they need to execute all paths to detect vulnerabilities. Thus, their accuracy is limited by time. To tackle this problem, in this paper, we propose Park, the first general framework of parallel-fork symbolic execution for smart contracts. The main idea is to use multiple processes during symbolic execution, leveraging multiple CPU cores to enhance efficiency. Firstly, we propose a fork-operation based dynamic forking algorithm to achieve parallel symbolic contract execution. Secondly, to address the SMT performance loss problem in parallelization, we propose an adaptive processes restriction and adjustment algorithm. Thirdly, we design a shared-memory based global variable reconstruction method to collect and rebuild the global variables from different processes. We implement Park as a plug-in and apply it to two popular symbolic execution tools for smart contracts: Oyente and Mythril. The experimental results with third-party datasets show that Park-Oyente and Park-Mythril can provide up to 6.84x and 7.06x speedup compared to original tools, respectively.
DOI 原文 ·
@inproceedings{paperbot7417,
title = {Park: accelerating smart contract vulnerability detection via parallel-fork symbolic execution},
author = {Peilin Zheng and Zibin Zheng and Xiapu Luo},
booktitle = {ISSTA},
year = {2022},
doi = {10.1145/3533767.3534395}
}