一句话：提出 LENT-SSE，通过已执行与邻近交易跳过/召回 SMT 求解，缓解多交易符号执行路径爆炸。
智能合约符号执行通常需处理多交易（TX）场景，这加剧了路径爆炸问题。论文首先定量分析多交易符号执行的瓶颈，发现交易路径存在冗余。为此提出 LENT-SSE，一种用于智能合约推测式符号执行的新启发式：利用已执行交易与正在执行路径间的冗余，设计基于已执行交易的跳过算法以减少 SMT 求解时间；并用基于邻近交易的召回算法减少错误跳过。在 SmartBugs 数据集上，LENT-SSE 在报告缺陷不减少的情况下，使总时间平均降低 37.4%，路径求解时间降低 65.2%；在包含 1000 个真实合约的数据集上，总时间与求解时间分别降低 38.1% 和 54.7%。
Symbolic execution has proven effective for code analytics in smart contracts. However, for smart contracts, existing symbolic tools use multiple-transaction symbolic execution, which differs from traditional symbolic tools and also exacerbates the path explosion problem. In this paper, we first quantitatively analyze the bottleneck of symbolic execution in multiple transactions (TXs), finding the redundancy of the paths of TXs. Based on this finding, we propose LENT-SSE as a new speculation heuristic for Speculative Symbolic Execution of smart contracts, which leverages the executed and near TXs for skipping and recalling the SMT solving of paths. LENT-SSE uses an executed-transaction-based skipping algorithm to reduce the time required for SMT solving by leveraging the redundancy between executed and executing paths. Moreover, LENT-SSE uses a near-transaction-based recalling algorithm to reduce false skipping of the solving paths. Experimental results on the SmartBugs dataset show that LENT-SSE can reduce the total time by 37.4% and the solving time of paths by 65.2% on average without reducing the reported bugs. On the other dataset of 1000 realistic contracts, the total time and solving time are reduced by 38.1% and 54.7%.
DOI 原文 ·
@inproceedings{paperbot8550,
title = {LENT-SSE: Leveraging Executed and Near Transactions for Speculative Symbolic Execution of Smart Contracts},
author = {Peilin Zheng and Bowei Su and Xiapu Luo and Ting Chen and Neng Zhang and Zibin Zheng},
booktitle = {ISSTA},
year = {2024},
doi = {10.1145/3650212.3680303}
}