Under-Constrained Symbolic Execution: Correctness Checking for Real Code
Under-Constrained Symbolic Execution: Correctness Checking for Real Code
复制标题
DOI：
--
复制
发表时间：
2015-08
期刊：
影响因子：
--
通讯作者：
David A. Ramos;D. Engler
中科院分区：
文献类型：
--
作者：
David A. Ramos;D. Engler
软件错误是众所周知的安全漏洞来源。符号执行是一种查找错误的技术，它考虑了程序的所有可能输入，但存在可扩展性限制。本文使用一种变体、欠约束的符号执行，通过直接检查单个函数而不是整个程序来提高可扩展性。我们展示了 UC-KLEE，这是一种用于检查 C/C++ 系统代码的新颖、可扩展的框架，以及两个用例。首先，我们使用UC-KLEE检查补丁是否会导致崩溃。我们检查了 BIND 和 OpenSSL 的 800 多个补丁，发现了 12 个错误，其中包括两个 OpenSSL 拒绝服务漏洞。我们还验证（带警告）115 个补丁不会导致崩溃。其次，我们使用 UC-KLEE 作为通用检查框架并实现检查器来查找内存泄漏、未初始化的数据和不安全的用户输入。我们对来自 BIND、OpenSSL 和 Linux 内核的 20,000 多个函数的检查器进行了评估，发现了 67 个错误，并验证了数百个函数没有泄漏，以及数千个函数不会访问未初始化的数据。
Software bugs are a well-known source of security vulnerabilities. One technique for finding bugs, symbolic execution, considers all possible inputs to a program but suffers from scalability limitations. This paper uses a variant, under-constrained symbolic execution, that improves scalability by directly checking individual functions, rather than whole programs. We present UC-KLEE, a novel, scalable framework for checking C/C++ systems code, along with two use cases. First, we use UC-KLEE to check whether patches introduce crashes. We check over 800 patches from BIND and OpenSSL and find 12 bugs, including two OpenSSL denial-of-service vulnerabilities. We also verify (with caveats) that 115 patches do not introduce crashes. Second, we use UC-KLEE as a generalized checking framework and implement checkers to find memory leaks, uninitialized data, and unsafe user input. We evaluate the checkers on over 20,000 functions from BIND, OpenSSL, and the Linux kernel, find 67 bugs, and verify that hundreds of functions are leak free and that thousands of functions do not access uninitialized data.