一句话：提出用长度编码自动机与符号模型检测求解字符串和长度约束，可处理现有方法难解的问题。
字符串与长度约束在软件安全分析中至关重要。现有求解器多基于推理规则演绎或自动机分析：前者在语言替换等复杂字符串操作下可能低效，后者难以扩展处理长度约束，并因近似而不利于反例生成。受逻辑电路表示字符串分析的启发，本文提出带长度编码的隐式自动机表示；该自动机具有无限状态，可表示超出正则表达式的语言。作者将字符串与长度约束转换为长度编码自动机上操作的依赖图，并借助无限状态系统的符号模型检测器作为分析引擎。实验表明，该方法能处理现有方法无法求解的复杂字符串与长度约束。
Strings with length constraints are prominent in software security analysis. Recent endeavors have made significant progress in developing constraint solvers for strings and integers. Most prior methods are based on deduction with inference rules or analysis using automata. The former may be inefficient when the constraints involve complex string manipulations such as language replacement; the latter may not be easily extended to handle length constraints and may be inadequate for counterexample generation due to approximation. Inspired by recent work on string analysis with logic circuit representation, we propose a new method for solving string with length constraints by an implicit representation of automata with length encoding. The length-encoded automata are of infinite states and can represent languages beyond regular expressions. By converting string and length constraints into a dependency graph of manipulations over length-encoded automata, a symbolic model checker for infinite state systems can be leveraged as an engine for the analysis of string and length constraints. Experiments show that our method has its unique capability of handling complex string and length constraints not solvable by existing methods.
DOI 原文 ·
@inproceedings{paperbot4693,
title = {A symbolic model checking approach to the analysis of string and length constraints},
author = {Hung-En Wang and Shih-Yu Chen and Fang Yu and Jie-Hong R. Jiang},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3238189}
}