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

摘要：

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

关键词：符号执行、多线程程序、程序分析

分类号：TP312(计算技术、计算机技术)

在线出版日期：2020-06-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：60-67