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

作     者：李曈 丁国富 LI Tong;DING Guo-fu

作者机构：清华大学计算机科学与技术系北京100084 华为技术有限公司2012实验室浙江杭州310052 

出 版 物：《计算机与现代化》 (Computer and Modernization)

年 卷 期：2020年第6期

页      码：60-67页

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

主 题 词：符号执行 多线程程序 程序分析 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1006-2475.2020.06.010

馆 藏 号：203936168...