一种支持多线程程序的符号执行技术

李 曈，丁国富

(1.清华大学计算机科学与技术系，北京 100084； 2.华为技术有限公司2012实验室，浙江 杭州 310052)

1 研究背景与研究内容

1.1 程序缺陷

随着计算机的不断普及，信息技术的不断发展，软件已经深入到人类生活的方方面面，小到每天的新闻浏览、移动支付，大到航空航天、军事安全等。现代人每天都要接触很多的应用程序，程序安全稳定的重要性不言而喻。但程序是人写的，程序中不可避免地会存在程序缺陷，导致程序运行卡顿、运算错误、崩溃退出等。软件测试、程序分析都是为了提前发现程序缺陷，避免对用户造成不必要的损失。IT企业中的程序员大部分的工作时间都是在解决程序缺陷，这极大地降低了程序开发的质量和速度。

著名的Web处理核心Mozilla在1998年开源，并使用Bugzilla平台进行程序缺陷报告和跟踪，截止2017年底，Mozilla在Bugzilla平台上收到的程序缺陷报告超过110万个，日均收到135个缺陷报告[1]。程序缺陷的解决时间也是描述程序缺陷严重性的重要指标之一。Bugzilla平台会将程序缺陷按严重情况进行分级，由高到低分为7个等级[2]。图1展示了Mozilla软件中不同严重等级的程序缺陷修复所需的平均时长，可以看出修改程序缺陷非常消耗开发人员的时间和精力。为了提高软件开发速度，改善软件开发环境，提高用户体验，研发出更好的程序分析方法和工具非常重要。

图1 Mozilla中程序缺陷修复所需的平均时长

1.2 多线程程序

单核CPU频率上限的逐渐到来，加上多核CPU技术的成熟和普及，使单线程程序性能随CPU频率不断提高而提高的“免费的午餐”时代结束，多线程编程越来越普及。

多线程程序目前已经在很多关键领域发挥着重要作用，比如网站的服务器，每时每刻都会处理大量的访问请求，会频繁地创建和销毁线程。在这种对多线程程序稳定性要求很高的场景中，对多线程程序进行全面的程序分析非常重要。

多线程程序与系统有比较多的交互，由于C/C++语言可以与系统环境比较方便地进行交互，且C/C++语言的性能比较好，使这门编程语言在多线程领域有比较大的优势。近些年来各领域的代表性工作都是使用C/C++语言编写的多线程程序，比如网站服务器领域的Nginx[3]、机器学习领域的Tensorflow[4]、GPU编程领域的CUDA[5]等。Pthread库是用C/C++语言实现POSIX标准的线程库，是C/C++语言中最常用的线程库，已经成为多线程编程开发人员必须掌握的知识。

1.3 程序分析方法

程序分析有多种方法，包括静态程序分析、动态程序分析、混合方法、形式化方法。静态程序分析不运行程序，而是在编译过程中收集数据流和控制流等信息来进行分析和检测，缺点在于误报率高。动态程序分析则是多次运行程序，通过在程序代码中进行插桩等方式来收集程序在运行过程中的各种信息，通过这些信息来对程序进行分析和检测，缺点在于对测试集依赖较大。混合方法是将静态分析和动态分析这2种方法综合使用的一种方法。形式化方法是近些年来出现的新方法，基于严格的数学基础，以形式规约和形式验证的方法对计算机硬件系统或软件系统进行验证[6]。

形式化方法的思路和已有的通过程序分析来寻找程序缺陷的思路有根本性的不同，已有的方法绝大部分都是“找bug”的研究思路，而形式化方法可以证明一段程序不存在某类bug。这类方法的优势在于理论上可以完美地解决程序缺陷的问题，缺陷在于形式化证明的难度很大，需要大量的数学证明和代码求解，且用来求解的代码量远大于被验证的程序，所以形式化方法离实际应用还有一段不小的距离。

符号执行是一种比较初级的形式化方法，也有人将符号执行划分到混合方法的分类中。符号执行是将变量当作符号量来对程序进行翻译和处理，会记录程序分支处相关变量取值的约束，从而避免了误报。另外，符号执行会在程序分支时新增一条执行路径，所以对测试输入集没有依赖，且对程序代码的覆盖率较高。符号执行的优点使符号执行被看作形式化方法的一种。

1.4 本文研究内容

综上，本文采用符号执行技术，针对使用Pthread库函数编写的C/C++语言多线程程序，设计并实现支持Pthread库函数的符号执行工具，对程序中存在的程序缺陷进行检查。其性能目标有2个：1)尽可能检测更多种类的程序缺陷；2)尽可能达到较高的代码覆盖率。

2 相关研究工作的分析总结

符号执行是一种程序分析技术，通过分析程序来得到特定程序路径执行的输入。符号执行的关键思想在于将输入变为符号量，从而将程序的输出视为一个符号量输入值的函数。符号执行的优点在于解决了静态程序分析误报率高和动态程序分析对测试集依赖较大的问题，可以做到0误报率，不依赖于测试集，且代码覆盖率高。

已有的符号执行工具中，主流的符号执行工具KLEE[7]、CUTE[8]、DART[9]没有提供对多线程程序的支持；Cloud9[10]首先将多线程程序支持加入到符号执行中后，这些年才有了一些用符号执行技术来检测多线程程序缺陷的工作，如jCUTE[11]、LCT[12]等。这些支持多线程程序的符号执行工具各有优缺点：

1)Cloud9[10]是第一个支持C语言多线程程序的符号执行工具，其优点在于支持分布式符号执行，可以在多台机器组成的集群环境中部署单个符号执行任务，缓解了符号执行时间效率较差的问题；其缺点在于工具稳定性很差，在单机测试的过程中，一些KLEE源码中的样例程序都会出现运行时错误，难以在实际中应用，原因在于Cloud9的核心解释器和约束求解器比较老，不稳定，在此之上增加分布式的功能，导致了Cloud9更加不稳定。

2)jCUTE[11]是CUTE[5]的扩展版，可以通过生成随机输入的方法来制造不同的线程交互顺序，且拥有窗口界面。但是并未开源，而且仅支持Java语言的程序，不支持C/C++语言程序。

3)LCT[12]可以通过枚举线程交互顺序来查找数据竞争类的程序缺陷。但是LCT支持C语言程序的工具并没有实现任何库函数。在符号执行中如果要分析库函数的话，必须要在符号执行工具中实现该库函数，不能用外部的运行库来代替。这样就导致LCT的被测试程序中不能使用任何C语言库函数，难以在实际中应用。

3 整体设计

3.1 符号执行基础框架选择

KLEE是学术界和工业界应用最广泛的开源符号执行工具。在学术界，很多工作都是基于KLEE设计和实现的[13-20]，截止至2019年9月已经有145篇论文是和KLEE相关的[21]。图2展示了KLEE发表以后，每年发表的与KLEE相关的论文数量，从中可以看出KLEE的研究与发展非常活跃。

图2 历年来发表的与KLEE相关的论文数量

KLEE的稳定性和后续发展空间都是符号执行工具中最好的，所以本文选择KLEE作为基础框架，在此之上进行Pthread库函数多线程程序支持的设计和实现。

符号执行的工作流程和编译器很相似，都是对程序指令逐条解释和处理，不同之处在于，符号执行会维护多条执行路径，每条执行路径中保存着该路径中所有符号量的约束集；在遇到库函数调用时，会用符号执行工具中实现的库函数进行代码替换。

3.2 KLEE的结构设计与工作流程

符号执行的工作流程和编译器很相似，都是对程序指令逐条解释和处理，不同之处在于，符号执行会维护多条执行路径，每条执行路径中保存着该路径中所有符号量的约束集；在遇到库函数调用时，会用符号执行工具中实现的库函数进行代码替换。KLEE整体工作流程如图3所示。

图3 KLEE的工作流程

KLEE的主要结构有4个部分，在整体工作流程中都有体现，这4个部分分别是：

1)执行路径。

执行路径是符号执行中最基本，也是最重要的概念，保存了一条程序路径上的函数调用栈、程序计数器、内存、符号量约束集等信息。

2)解释器。

KLEE的处理流程类似于程序解释器，会对程序指令逐条翻译和处理，负责翻译程序指令的就是KLEE的解释器，解释器保存了全局信息，并实现了解释器中各种程序指令的处理方式。

3)库函数。

符号执行需要记录所有表达式，被分析程序中使用库函数的话，不能直接调用系统中的运行时库，否则会漏掉表达式以及符号量的取值约束。所以KLEE需要自己实现库函数，被分析程序调用库函数时会进行代码替换。

4)求解器。

符号执行将一条执行路径中的所有程序指令都处理完后，会将执行路径中的所有约束集整理起来发送给SMT、Z3等求解器进行求解，并对结果进行汇总和输出，同时根据求解结果生成测试输入。

3.3 多线程程序支持的设计

基于3.2节对KLEE结构的分析，在KLEE中加入多线程程序支持需要对KLEE的4个部分主要结构分别进行考虑，其中，求解器是符号执行外部的步骤，符号执行工具的任务是将约束集发送给求解器；而且求解器是对表达式进行求解的，和多线程程序的支持无关，所以，只需要从执行路径、解释器、库函数这3个部分对多线程程序支持进行设计。

3.3.1 在执行路径中加入多线程程序支持

执行路径主要负责保存和管理执行路径上的程序计数器、函数调用栈等数据，要加入多线程支持，首先要在执行路径中加入线程的数据。从符号执行的角度来看，增加一条线程，只是增加了一条同时执行的指令，需要增加一个数据结构来表示线程的数据，包括本线程的函数调用栈、程序计数器等。

但是比较困难的地方在于，如何设计执行路径与线程这2个数据结构之间的关系。一个很直观的思路是——线程中包含该线程中所有的执行路径。这个思路和实际多线程编程的思路一致，无需额外转换，实现起来简单且出错概率小。但深入研究可以发现，子线程中有新的执行路径分支创建出来时，会有2个严重的问题：

1)只有一条执行路径可以正常退出，其他执行路径退出时，会发现线程的相关数据已经释放了，从而导致多次释放内存的运行时错误。

2)如果子线程是可结合状态的(joinable)，父线程只会接收子线程的一条执行路径，子线程的其他执行路径会丢失掉。

图4展示了这种情况，ExecutionState2是子线程中新分支出来的执行路径，但无法正常返回父线程，因为ExecutionState0在接收了ExecutionState1后，不再阻塞等待，而是接着向下执行，ExecutionState2返回父线程时会遇到错误的上下文环境。

图4 子线程中新分支出来的执行路径无法正常结束

为了避免这2个问题，线程的数据结构需要放在执行路径中。图5展示了图4中例子在新的模型中的运行方式，当子线程中遇到分支语句时，会将包含当前所有线程信息的执行路径复制一份，2个执行路径各走一条分支。图5中，2个灰色方框表示2个执行路径走的分支不同。

图5 子线程中的分支语句会创建出新的执行路径

3.3.2 在解释器和库函数中加入多线程程序支持

解释器的作用是实现程序指令翻译和处理，库函数的作用是提供代码实现，这两者需要相互配合才能完成库函数调用指令的处理。实现Pthread库函数的支持，既需要考虑库函数的语义，也需要考虑如何与符号执行核心进行配合。本节介绍主要的Pthread库函数在符号执行解释器中的处理方式，以及在符号执行库函数中的实现。线程的程序计数器、函数调用栈等动态信息保存在执行路径的线程类中；线程是否分离(detach)、线程的事件id等信息保存在库函数中，为了便于描述，将保存在库函数中的信息称为库函数空间。

1)线程创建函数——pthread_create。

创建一个新线程，首先要从全局分配一个新的线程id；然后设置库函数空间中线程的状态；最后调用符号执行核心中创建新线程的函数接口，进入符号执行核心中进行处理。在符号执行核心中，首先会定位线程的初始函数；然后将pthread_create中传递给线程初始函数的参数进行绑定；再将线程的函数调用栈初始化为空，并将线程的程序计数器初始化到线程初始函数的开头；最后在执行路径的线程队列中增加新建的线程。整体流程如图6所示。

图6 pthread_create的处理流程

2)线程终止函数——pthread_exit。

终结当前线程，首先要检查线程状态，如果线程是分离的，直接回收库函数空间中该线程的数据；如果线程是可结合的，则需要将库函数中该线程的数据结构中已结束标识设为1，并返回指针指向线程返回值，然后发出唤醒事件，告知所有阻塞等待该线程完成的线程。之后，调用klee.h中定义的接口klee_thread_terminate函数进入符号执行核心中进行处理。在符号执行核心中，如果当前执行路径中只剩当前线程这一个线程，就直接结束当前执行路径，回收该执行路径的所有资源；否则将该线程的数据清空。整体流程如图7所示。

图7 pthread_exit的处理流程

3)线程等待函数——pthread_join。

线程等待函数用来阻塞等待一个线程，并接收该线程的返回值指针。处理时，首先会进行线程id的检测，如果线程id不合法，或者线程id是当前线程，则返回错误信息；第二步会检测线程的状态，如果线程状态是分离的，则返回错误信息；然后，如果线程尚未结束，则通过调用klee.h中定义的klee_thread_sleep函数进入阻塞状态，并将等待事件设为该线程的事件id；如果线程已经结束，则接收线程的返回值指针并返回。最后，回收该线程在库函数中的数据。整体流程如图8所示。

图8 pthread_join的处理流程

4)线程分离函数——pthread_detach。

图9 pthread_detach的处理流程

线程分离函数用来将指定线程设为分离状态，一个分离状态的线程执行完成后，会直接销毁，不会返回父线程。MTSE工具在处理pthread_detach函数时，首先会检查线程id是否存在；然后会检查该线程状态是否已经结束，如果已经结束，则直接回收资源，否则将该线程的状态设为分离状态。整体流程如图9所示。

5)获取线程id函数——pthread_self。

pthread_self函数用于获取当前线程的线程id。MTSE在处理pthread_self函数时，会通过调用klee.h中的klee_thread_self函数直接进入符号执行核心，获取当前线程的线程id，并写入klee_thread_self传入的指针中。整体流程如图10所示。

图10 pthread_self的处理流程

6)线程比较函数——pthread_equal。

线程比较函数用来比较2个线程是否是同一个线程，接收的参数为2个pthread_t类型的线程id。这个函数比较简单，不需要进入符号执行核心处理，直接在库函数实现中对2个线程id进行比较即可。设置pthread_equal函数的目的在于防止未来线程id的数据类型变化导致代码不向后兼容，但是在库函数中不存在这种问题，因为符号执行中的库函数实现不被其他代码调用，不需要向后兼容。

7)线程同步互斥函数。

多线程编程中同步互斥是非常重要的一部分[22]，线程的同步互斥是通过各种锁来实现的，常见的锁包括互斥锁mutex、自旋锁spinlock、读写锁rwlock。对于符号执行来说，自旋锁的空转等待没有实际意义，因为符号执行并不是真正执行程序，空转等待不会带来性能上的优势；而且解释器只有一个，空转等待的话会造成整个符号执行系统空转。所以，在符号执行中，自旋锁被当作互斥锁实现，读写锁除了判断读者写者外，锁这部分的操作也是用互斥锁来实现的。

互斥锁在MTSE的库函数实现中有自己的数据结构，保存了锁的事件id、锁是否被占用、锁的拥有者、排队的线程数这些信息。使用互斥锁时，首先需要调用pthread_mutex_init函数对锁变量进行初始化，内容包括分配事件id、申请内存。通过调用pthread_mutex_lock函数对互斥锁变量执行上锁操作时，会判断是否能获取到这个锁，如果不行，会进入阻塞等待状态。通过pthread_mutex_trylock函数对互斥锁变量执行上锁操作时，判断不能获取到这个锁的时候，会返回调用方，由调用方代码决定获取不到锁时的下一步操作。通过调用pthread_mutex_unlock函数释放互斥锁变量时，会进入符号执行核心，遍历当前执行路径中所有线程，选择一个等待该事件的线程，将其线程状态修改为就绪态。销毁一个互斥锁变量需要调用pthread_mutex_destroy函数，该函数会直接释放库函数空间中这个锁变量占用的内存资源。

3.4 设计的局限性

本文设计的支持Pthread多线程程序的符号执行有一定的局限性：

1)Pthread库函数的参数中不支持符号量。其原因在于本文对Pthread库函数的处理方式是参照实际执行中的执行方式来处理的，并没有对符号量参数实现相应的约束设计和求解。

2)Pthread库函数的实现并不完全支持。Pthread库函数有100多个，本文只实现了常用的Pthread库函数，可以对大多数Pthread多线程程序进行检测。

4 系统实现

本文的工作基于KLEE-2.0实现，命名为MTSE(Multi-Thread Symbolic Execution)，整体工作流程如图11所示。

相较于图3中KLEE的工作流程增加了2个模块，在图11中用深色方块表示。新增的2个模块为：

1)线程调度模块。

KLEE的解释器每处理完一个程序指令后，会重新挑选一个执行路径。MTSE在此基础上，会在执行路径选择一个线程来执行，并在选择线程的过程中完成线程状态检查的任务，保证不会选择处于阻塞状态的线程来执行。如果当前执行路径中所有线程都处于阻塞状态，MTSE会报出可能发生死锁的错误，同时结束该执行路径。

目前MTSE中线程调度策略采用的是单核FIFO调度，采用这种调度策略的原因有2点：KLEE的解释器原本就是单线程执行的；多线程程序中的基础程序缺陷检测与线程调度方式无关。

2)线程相关程序指令处理模块。

将解释器分为2个部分，一部分负责处理线程相关的指令，按照第3章介绍的方式实现；另一部分负责处理其他程序指令，在这部分中额外修改了return指令的处理方式，原因是加入多线程程序的支持后，子线程的函数调用栈为空时的return指令不能转换为exit指令，而应该转换为pthread_exit指令进行处理。

图11 MTSE的工作流程

5 性能测试

5.1 评价指标

第1章已经介绍过MTSE工具的设计目标，根据设计目标，本文设置了2个评价指标：

1)功能性。

程序分析工具的功能性表现为可以查找的程序缺陷的种类和数量上。能查找更多类型、更多数量的程序分析工具性能更好。

2)代码覆盖率。

符号执行能获得学术界和工业界的关注，最主要的原因在于符号执行可以达到比较高的代码覆盖率。代码覆盖率越高，表示对程序分析得越完全，程序的稳定性会有更高的保障。

5.2 测试数据

本文从实际生产环境中抽取了45个使用Pthread库函数编写的C/C++语言多线程程序作为测试数据。这45个测试程序包含了5类基本的程序缺陷：指针越界(数组越界)、加法溢出、乘法溢出、移位溢出、除0错误。

5.3 实验方案

目前已有的工作中，只有Cloud9[6]可以对使用Pthread库函数的C语言多线程程序进行符号执行，所以本文采用对比实验的方案，用MTSE和Cloud9在相同系统环境、相同时间限制内对测试程序进行分析，来检验MTSE在2个评价指标上的性能表现。

实验的系统环境如表1所示，虽然实验在多核服务器上运行，但是每个任务仅运行在单个核上。

表1 实验的系统环境

5.4 实验结果与分析

5.4.1 功能性测试结果与分析

测试程序共45个，包含了5个程序缺陷，对比实验结果见表2。

表2 Cloud9与MTSE的功能测试

从表2可以看出，Cloud9中没有乘法溢出、移位溢出和减法溢出的检测；除0错误的2个例子中，Cloud9检测不到的测试程序的情况是分母为一个符号量加5，符号量是负数的时候才可能出现除0的情况，检测不到的原因在于Cloud9的约束求解器版本较老，不能处理负数的情况。

从查找到的程序缺陷种类和数量来看，MTSE相较于Cloud9在功能性上有约50%的提升。

5.4.2 代码覆盖率测试结果与分析

代码覆盖率是符号执行的核心性能指标[23]，代码覆盖率可以细分为指令覆盖率和分支覆盖率，前者表示所有程序指令的覆盖率，后者表示所有程序分支的覆盖率。本文用这45个样例测试了MTSE和Cloud9的指令覆盖率和分支覆盖率，有5个样例在Cloud9中执行结束的时候会出现运行时错误，虽然可以报出程序缺陷，但是无法统计指令覆盖率和分支覆盖率。其余40个样例的结果如图12和图13所示。

图12是指令覆盖率的结果，MTSE在指令覆盖率上相对于Cloud9平均提升了31%。图13是分支覆盖率的结果，MTSE在分支覆盖率上相对于Cloud9平均提升了30%。

图12 MTSE和Cloud9的指令覆盖率对比

图13 MTSE和Cloud9的分支覆盖率对比

6 结束语

本文基于KLEE设计并实现了支持Pthread库函数的符号执行工具，相较于同类工作有不错的性能提升。本文的主要贡献包括：

1)分析了符号执行的工作流程，并在此基础上设计了支持多线程程序的代码架构；

2)分析了主要Pthread库函数的语义，实现了相关的库函数，并对解释器进行了扩展；

3)从实际生产中抽取了测试程序并设计实验，对MTSE工具进行了横向性能对比测试。

在本文工作的基础上，笔者未来工作的方向是将符号执行和动态方法相结合[23]，增加了多线程支持的符号执行可以结合其他的静态方法或者动态方法来进行更多类型的检测。一个笔者正在做的例子是将符号执行和动态方法中数据竞争[24]的技术结合起来，用符号执行的特性来解决动态方法对测试集依赖较大的缺点。