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

符号执行是一种实用的验证程序中是否包含某类错误的技术，具有0误报率的优点，但是主流的执行工具并不支持分析多线程程序。本文对已有的多线程程序的符号执行工具进行分析，发现存在的问题有：1）有些工具性能好，但是不支持外部库，实用性很差；2）有些工具支持外部库函数，但是版本老，难以更新和维护，无法检查减法溢出、乘法溢出、移位溢出等基本类型的bug。本文基于最主流的符号执行工具KLEE设计并实现支持多线程程序的符号执行工具——MTSE（Multi-Thread Symbolic Execution）。MTSE支持libc和libc++库，并且相对于已有的同类工作Cloud9，MTSE可以多查找出约50%的程序缺陷，并且指令覆盖率和分支覆盖率上均有约30%的提升。

A Symbolic Execution Technology Supporting Multi-thread Program

Symbolic execution is a useful method in program verifying. But most symbolic execution tools don’t support multi-thread program. This paper analyzes the existed tools which support multi-thread program, and finds these problems: 1) some tools have good performance, but do not support lib, and hard to use practically; 2) some tools support lib, but are too old to upgrade, and can not find some basic bugs such as subtraction overflow, multiplication overflow and shift overflow. To solve these problems, this paper designs and implements MTSE(Multi-Thread Symbolic Execution) based on KLEE. MTSE supports multi-thread program with libc and libc++. MTSE can find 50% more bugs than Cloud9, and bring about 30% improvement in both instruction coverage and branch coverage compared with Cloud9.