Verifying systems rules using rule-directed symbolic execution
Verifying systems rules using rule-directed symbolic execution
复制标题
DOI：
10.1145/2451116.2451152
复制
发表时间：
2013-03
期刊：
影响因子：
--
通讯作者：
Heming Cui;Gang Hu;Jingyue Wu;Junfeng Yang
中科院分区：
文献类型：
--
作者：
Heming Cui;Gang Hu;Jingyue Wu;Junfeng Yang
系统代码必须遵守许多规则，例如“必须关闭打开的文件”。验证规则的一种方法是静态分析，但这种技术无法推断代码的精确运行时效果，常常会产生许多误报。另一种方法是符号执行，这是一种验证所有输入上的程序路径（不超过有限大小）的技术。然而，当应用于验证规则时，现有的符号执行系统常常盲目地探索许多冗余的程序路径，而遗漏了可能包含错误的相关路径。我们的主要见解是，只有一小部分路径与规则相关，其余（大多数）路径是不相关的，不需要验证。基于这一见解，我们创建了 WOODPECKER，一种新的符号执行系统，用于有效检查系统程序的规则。它提供了一组内置的常见规则检查器，以及一个供用户轻松检查新规则的界面。它将符号执行引导到与检查规则相关的程序路径，并合理地修剪冗余路径，以指数方式加速符号执行。它被设计为与启发式无关，使用户能够利用现有的强大搜索启发式。对 136 个系统程序总计 545K 行代码（包括一些最广泛使用的程序）的评估表明，每次验证运行的时间限制通常仅为一小时，WOODPECKER 有效地验证了有界输入的 28.7% 的程序和规则组合，而现有的符号执行系统 KLEE 仅验证了 8.5%。对于其余组合，WOODPECKER 验证的相关路径数量是 KLEE 的 4.6 倍。 WOODPECKER 的时间限制更长，比 KLEE 验证更多的路径，例如，在 4 小时的限制下验证的路径数量是 KLEE 的 17 倍。 WOODPECKER 检测到 113 条违规行为，其中包括 10 条严重数据丢失错误，其中 2 条最严重的错误已得到相应开发人员的确认。
Systems code must obey many rules, such as "opened files must be closed." One approach to verifying rules is static analysis, but this technique cannot infer precise runtime effects of code, often emitting many false positives. An alternative is symbolic execution, a technique that verifies program paths over all inputs up to a bounded size. However, when applied to verify rules, existing symbolic execution systems often blindly explore many redundant program paths while missing relevant ones that may contain bugs. Our key insight is that only a small portion of paths are relevant to rules, and the rest (majority) of paths are irrelevant and do not need to be verified. Based on this insight, we create WOODPECKER, a new symbolic execution system for effectively checking rules on systems programs. It provides a set of builtin checkers for common rules, and an interface for users to easily check new rules. It directs symbolic execution toward the program paths relevant to a checked rule, and soundly prunes redundant paths, exponentially speeding up symbolic execution. It is designed to be heuristic-agnostic, enabling users to leverage existing powerful search heuristics. Evaluation on 136 systems programs totaling 545K lines of code, including some of the most widely used programs, shows that, with a time limit of typically just one hour for each verification run, WOODPECKER effectively verifies 28.7% of the program and rule combinations over bounded input, whereas an existing symbolic execution system KLEE verifies only 8.5%. For the remaining combinations, WOODPECKER verifies 4.6 times as many relevant paths as KLEE. With a longer time limit, WOODPECKER verifies much more paths than KLEE, e.g., 17 times as many with a fourhour limit. WOODPECKER detects 113 rule violations, including 10 serious data loss errors with 2 most serious ones already confirmed by the corresponding developers.