klee源码分析

symbolic execution

最近一个月在看符号执行相关的东西，有了初步的理解，感觉还是得结合具体的实践才能加深理解，但手头没相关工作，所以对符号执行到现在也感觉理解的不是很到位。

思想付诸代码实践

根据以往学习新知识的经验，决定找一个符号执行的工具，通过啃源码来学习相关思想。于是找到了klee。

klee基于LLVM，针对的是llvm能够识别的由clang编译源代码生成的.bc文件，支不支持二进制程序我不知道。在这里，可以这样理解，llvm将c源码转化为其可以识别的llvm指令字节码，klee以llvm指令集为基础，对llvm指令进行模拟执行，并在模拟执行的过程中结合一些数据结构来实现符号执行的思想。

下面来具体分析klee源码。关于源码的注释，有兴趣的可以通过邮箱找我获取。

在tools/klee文件夹下找到main.cpp文件，将该文件的main函数作为程序的起始点。在此说明下，对于replay相关的执行流程，暂且忽略，不影响问题的研究。在main函数中：

  1. llvm相关的初始化工作
  2. fork一个WatchDog，用于监视超时时间
  3. 初始化两个全局变量，ctx和mainModule。ctx类管理着与llvm核心框架相关的一些全局数据；mainModule存储着LLVM module所有的信息，是所有LLVM IR的最顶级容器。
  4. 完成主程序模块与各种libc的链接
  5. 将用户指定的环境变量的配置文件中的具体配置读出并存储到pEnvp变量中；将用户参数存储到pArgv变量中
  6. 实例化一个interpreter，并在externalsAndGlobalsCheck(finalModule)中执行一些看不太懂得check。
  7. 执行关键函数runFunctionAsMain
  8. 打印一些结果信息

上面的代码主要是准备解释执行的环境，然后进入具体的解释执行函数interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp)，该函数的参数说明执行的初始函数为mainFn，参数为out->numArgs和out->args，执行环境为pEnvp。在runFunctionAsMain函数中：

  1. 在klee的functionMap中找到参数f对应的函数(这里为main)，并用KFunction这个结构进行结构化，以便能够被klee识别和使用
  2. 迭代枚举main的参数，为argc个参数以及envc个环境变量分配指针空间，并存储在arguments这个向量中(这里，klee好像规定解释执行的函数(这里为main)的参数不能超过3个)
  3. 初始化记录混合符号执行路径以及单纯符号执行路径的流pathOS和symPathOS
  4. 记录符号执行时的状态切换，根据参数parentFrame为0可知，现在为初始状态
  5. 绑定参数，这里对于参数绑定的方法有点类似于压栈的操作，将参数复制到描述当前函数调用的StackFrame栈桢结构中，可以理解为模拟main函数执行的环境。对于klee绑定操作的解释，这里引用http://www.chengyuzhang.com/article/135对内存模型(Memory model)的解释:

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

每一个ExecutionState 使用AddressSpace 数据结构来保存从MemoryObjects -> ObjectState 的映射（AddressSpace是通过一个固定的树来实现的，所以可以很轻易的复制和共享）。每个AddressSpace都会包含在映射中ObjectStates 的一部分。当一个AddressSpace被复制的时候，它会丢失它所包含的ObjectState。之后所有对ObjectState的写入操作，都会生成一个这个对象的复制（AddressSpace::getWriteable）。这是一个保险机制（这个机制对所有的对象都是有效的，不仅仅的全局对象）。

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

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

简单来说，ExecutionState 使用AddressSpace 数据结构来保存从MemoryObjects -> ObjectState 的映射，这个映射代表着MemoryObject存储这ObjectState这个东西。这一步中对于参数的操作可以理解为将参数用MemoryObject和ObjectState等klee能够进行管理的类进行封装，以便后续使用。

  1. 将当前进程作为进程树的根节点，进入核心函数run(*state)
  2. 执行完run函数后，进行一些善后处理

在函数run(*state)中：

  1. 通过bindModuleConstants()函数对模块中每个函数的每条指令的常数进行一定的处理，将处理后的结果存储在某个数据结构中，在bindModuleConstants()函数中，是按照模块->函数->指令的层次结构来进行划分，逐层迭代的
  2. 将当前state添加到states这个全局中，这里说明一下，对于Executor的种子执行模式，我们也不关心。
  3. 在stepInstruction(state)函数中，对当前指令的covered属性进行判断并将该信息记录到相应数据结构中这里说明一下，只有当当前指令是unreachable，并且他的上条指令是不带return的函数调用时，该指令的covered属性才为false，其余情况下都记为true，记录后会将pc指向下一条指令
  4. 通过executeInstruction(state, ki)函数，基于llvm指令集，对当前指令进行具体的模拟执行
  5. 在updateStates(&state)中，对states进行更新。不同的搜索策略，其更新states这个管理所有state的全局变量的策略不同
  6. 时间相关的check，不关心
  7. 紧接着是得到一个searcher实例，然后通过该实例所采取的搜索策略来搜索执行下一个state，就这样进行搜索state->执行state的循环，直到执行完毕

在executeInstruction(state, ki)函数中，是对指令字节码的具体解析，指令细节可参考http://llvm.org/docs/LangRef.html，下面以几个比较具有代表性的指令为例：

Instruction::Ret：

  1. 用llvm对应的指令形式包装一下
  2. 得到ret所在的函数 的调用语句的地址
  3. 查看ret指令后是否有操作数
  4. 如果栈桢数目<=1，则考虑到栈桢的层层叠加的性质，当栈中的栈桢数为1时，说明该ret指令执行完毕后，程序就进入到了初始栈桢，意味着整个程序即将执行完毕，所以下面会exit；否则的话，由于ret指令的功能，执行完该条，就返回到了上一个栈桢，即调用者所在的栈桢，所以需要将当前栈桢弹出。
  5. 设置正确的PC值
  6. 当存在操作数时，对操作数进行处理

Instruction::Br

  1. 分为无条件跳转和有条件跳转。如果为无条件跳转，则只需进行基本块的切换即可
  2. 对于有条件跳转，通过Executor::StatePair branches = fork(state, cond, false)来处理分支，对于分支的处理，可以概括为：拿着该分支的限制条件(布尔表达式的并集)去找求解器进行求解，以此来判断两条分支的可行性，可行的分支会返回一个与其相对应的state实例，不可行的话会返回0，比如，若都可行，则返回(trueState,falseState)
  3. 对一些统计信息进行更新，举个例子，如果传进该函数的状态非空，并且在统计管理器中找不到该状态的索引的话，则认为该状态是coveredNew的，即新覆盖的
  4. 判断条件分支语句下的两个分支是否都可满足,然后通过函数transferToBasicBlock进行具体的基本块的切换

这里需要对void Executor::transferToBasicBlock(BasicBlock dst, BasicBlock src,ExecutionState &state)这个函数进行说明：

该函数就是做一个基本块的转换，这个函数改变的唯一变量就是state的pc值了，仅仅是将pc值置为将要跳转到的下一个基本块的入口，以此来完成基本块的转换而在完成转换的过程中，由于可能将要跳转的基本块的入口是一个phi指令，所以需要做额外的处理，而这个额外的处理就是记录下到达该phi node所在基本块的前置基本块，以方便决定phi的值

Arithmetic / logical

对于逻辑运算指令，只是在对应的地址绑定上对应的符号化表达式，这种符号化的表达式是求解器可以识别的

其他
对于其他的指令，需要说明的与上述指令类似，这里忽略，有兴趣的自行研究

After

勉勉强强读完了klee的主流程代码，感觉符号执行更像是一种思想，将可变输入用符号X(与数学中的X有着差不多的意思)进行代替，对程序的执行流程进行模拟，对执行过程中x的变换f进行记录，记录成求解器可以识别的表达式的形式f(x)，在任何需要知道x所代表的值的程序执行点，都可以用求解器对f(x)进行求解。对程序的执行流程的模拟，一般可以基于某种指令集，结合一些数据结构来实现，比如klee基于LLVM。而整个的模拟的过程，都是我们可以进行代码干预的，比如在何时进行信息记录，在何时进行数据的改变等等，都是可以在模拟执行的过程中通过一些插桩代码进行实现的，这些插桩代码也可以实现我们所需要的对于程序的分析，比如污点分析。

接下来会去看JonathanSalwan的Triton的相关资料，并阅读该项目的源码，以加深自己在这方面的理解。