一句话：提出基于 token 符号化的语法无关符号执行，并用两阶段算法生成更易通过解析器的输入。
解析代码在软件中广泛存在，而复杂解析程序的符号执行颇具挑战。采用字节级符号化时，生成的输入常被解析程序拒绝，从而损害符号执行的有效性与效率。本文观察到复杂解析程序通常采用基于 token 的输入语法检查，一个 token 序列对应输入语法的一种用例。为此，作者提出语法无关符号执行，核心思想是以 token 而非输入字节作为符号化单位。技术上设计两阶段算法：第一阶段收集 token 值的字节级约束；第二阶段利用 token 符号化与第一阶段收集的约束生成程序输入，使其更可能通过解析代码。目标是自动生成 token 序列，从而更有效、高效地测试复杂解析程序。
Parsing code exists extensively in software. Symbolic execution of complex parsing programs is challenging. The inputs generated by the symbolic execution using the byte-level symbolization are usually rejected by the parsing program, which dooms the effectiveness and efficiency of symbolic execution. Complex parsing programs usually adopt token-based input grammar checking. A token sequence represents one case of the input grammar. Based on this observation, we propose grammar-agnostic symbolic execution that can automatically generate token sequences to test complex parsing programs effectively and efficiently. Our method's key idea is to symbolize tokens instead of input bytes to improve the efficiency of symbolic execution. Technically, we propose a novel two-stage algorithm: the first stage collects the byte-level constraints of token values; the second stage employs token symbolization and the constraints collected in the first stage to generate the program inputs that are more possible to pass the parsing code.
DOI 原文 ·
@inproceedings{paperbot6693,
title = {Grammar-agnostic symbolic execution by token symbolization},
author = {Weiyu Pan and Zhenbang Chen and Guofeng Zhang and Yunlai Luo and Yufeng Zhang and Ji Wang},
booktitle = {ISSTA},
year = {2021},
doi = {10.1145/3460319.3464845}
}