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

• 作者: 丁国富 李曈
• 来源期刊: 计算机与现代化
• 学科: 工学
• 关键词: 符号执行 多线程程序 程序分析
• 年，卷（期）: 2020,（6）
• 所属期刊栏目: 软件工程
• 页码范围: 60-67
• 页数: 8页
• 分类号: TP312
• 字数: 6687字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-2475.2020.06.010

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李曈	清华大学计算机科学与技术系	1	0	0.0	0.0
2	丁国富		1	0	0.0	0.0