一句话：提出基于跨步值区间抽象的符号执行引擎，减少 SMT 查询以加速可达性判定。
符号执行引擎在执行中频繁查询 SMT 求解器以判定代码可达性，而 SMT 求解常成为性能瓶颈。本文受抽象解释启发，提出抽象符号执行（ASE）引擎，通过逐级变弱的抽象更快计算可达性，从而减少 SMT 查询。作者设计并实现了基于跨步值区间（SVI）集合的值集判定过程，可精确或欠近似地确定变量值集；ASE 先从 SVI 抽象开始推理，仅在必要时使用 SMT 中的位向量理论，并能检测当前抽象何时不完整以切换到下一抽象。作者为 64 位 RISC-V 子集实现原型。实验表明，该原型通常通过显著减少 SMT 查询来缩短符号执行时间，且抽象失败时的尝试开销仍较低。
A symbolic execution engine regularly queries a Satisfiability Modulo Theory (SMT) solver to determine reachability of code during execution. Unfortunately, the SMT solver is often the bottleneck of symbolic execution. Inspired by abstract interpretation, we propose an abstract symbolic execution (ASE) engine which aims at querying the SMT solver less often by trying to compute reachability faster through an increasingly weaker abstraction. For this purpose, we have designed and implemented a value set decision procedure based on strided value interval (SVI) sets for efficiently determining precise, or under-approximating value sets for variables. Our ASE engine begins reasoning with respect to the SVI abstraction, and then only if needed uses the theory of bit-vectors implemented in SMT solvers. Our ASE engine efficiently detects when the former abstraction becomes incomplete to move on and try the next abstraction.We have designed and implemented a prototype of our engine for a subset of 64-bit RISC-V. Our experimental evaluation shows that our prototype often improves symbolic execution time by significantly reducing the number of SMT queries while, whenever the abstraction does not work, the overhead for trying still remains low.
DOI 原文 ·
@inproceedings{paperbot6574,
title = {ASE: A Value Set Decision Procedure for Symbolic Execution},
author = {Alireza S. Abyaneh and Christoph M. Kirsch},
booktitle = {ASE},
year = {2021},
doi = {10.1109/ase51524.2021.9678584}
}