Skip to content
Table of contents

KLEE 使用

3 min read ··· views #klee / #符号执行 / #软件测试

使用

KLEE 依赖较多，除了 LLVM、CMake 之类的通用依赖之外，还需要为其编译 SAT 求解器 MiniSat 和 SMT 求解器 STP。为了简化使用，可以直接使用官方提供的 Docker 镜像，命令如下：

docker run -ti --name=my_first_klee_container --ulimit='stack=-1:-1' klee/klee:3.0

docker start -aiklee_container
shell

KLEE 运行在 LLVM 位码上。要使用 KLEE 运行程序，需要先用 clang -emit-llvm 将程序编译为 LLVM 位码。

clang -I ../klee_build/include -emit-llvm -g -O0 -Xclang -disable-O0-optnone -c test.c -o test.bc
sh

运行 KLEE

要在位码文件上运行 KLEE，只需执行：

$ klee get_sign.bc
bash

应该会看到类似下面的输出：

KLEE: output directory = "klee-out-0"

KLEE: done: total instructions = 33
KLEE: done: completed paths = 3
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 3
bash
$ ls klee-last/
assembly.ll      run.istats       test000002.ktest
info             run.stats        test000003.ktest
messages.txt     test000001.ktest warnings.txt
sh

KLEE 生成的测试用例

KLEE 生成的测试用例被写入以 .ktest 为扩展名的文件中。这些是二进制文件，可以使用 ktest-tool 实用程序读取。ktest-tool 会输出同一对象的不同表示形式，例如 Python 字节字符串（data）、整数（int）或 ASCII 文本（text）。

$ ktest-tool klee-last/test000001.ktest
ktest file : 'klee-last/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: ....
sh

执行测试用例

虽然我们可以手动（或借助现有的测试基础架构）运行 KLEE 生成的测试用例，但 KLEE 提供了一个方便的重放库：它将对 klee_make_symbolic 的调用替换为对另一个函数的调用，该函数会将存储在 .ktest 文件中的值赋给程序输入。使用时，只需将程序与 libkleeRuntest 库链接，并将环境变量 KTEST_FILE 设置为所需测试用例的文件名。

$ export LD_LIBRARY_PATH=path-to-klee-build-dir/lib/:$LD_LIBRARY_PATH
$ gcc -I ../../include -L path-to-klee-build-dir/lib/ get_sign.c -lkleeRuntest
$ KTEST_FILE=klee-last/test000001.ktest ./a.out
$ echo $?
0
$ KTEST_FILE=klee-last/test000002.ktest ./a.out
$ echo $?
1
$ KTEST_FILE=klee-last/test000003.ktest ./a.out
$ echo $?
255
sh

KLEE 对浮点数的处理

KLEE 的符号执行引擎确实支持浮点数（如 float 和 double 类型），但处理能力有限。KLEE 原生并不完全支持浮点数的符号执行，尤其是在精确度和操作复杂度上可能会遇到一些困难。这是因为符号执行主要针对整数类型进行了优化，而浮点数涉及的数值范围、舍入误差等问题，使符号执行变得更加复杂。

  1. 符号执行支持：KLEE 确实能够对浮点数进行符号执行，但对某些操作（如浮点比较、算术运算等）可能没有与整数运算同等的精确支持。这意味着 KLEE 在遇到浮点数时，可能无法像处理整数那样精确地模拟计算过程，尤其是在符号约束（symbolic constraints）和符号路径（symbolic path）上。

  2. 浮点数具体化（Concretization）：如果 KLEE 遇到无法精确符号执行的浮点数表达式，通常会将其“具体化”为一个常数（如 0）。例如，当代码中涉及浮点数的算术运算或比较时，KLEE 可能会将浮点数的值设为默认值（通常是 0），以避免符号执行失败。

  3. 浮点数操作的精度问题：浮点数计算涉及舍入误差和精度问题，这对符号执行来说是一个挑战。KLEE 在浮点数计算时可能无法精确模拟这些操作，尤其是对于三角函数、对数等复杂的浮点数函数，符号执行的表现可能不如整数。

  4. 浮点数的优化与支持：KLEE 团队在浮点数符号执行方面已经进行了一些优化。具体来说，KLEE 使用了一个名为 SymFPU 的浮点数支持库来改进对浮点数操作的处理。SymFPU 专门用于浮点数符号执行，在有限的操作和函数支持上有所改进。