KLEE概览

Posted 2021-01-04 linkj

klee是什么

klee是通过对llvm bitcode进行解释以实现符号执行的工具。它通过插入函数调用（klee_make_symbolic）对内存进行符号化。并且会跟踪符号内存的使用，并收集使用这些符号内存的约束。如果有使用前面符号内存的其他内存，那么该内存也将会被符号化。当遇到一个使用符号化内存的分支时，KLEE会将执行状态一分为二，看看分支的哪一边可以找到一个可以满足符号约束的解。KLEE使用STP来求解这些符号约束。

klee的主要组件

1. 解释器（Interpreter）

klee::Interpreter 在字节码解释器接口中是一个主要的抽象类。klee::Executor 是这个类的一个主要的实例。应用程序的状态（比如说：内存，寄存器，和程序计数器）会被存储在klee::ExecutionState 的一个实例中。每一条路径被执行的的时候都会有一个这样子的实例（除非当一些执行状态又合并到了一起的时候）。在有分支的地方，如果条件是符号化的，那klee::Executor::fork 方法就会返回一个klee::ExecutionState::StatePair 来表示一对由分支产生的ExecutionState 。

1. 内存建模（memory）

MemoryObject 表示程序里面的地址分配（比如说调用malloc，stack objects， global variables），同时我们也可以简单的认为它是一个分配在某个地址上的对象独一无二的名字。ObjectState 是用来存储在一个特定的ExecutionState 中一个MemoryObject 中实际的内容（是不能被共享的）。

每个ExecutionState都存放着一个MenoryObjects->ObjectState的映射，利用地址空间数据结构（AddressSpace）进行存储，以immutable tree的形式实现。采用COW(写时复制)的方式，当向一个ObjectState进行写操作的时候，将会为这个object创建一个副本（AddressSpace::getWriteable）

通过函数AddressSpace::getWriteable(ObjectState os),找到适合写入的os,如果需要将进行object副本创建吗，返回os或者os的副本

从状态和映射的角度来看，stack、heap和全局对象并没有什么区别。唯一对stack对象有一些不同的处理就是，MemoryObject会被标记为isLocal并且这个MemoryObject会被存储在StackFrame的分配表里面。当StackFrame进行pop之后，这些对象都会被释放掉，以至于当前状态就再也不能直接访问内存了（对内存对象的引用可能仍然会在ReadExprs里，但是理论上说，实际的地址我们应该是找不到了）。

另外很重要的一点是，AddressSpace的映射是有序的。当我们想将一个符号化的地址解析为ObjectState时我们会用到它，我们先用一个特殊的值来表示符号化的地址，然后用这个值来找那些指针指向这个地址的对象。MemoryObjects和ObjectStates处理方式一样。

当处理符号化地址的时候，会先为这个符号化地址获得一个具体值，然后利用它开始查看指针能够落到的Object范围？

1. 表达式（Expression）

表达式（Expressions）
很多Expr类都对llvm的指令集进行了建模。ref

Expr类对llvm指令集进行建模，也用于表示具体表达式（constant expression）
有四种类型：

1.Constant Expr
2.Concat Expr:用一些字节组成更大的类型
3.Extract Expr：从大的类型中提取出小的
4.ReadExpr:符号化数组访问，（index，value）列表形式

内存的实现方式是将所有的访问拆解为字节级的操作，所以内存系统（即ObjectState）会用到大量的ConcatExpr和ExtractExpr，所以这些表达式应该尽可能的压缩他们的操作数。

ReadExpr可能是里面最重要的。理论上说，它就是一个索引和一些更新（写入）。ReadExpr会计算所有的值，所以两个索引是可以相等的。ObjectState使用一个cache处理具体的index的具体写入和符号化写入，但是对于符号化的index必须要创建一个列表。上述更新存储在UpdateList和UpdateNode结构中,以immutable的形式，这样可使拷贝成本较小且更容易实现共享。

对于每个ObjectState都会维护一个（index,value）吗？index和value分别代表什么含义?是offset和value吗？

1. 搜索器（Searcher）

基础类是klee::Searcher。Executor通过使用一个Searcher 去选择下一个状态（也就是说一个程序实例只走一条路径），从而使得一条语句被执行。在KLEE中有非常多的Searcher实现，分别实现了不同的搜索策略。

klee提供了多种搜索策略:

klee::RandomSearcher 随机选择
klee::DFSSearcher 深度优先搜索
klee::MergingSearcher 合并states