[paper learn] Symbolic execution with SYMCC: Dont interpret, compile!

Static Analysis

# Introduction

SYMCC 替换了编译器 做了一些插桩

# Background

符号执行框架分为前端后端，前端负责计算 expr 传递给后端的 solver (e.g. Z3).
alt text
Concolic execution 和 symbolic execution 的主要区别在于它们如何处理程序中的条件分支语句。 在 concolic execution 中，程序的某些路径会被选择执行，这取决于之前执行过程中的输入值和执行顺序。然后，这些已经执行过的路径将会被记录下来，而未执行过的路径将会被探索并执行，以便发现程序中的错误。

所以 CE 的本质是记录输入下的路径和路径的约束条件 而不是直接利用 CE 求解一个路径。

目前的符号执行技术有两种形式

  • IR-based : 逐行对 ir 语句解释 进行符号计算 优点是任意实现 缺点是 远离机器码 IR 到机器码的过程中应该还有问题
  • IR-less : 在机器码上通过 CPU 提供的功能对某些指令 hook 能够跳转进自己的代码进行执行和分析 缺点就是指令很多 要对大部分指令都进行一个符号的处理 但是速度快

这里减少 overhead 的方法就是避免将只涉及到 concrete value 的指令送给 SE backend。这部分不是很 care。

# Compilation-based symbolic execution

作者的做法就是直接写个 pass 编译进目标程序 其实就是插桩。

1
2
3
4
5
6
7
define i32 @is_double (i32, i32) {
	%3 = shl nsw i32 %1 , 1     // shift left 1 => 乘2
	%4 = icmp eq i32 %3 , %0
	%5 = zext i1 %4 to i32   // 指令将 %4 中的 1 或 0 值转换为 32 位整数类型
	ret i32 %5
}

插桩后，就是格外多走一步生成符号表达式丢给后端，程序逻辑并没有变.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
define i32 @is_double (i32, i32) {
	; symbolic computation
	%3 = call i8* @_sym_get_parameter_expression (i8 0)
	%4 = call i8* @_sym_get_parameter_expression (i8 1)
	%5 = call i8* @_sym_build_integer (i64 1)
	%6 = call i8* @_sym_build_shift_left (i8* %4 , i8* %5)
	%7 = call i8* @_sym_build_equal (i8* %6 , i8* %3)
	%8 = call i8* @_sym_build_bool_to_bits (i8* %7)
        
	; concrete computation (as before)
	%9 = shl nsw i32 %1 , 1
	%10 = icmp eq i32 %9 , %0
	%11 = zext i1 %10 to i32
	call void @_sym_set_return_expression (i8* %8)
	ret i32 %11
}

这里插桩的方法就是先用其他 IR-based 的解释器扫描一下 然后找出应该进行符号执行的地方 插入代码而不是执行代码。

另外的问题就是优化问题，由于是在 IR 层扫描语义后插桩，llvm 后端优化后可能会导致出现问题，而且优化后也会优化插桩的需要。
In the current implementation, our pass runs in the middle of the optimization pipeline, after basic optimizations like dead-code elimination and strength reduction but before the vectorizer

最后就是 SE 的边界问题，一个符号值调用外部库再回来其实就算作 concrete 了，不过可以通过对 libc 的某些函数进行一些简单的，比如 memcpy，还有 read (这里没对 scanf 进行实现 没法跟踪 scanf 的符号执行), 这里也有个 c++ 库的插桩版本。

# practice

这里没开 Z3 (高性能的无约束、位向量和有限域布尔求解器)。
symcc 的每个指导下一次数据输入的生成数据就放在 output 这个宏下面，需要指定。
symcc 提出了一个协调 fuzzer 数据交换的工具 fuzzing_helper (rust)

1
2
3
4
cmake -G Ninja -DQSYM_BACKEND=ON -DZ3_TRUST_SYSTEM_VERSION=on .
export SYMCC_OUTPUT_DIR=`pwd`/results
cargo install --path util/symcc_fuzzing_helper

这里随便写个相对复杂的 c 程序让 afl+symcc 来 fuzz（这里有个小坑就是 scanf 这里没实现符号化的追踪 只能 read)

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
#include <stdio.h>
#include <unistd.h>
#include <stdlib.h>
#include <string.h>
#include <stdint.h>

void foo() {
    uint32_t input;
    char buf[0x21];
    int *ptr = NULL;

    read(0, &input, 4);
    int n = read(0, &buf, 0x20);
    buf[n] = '\x00';


    printf("[D] input : %d\n", input);
    printf("[D] buf : %s\n", buf);

    if(input < 0xffffff && input > 0xfffff) {
        if(input % 2 == 0) {
            goto out;
        }
        if (buf[1] == 'A' && buf[3] == 'C') {
            if(buf[0] != 'A')
                goto out;
            if(strlen(buf) == 5) {
                printf("[+] reach out destination\n");
                *ptr = 1;
            }
        }
    }
out:
    return;
}
int main() {
    foo();
    return 1;
}
1
2
3
4
5
6
7
8
9
10
11
12
md afl_build; cd afl_build
cp ../test.c .
CC=$AFL/afl-clang-fast
$CC -o test test.c -g -no-pie

md symcc_build; cd symcc_build
cp ../test.c .
CC=~/proj/symcc/symcc
$CC -o test test.c -g -no-pie

mkdir corpus
echo A > corpus/dummy

注意这里必须要两个 afl

1
2
3
$AFL/afl-fuzz -M afl-master -i corpus -o afl_out -m none -- afl_build/test 
$AFL/afl-fuzz -M afl-slave -i corpus -o afl_out -m none -- afl_build/test 
symcc_fuzzing_helper -o afl_out -a afl-slave -n symcc -- symcc_build/test
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
$ tree -L 2
.
├── afl_build
│   ├── test
│   └── test.c
├── afl_out
│   ├── afl-master
│   └── symcc
├── corpus
│   └── dummy
├── symcc_build
│   ├── afl_out
│   ├── test
│   └── test.c
└── test.c

alt text

效果如下 看来还是不错的 单 afl 测要个半天 而且最重要的这个不会干扰 afl 的插桩 编译一个 afl 的版本和 symcc 的版本 这就非常 nice.

counter “imported” in the “path geometry” section increase after a short time - this means that the fuzzer instances and SymCC are exchanging inputs.

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
afl_out
├── afl-master
│   ├── crashes
│   │   ├── id:000000,sig:04,src:000003,op:havoc,rep:2
│   │   └── README.txt
│   ├── fuzz_bitmap
│   ├── fuzzer_stats
│   ├── hangs
│   ├── plot_data
│   └── queue
│       ├── id:000000,orig:dummy
│       ├── id:000001,src:000000,op:havoc,rep:4,+cov
│       ├── id:000002,src:000000,op:havoc,rep:8,+cov
│       └── id:000003,src:000001+000002,op:splice,rep:8,+cov
├── afl-slave
│   ├── crashes
│   │   ├── id:000000,sig:04,src:000002+000003,op:splice,rep:2
│   │   └── README.txt
│   ├── fuzz_bitmap
│   ├── fuzzer_stats
│   ├── hangs
│   ├── plot_data
│   └── queue
│       ├── id:000000,orig:dummy
│       ├── id:000001,src:000000,op:havoc,rep:2,+cov
│       ├── id:000002,sync:afl-master,src:000002,+cov
│       └── id:000003,sync:afl-master,src:000003,+cov
└── symcc
    ├── bitmap
    ├── crashes
    ├── hangs
    ├── queue
    │   ├── id:000000,src:000001
    │   ├── id:000001,src:000002
    │   └── id:000002,src:000002
    └── stats

# helper 原理

大概看了一下

  1. 从目标 slave 的 queue 读取 queue 上的 testcase 查 hash 表看是不是新的 case
  2. 用这个 testcase 去执行一次 symcc 编译过的程序 获取多个指导输出
  3. 分别用这几个 symcc 的指导输出 送给 afl-showmap 去测试能不能触发新的路径 根据它的返回值 决定挂到 afl 的哪个队列上

afl-showmap

1
afl-showmap -t 5000 -m none -b -o map.data -- ~/vuln-discovery/symcc_test/afl_build/test < ./Cargo.toml

根据一个输入 将被测程序本次的位图写入一个 map.data 文件