KLEE 入门
Eveneko Blogger

KLEE

安装依赖

for ubuntu

1
sudo apt-get install build-essential curl libcap-dev git cmake libncurses5-dev python-minimal python-pip unzip libtcmalloc-minimal4 libgoogle-perftools-dev libsqlite3-dev doxygen

for ubuntu >= 18.04

1
sudo apt-get install python3 python3-pip gcc-multilib g++-multilib 

查看ubuntu版本

1
cat /etc/lsb-release

安装lit以启用测试,tabulate支持klee-stats和wllvm中的其他功能,以便更容易将程序编译到LLVM位码

1
pip3 install lit tabulate wllvm

安装 llvm9

1
sudo apt-get install clang-9 llvm-9 llvm-9-dev llvm-9-tools  

安装约束求解器

任选其一

  • STP(recommend)
  • Z3
  • metaSTM

STP

外部依赖

1
sudo apt-get install cmake bison flex libboost-all-dev python perl zlib1g-dev minisat

安装STP

1
2
3
4
5
6
7
8
git clone https://github.com/stp/stp.git
cd stp
git checkout tags/2.3.3
c
cd build
cmake ..
make -j
sudo make install

在对更大的基准运行带有STP的KLEE之前,必须将堆栈的大小设置为非常大的值

可以写到 .bashrc 持久化

1
ulimit -s unlimited

获取KLEE

1
git clone https://github.com/klee/klee.git

配置KLEE

1
2
mkdir build
cd build

配置选项

1
2
3
4
5
6
7
8
9
10
11
cmake \
-DENABLE_SOLVER_STP=ON \
-DENABLE_POSIX_RUNTIME=ON \
-DENABLE_KLEE_UCLIBC=ON \
-DKLEE_UCLIBC_PATH=<KLEE_UCLIBC_SOURCE_DIR> \
-DENABLE_UNIT_TESTS=ON \
-DGTEST_SRC_DIR=<GTEST_SOURCE_DIR> \
-DLLVM_CONFIG_BINARY=<PATH_TO_llvm-config-9> \
-DLLVMCC=<PATH_TO_clang-9> \
-DLLVMCXX=<PATH_TO_clang++-9> \
<KLEE_SRC_DIRECTORY>
1
2
3
4
5
6
7
8
cmake \
-DENABLE_SOLVER_STP=ON \
-DENABLE_POSIX_RUNTIME=ON \
-DENABLE_KLEE_UCLIBC=ON \
-DKLEE_UCLIBC_PATH=/home/eveneko/Workspace/klee-uclibc \
-DENABLE_UNIT_TESTS=OFF \
-DENABLE_SYSTEM_TESTS=OFF \
/home/eveneko/Workspace/klee

默认选项,这些选项不包括对uClibC和POSIX运行时的支持

1
cmake ..

Build KLEE

1
make -j

Example

get_sign

1
2
3
# examples/get_sign

clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c
  • clang -emit-llvm 将其编译为LLVM位码
  • -I 参数是为了让编译器可以找到klee/klee.h
  • -g 构建以向位码文件添加调试信息非常有用,我们使用位码文件生成源线级统计信息。
  • -O0 -Xclang -disable-O0-optnone 传递给KLEE的位码不应该优化,因为我们手工为KLEE挑选了正确的优化。在较新的LLVM版本(>5.0)中,为KLEE编译时不应使用-O0零标志,因为它阻止KLEE进行自己的优化。

运行KLEE

1
klee get_sign.bc

KLEE生成的测试用例

1
ktest-tool klee-last/test000001.ktest

regexp

1
clang -I ../../include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone Regexp.c
  • -c 是因为我们希望将代码编译到对象文件(而不是本机可执行文件)

llvm-nm来验证此步骤是否有效

1
llvm-nm Regexp.bc

通常,在运行此程序之前,我们需要链接它才能创建本机可执行文件。然而,KLEE直接在LLVM位码文件上运行。

由于此程序只有一个文件,因此无需链接。

对于具有多个输入的“真实”程序,可以使用llvm链接工具代替常规链接步骤,将多个LLVM位码文件合并到一个模块中,该模块可以由KLEE执行。

使用KLEE执行代码

1
klee --only-output-states-covering-new Regexp.bc
  • --only-output-states-covering-new 将测试生成限制在实际覆盖新代码的状态。
  • --emit-all-errors 为所有路径生成测试用例。

默认情况下,KLEE将运行到用户按下Control-C 停止。

  • -max-time=<time span>:在给定的时间后停止执行,例如10min或1h5s。
  • -max-forks=N:停止在N符号分支之后分叉,并运行剩余的终止路径。
  • -max-memory=N:尝试将内存消耗限制在N兆字节。

Coreutils

使用gcov构建coreutils

1
2
3
4
5
6
7
coreutils-6.11$ mkdir obj-gcov
coreutils-6.11$ cd obj-gcov
obj-gcov$ ../configure --disable-nls CFLAGS="-g -fprofile-arcs -ftest-coverage"
... verify that configure worked ...
obj-gcov$ make
obj-gcov$ make -C src arch hostname
... verify that make worked ...
  • --disable-nls 因为这在C库中添加了许多我们不感兴趣的额外初始化
1
2
3
4
5
6
7
8
9
10
11
12
13
obj-gcov$ cd src
src$ ls -l ls echo cat
-rwxrwxr-x 1 klee klee 150632 Nov 21 21:58 cat
-rwxrwxr-x 1 klee klee 135984 Nov 21 21:58 echo
-rwxrwxr-x 1 klee klee 390552 Nov 21 21:58 ls
src$ ./cat --version
cat (GNU coreutils) 6.11
Copyright (C) 2008 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by Torbjorn Granlund and Richard M. Stallman.

在gcov支持下构建

我们可以使用gcov工具本身生成人类可读的覆盖信息形式

1
2
3
4
5
6
7
8
9
10
11
12
13
src$ rm -f *.gcda # Get rid of any stale gcov files
src$ ./echo**

src$ ls -l echo.gcda
-rw-rw-r-- 1 klee klee 896 Nov 21 22:00 echo.gcda
src$ gcov echo
File '../../src/echo.c'
Lines executed:24.27% of 103
Creating 'echo.c.gcov'

File '../../src/system.h'
Lines executed:0.00% of 3
Creating 'system.h.gcov'

安装WLLVM

1
pip install --upgrade wllvm

要成功执行WLLVM,必须将环境变量LLVM_COMPILER设置为底层LLVM编译器(dragonegg或clang)

1
export LLVM_COMPILER=clang

使用LLVM构建Coreutils

1
2
3
4
5
6
7
coreutils-6.11$ mkdir obj-llvm
coreutils-6.11$ cd obj-llvm
obj-llvm$ CC=wllvm ../configure --disable-nls CFLAGS="-g -O1 -Xclang -disable-llvm-passes -D__NO_STRING_INLINES -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__"
... verify that configure worked ...
obj-llvm$ make
obj-llvm$ make -C src arch hostname
... verify that make worked ...

coreutils 可执行文件

1
2
3
4
5
6
7
8
9
10
11
12
13
obj-llvm$ cd src
src$ ls -l ls echo cat
-rwxrwxr-x 1 klee klee 105448 Nov 21 12:03 cat
-rwxrwxr-x 1 klee klee 95424 Nov 21 12:03 echo
-rwxrwxr-x 1 klee klee 289624 Nov 21 12:03 ls
src$ ./cat --version
cat (GNU coreutils) 6.11
Copyright (C) 2008 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by Torbjorn Granlund and Richard M. Stallman.

我们获得的不是LLVM位码文件,而是可执行文件。

要获取所有Coreutils的LLVM位码版本,我们可以在所有可执行文件上调用extract-bc:

1
2
3
src$ find . -executable -type f | xargs -I '{}' extract-bc '{}'
src$ ls -l ls.bc
-rw-rw-r-- 1 klee klee 543052ls Nov 21 12:03 ls.bc

使用KLEE作为解释器

1
klee --libc=uclibc --posix-runtime  ./cat.bc --version

向应用程序介绍符号数据

1
klee --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3

获得KLEE内部统计数据的简短摘要

1
klee-stats klee-last

运行LLVM优化传递

1
klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3

重播KLEE生成的测试用例

1
klee-replay ./echo ../../obj-llvm/src/klee-last/test000001.ktest

Reference

  • Post title:KLEE 入门
  • Post author:Eveneko
  • Create time:2021-11-18 18:28:18
  • Post link:https://eveneko.com/2021/11/18/klee/
  • Copyright Notice:All articles in this blog are licensed under BY-NC-SA unless stating additionally.
 Comments