KLEE 符号执行

发表于 分类于 阅读次数： 本文字数： 817 阅读时长 ≈ 3 分钟

#基本使用

  1. 修改程序源码，在合适的地方插入符号值
1
2
3
4
5
 int main() {
   int a;
+  klee_make_symbolic(&a, sizeof(a), "a");
   return get_sign(a);
 }
  1. 编译成 LLVM bitcode
1
$ clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c
  1. 符号模拟执行 bitcode
1
$ klee get_sign.bc
  1. 查看模拟得到的 test cases
1
$ ktest-tool klee-last/test000001.ktest

#内部实现

#Directory Structure

  • lib - KLEE 核心源代码
    • Basic - 不依赖 LLVM 的工具代码, 一堆工具类
    • Support - 依赖 LLVM 的工具代码, 一堆工具类
      • KTest.cpp
      • Statistics.cpp
    • Module - klee facilities for working with LLVM modules, including the shadow module/instruction structures we use during execution.
    • Expr - 表达式对象
    • Solver - 求解器 binder
    • Core - 核心符号虚拟机
  • tools - KLEE 的二进制
    • kleaver - 查询什么 log
    • klee - 符号模拟执行一个 bitcode
    • klee-replay - 复现 ktest
    • klee-stats
    • klee-zesti
    • ktest-gen
    • ktest-randgen
    • ktest-tool
  • runtime - 符号模拟执行时依赖的库

#Utilities KLEE 辅助类

#引用计数 ReferenceCounter ref<T>

这两个类用于实现引用计数

ReferenceCounter 放在被计数的对象中

1
2
3
class Human {
  ReferenceCounter _refCount;
};

ref<T> 是对象的引用, 重载了*和->运算符, 可以像指针一样使用

1
2
ref<Human> r(new Human());
r->hello();

#tools/klee KLEE 工具源码

#main 主函数

  • klee::loadFile 加载输入文件，可以是单个bitcode(.bc)或者archive(.a), 得到一组llvm::Module

  • klee::linkModules 把所有 Module 链接成一整个

  • 检查 triple

  • 配置 Libcxx, Libc

  • 配置程序运行环境: argc, argv, envp

  • 创建 Handler, Executor impl Interpreter

  • externalsAndGlobalsCheck 做检查

  • Replay or 模拟执行

  • interpreter->runFunctionAsMain 开始模拟执行

#Executor::run 开始

  • usingSeeds 判断

  • 主循环

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
// main interpreter loop
while (!states.empty() && !haltExecution) {
  ExecutionState &state = searcher->selectState();  // 选择一个 State
  KInstruction *ki = state.pc;  // 取指令
  stepInstruction(state);  // 更新 PC

  executeInstruction(state, ki);  // 执行指令
  timers.invoke();
  if (::dumpStates) dumpStates();
  if (::dumpPTree) dumpPTree();

  updateStates(&state);  // 更新 State

  if (!checkMemoryUsage()) {
    // update searchers when states were terminated early due to memory pressure
    updateStates(nullptr);
  }
}

很清晰的代码, 每次循环选择一个程序 ExecutionState, 执行下条 KInstruction, 更新状态, 然后重复.

其中 Searcher 实现了探索的策略, klee 中有多种实现, 如 BFS/DFS/Random 等

#程序状态 ExecutionState, StackFrame

执行状态, 包括栈帧

1
2
3
4
5
6
7
8
9
10
class ExecutionState {
  /// @brief Pointer to instruction to be executed after the current
  /// instruction
  KInstIterator pc;

  /// @brief Stack representing the current instruction stream
  std::vector<StackFrame> stack;

  // ...
};

栈帧里面包含 locals, 是一堆预分配的 Cell, 数量等于函数参数+指令总数

1
2
3
4
5
6
7
8
struct StackFrame {
  KInstIterator caller;
  KFunction *kf;
  CallPathNode *callPathNode;

  std::vector<const MemoryObject *> allocas;
  Cell *locals;
};

Cell 即对 Expr 的引用

1
2
3
4
5
namespace klee {
  struct Cell {
    ref<Expr> value;
  };
}

#Executor::executeInstruction 开始

根据指令 opcode 对应处理

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
case Instruction::Ret:
      // 求解return返回的值
      result = eval(ki, 0, state).value;

      // 考虑是否需要进行 coercion

      // bindLocal caller指令 的 dest cell 的 value
      bindLocal(kcaller, state, result);

case Instruction::Br:

case Instruction::IndirectBr:
case Instruction::Switch:
case Instruction::Unreachable:
case Instruction::Invoke:
case Instruction::Call:
case Instruction::PHI:
case Instruction::Select:
case Instruction::VAArg:
case Instruction::Add:
case Instruction::Sub:
case Instruction::Mul:
case Instruction::UDiv:
case Instruction::SDiv:
case Instruction::URem:
case Instruction::SRem:
case Instruction::And:
case Instruction::Or:
case Instruction::Xor:
case Instruction::Shl:
case Instruction::LShr:
case Instruction::AShr:
case Instruction::ICmp:
case Instruction::Alloca:
case Instruction::Load:
case Instruction::Store:
case Instruction::GetElementPtr:
case Instruction::Trunc:
case Instruction::ZExt:
case Instruction::SExt:
case Instruction::IntToPtr:
case Instruction::PtrToInt:
case Instruction::BitCast:
case Instruction::FNeg:
case Instruction::FAdd:
case Instruction::FSub:
case Instruction::FMul:
case Instruction::FDiv:
case Instruction::FRem:
case Instruction::FPTrunc:
case Instruction::FPExt:
case Instruction::FPToUI:
case Instruction::FPToSI:
case Instruction::UIToFP:
case Instruction::SIToFP:
case Instruction::FCmp:
case Instruction::InsertValue:
case Instruction::ExtractValue:
case Instruction::Fence:
case Instruction::InsertElement:
case Instruction::ExtractElement:
case Instruction::ShuffleVector:
case Instruction::Resume:
case Instruction::LandingPad:
case Instruction::AtomicRMW:
case Instruction::AtomicCmpXchg: