符号执行

通俗的解释就是,给定程序的输出,分析程序可以通过哪些路径达到给定的输出

KLEE

安装(推荐使用Docker安装):

docker pull klee/klee:2.0

持久性容器:当退出容器时,容器里面的内容不会初始化
docker run -ti --name=namestring --ulimit='stack=-1:-1' klee/klee

启动容器
docker start -ai namestring

简单使用

给出的是官方实例的代码

#include <klee/klee.h>

int get_sign(int x) {
  if (x == 0)
     return 0;

  if (x < 0)
     return -1;
  else 
     return 1;
} 

int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
}

可以看到程序有三条路径输出

clang -I ../../include/ -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c

编译生成 get_sign.bc 文件,用klee 运行一下

klee get_sign.bc

输出如下

klee@2038f8489243:~/klee_src/examples/get_sign$ klee get_sign.bc 
KLEE: output directory is "/home/klee/klee_src/examples/get_sign/klee-out-1"
KLEE: Using STP solver backend

KLEE: done: total instructions = 33
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3

可以看到一共有33条指令,完成路径3条,产生3个测试用例

接下来看一下klee-last文件夹,里面存放的就是测试用例

输入如下命令,即可查看.ktest文件夹的内容

ktest-tool test000001.ktest

输出如下

ktest file : 'test000001.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x00'
object 0: hex : 0x00000000
object 0: int : 0
object 0: uint: 0
object 0: text: ....

明日计划

白天:全国大学生信息安全竞赛

赛后:继续学习符号执行框架



符号执行      klee

本博客所有文章除特别声明外,均采用 CC BY-SA 3.0协议 。转载请注明出处!