基于约束的测试

Constraint Based Testing

KLEE: KLEE Symbolic Execution Engine

Godefroid P, Klarlund N, Sen K. DART: Directed automated random testing. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2005: 213-223.

Baldoni R, Coppa E, D’elia D C, et al. A survey of symbolic execution techniques. ACM Computing Surveys, 2018, 51(3): 1-39.

约束求解器作为一种强大的问题求解工具，能够通过分析和求解一组逻辑约束条件，确定满足特定要求的变量取值。符号执行 (Symbolic Execution) 是一种将程序执行过程与约束求解技术相结合的自动化测试方法，其核心思想是使用符号变量代替具体输入数据执行程序，并在执行过程中根据程序的分支条件不断收集和构建路径约束 (Path Constraint)，从而将测试用例生成问题转化为约束可满足性问题。

运行下述代码需要安装 KLEE 和 CLANG，并配置 Makefile 中的相关路径

A Simple Demo

对于如下一个简单的 function() 待测函数，我们可以通过 klee_make_symbolic() 将输入变量 x 和 y 声明为符号变量来进行符号执行：

// basic.c
#include <klee/klee.h>

int function(int x, int y) {
  int z = 2 * y;
  if (x == z) {
    y = y + 2;
    if (x > y + 10) {
      return 1;
    }
  }
  return 0;
}

int main(void) {
  int x;
  int y;

  klee_make_symbolic(&x, sizeof(x), "x");
  klee_make_symbolic(&y, sizeof(y), "y");

  function(x, y);
  return 0;
}

make basic

KLEE 将探索得到 3 个路径，并分别为每个路径生成一个测试数据。在输出目录中：

  • .ktest 文件记录了每个测试的具体输入，可使用 ktest-tool 查看；
  • .path 文件记录每个测试执行的 Path；
  • .smt2 文件记录每个测试对应的 Path Constraint (使用 SMT-LIBv2 格式)，可以看到 KLEE 会将 32 位 int 编码编码为 4 个 8-bits vector，并将整数运算映射为 bvadd 和 bvmul 等 bit-vector 运算。
  • run.stats 文件记录覆盖率等统计信息，可使用 klee-stats 查看。

对于如下的二分查找实现 binary_search()，我们通过 klee_make_symbolic() 将整个数组 values[] 和待查找值 key 都设为符号值，同时通过 klee_assume() 指定数组元素位于 0 到 20 之间、且严格递增，即令 KLEE 只探索合法的有序数组。同时，为了对程序输出进行自动判定，我们将 binary_search() 的结果和一个线性查找方法 linear_search() 进行比对 (一种 Differential Testing 策略)：

// binary.c
#include <klee/klee.h>
#include <stdio.h>

#define SIZE 7

int binary_search(const int values[], int size, int key) {
  int low = 0;
  int high = size - 1;

  while (low <= high) {
    int mid = low + (high - low) / 2;
    if (values[mid] == key) {
      return mid;
    }
    if (values[mid] < key) {
      low = mid + 1;
    } else {
      high = mid - 1;
    }
  }
  return -1;
}

int linear_search(const int values[], int size, int key) {
  for (int i = 0; i < size; i++) {
    if (values[i] == key) {
      return i;
    }
  }
  return -1;
}

int main(void) {
  int values[SIZE];
  int key;

  klee_make_symbolic(values, sizeof(values), "values");
  klee_make_symbolic(&key, sizeof(key), "key");

  for (int i = 0; i < SIZE; ++i) {
    klee_assume(values[i] >= 0);
    klee_assume(values[i] <= 20);

    if (i > 0) {
      klee_assume(values[i - 1] < values[i]);
    }
  }

  int actual = binary_search(values, SIZE, key);
  int expected = linear_search(values, SIZE, key);

  if (actual != expected) {
    printf("Binary Search = %d, Linear Search = %d\n", actual, expected);
    klee_report_error(__FILE__, __LINE__, "wrong result", "binary.err");
  }

  return 0;
}

make binary

KLEE 将探索得到 15 个路径，覆盖 SIZE = 7 下的所有可能执行情况。

此时，如果故意向代码中植入一个错误，例如将 while (low <= high) 改为 while (low < high)，则 KLEE 将生成触发该错误的测试数据，并生成对应的 .binary.err 文件。例如，对于如下输入，正确实现应返回 0，但在错误实现中会观察到 -1：

int arr[7] = {0, 1, 2, 3, 4, 16, 17};
int key = 0;

Path Explosion

符号执行的一个局限是路径爆炸问题。例如，对于如下待测函数 function()，每次循环都产生两个分支，因此在 N 次循环下将产 2^N 种不同的执行路径：

// path.c
#include <klee/klee.h>

#define N 5
volatile int score = 0;

void function(int choices[]) {
  for (int i = 0; i < N; i++) {
    if (choices[i] == 1) {
      score += 1;
    }
  }
}

int main(void) {
  int choices[N];
  klee_make_symbolic(choices, sizeof(choices), "choices");

  function(choices);
  return 0;
}

make path

当 N = 5 时，KLEE 能快速探索得到 32 条路径，但当 N = 20 时，所有路径总数将达到 1,048,576。

为了限制探索 (有界符号执行)，Makefile 中使用 --max-time=5s 和 --max-memory=512 限制 KLEE 的探索时间和内存使用。此外，还可以通过 --max-tests=100 限制生成的测试个数，或通过 --max-depth=5 来限制每条路径最多经过多少个符号分支。

在此基础上，还可通过修改 --search 来较不同搜索方式的区别：

  • dfs: 较快到达叶节点，较早产生 completed paths；
  • bfs: 长时间扩展中间状态，completed paths 可能很少甚至为 0；
  • random-path: 能到达一些叶节点，但数量和顺序受随机性影响；

Complex Arithmetic

符号执行的一个局限是复杂约束的求解问题。例如，如下 hash() 函数实现了一个通过乘法、异或、移位和旋转等非线性运算来计算 8 个大写字母对应 Hash 值的 Toy Hash 程序：

#include <stdint.h>
#include <klee/klee.h>

#define INPUT_SIZE 8
#define TARGET_HASH 0x91940bbbu // KLEEDEMO

static uint32_t rotate_left(uint32_t value, unsigned amount) {
  return (value << amount) | (value >> (32 - amount));
}

static uint32_t hash(const unsigned char input[INPUT_SIZE]) {
  uint32_t result = 0x811c9dc5u;

  for (int i = 0; i < INPUT_SIZE; ++i) {
    result ^= input[i];
    result *= 0x01000193u;
    result = rotate_left(result, 5);
    result ^= result >> 13;
    result *= 0x85ebca6bu;
  }

  return result;
}

int main(void) {
  unsigned char input[INPUT_SIZE];

  klee_make_symbolic(input, sizeof(input), "input");

  for (int i = 0; i < INPUT_SIZE; i++) {
    klee_assume(input[i] >= 'A');
    klee_assume(input[i] <= 'Z');
  }

  if (hash(input) == TARGET_HASH) {
    klee_report_error(__FILE__, __LINE__, "hash preimage found", "hash.err");
  }

  return 0;
}

make hash

此时，求解器需要求解约束 hash(input) == TARGET_HASH，即找到目标 Hash 值 0x91940bbbu 对应的原始字符串 KLEEDEMO。这里 Makefile 使用 --max-solver-time 限制单次约束求解时间，并使用 --max-time=10s 限制整体运行时间。

Makefile

CLANG = [CLANG_PATH]
CFLAGS = [KLEE_INCLUDE_PATH] -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone
KLEE_FLAGS = --solver-backend=z3 --search=dfs --write-paths --write-smt2s

.PHONY: all basic binary hash path clean

all: basic.bc binary.bc hash.bc path.bc

%.bc: %.c
  $(CLANG) $(CFLAGS) $< -o $@

basic: basic.bc
  klee $(KLEE_FLAGS) --output-dir=klee-basic $<

binary: binary.bc
  klee $(KLEE_FLAGS) --emit-all-errors --output-dir=klee-binary $<

path: path.bc
  -klee --solver-backend=z3 --search=dfs --output-dir=klee-path \
    --max-time=5s --max-memory=512 \
    --write-no-tests --dump-states-on-halt=false \
    --output-stats=false --output-istats=false $<

hash: hash.bc
  -klee $(KLEE_FLAGS) --output-dir=klee-hash \
    --max-solver-time=10s --max-time=20s $<

clean:
  rm -rf -- *.bc klee-basic klee-binary klee-path klee-hash