KLEE项目地址

KLEE符号执行引擎 是一个强大的工具，通过符号执行技术来测试程序，探索不同的执行路径。KLEE最早由斯坦福大学开发，专门用于系统化地测试C和C++程序的所有可能执行路径。以下是KLEE的工作原理和主要组件(由GPT生成)：

KLEE相关概念

KLEE的关键概念

• 符号执行：KLEE使用符号变量代替具体值，将输入抽象成符号表达式，这样可以同时代表多个可能的执行路径。KLEE会为每个路径生成一组约束条件，这些条件描述了程序必须满足的路径条件。
• 约束求解：KLEE依赖约束求解器来判断每个路径的约束条件是否可满足。如果约束条件可解，则KLEE会继续探索该路径；否则，该路径会被丢弃。
• 路径探索：KLEE系统化地探索尽可能多的路径，以发现潜在的bug、崩溃或意外行为。当识别到错误时，KLEE会生成具体的测试用例来展示问题，帮助开发者复现并修复bug。

KLEE的主要组件

• 路径选择算法：帮助KLEE决定下一个需要探索的路径。常用策略包括深度优先搜索和广度优先搜索，KLEE允许选择不同策略以实现不同的测试目标。
• LLVM基础设施：KLEE运行在LLVM中间表示（IR）之上，而不是直接使用源码，因此能够适应所有可编译为LLVM IR的语言（如C/C++）。
• 测试用例生成：KLEE通过生成输入的具体值，使程序沿特定路径执行。这一功能对于自动化测试特别有价值，可以覆盖普通单元测试中可能遗漏的边缘情况。

KLEE的应用场景

• 错误检测：KLEE非常适合于检测缓冲区溢出、内存泄漏和其他安全漏洞。
• 代码覆盖率：KLEE能产生很高的代码覆盖率，特别适合于关键性的软件系统。
• 优化与分析：在研究中，KLEE有时用于分析程序行为或优化某些方面，如路径探索的效率。

KLEE的局限性

• 可扩展性：符号执行计算量庞大，KLEE在处理大型代码库时可能遇到状态爆炸问题。
• 环境建模：对于复杂系统（如网络、文件或设备交互），精确地模拟这些交互以进行符号执行具有挑战性。
• 约束复杂性：KLEE的性能高度依赖于约束求解器的效率，如果约束过于复杂，求解速度会变慢。

使用KLEE的步骤

• 安装LLVM和KLEE：在类Unix操作系统上安装LLVM（通常是兼容的3.4版本）和KLEE。
• 准备代码：将程序代码编译为LLVM IR（.bc文件）。
• 运行KLEE：使用.bc文件执行KLEE，指定最大时间、内存约束和路径探索策略等选项。
• 分析结果：检查KLEE生成的测试用例和执行路径，识别错误并优化代码覆盖率。

阅读论文KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs后做了一下笔记

论文逻辑：阐述模糊测试的常见问题->解释KLEE的优点->简单介绍KLEE对tr.c这个文件如何进行符号执行->解释KLEE的机理(其实就是和传统的符号执行一样)->KLEE的约束优化策略

KLEE优化策略

Expression Rewriting

表达式重写，简单来说就是精简表达式

Constraint Set Simplification

约束化简，当存在一个约束，同时此时的状态已经满足这个约束，则直接将这个约束化简为true

Implied Value Concretization

隐含值具体化，例子是x+1=10直接具体化为x=9，这样可以返回出一个常量表达式，利于约束求解

Counter-example Cache

反例缓存的目的是通过缓存已处理过的约束集合及其相应的解答，避免重复求解类似的问题，从而提高效率。