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

A Symbolic Execution Technology Supporting Multi-thread Program

作　　者：李曈 丁国富 LI Tong;DING Guo-fu(Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;Huawei Technologies Co. Ltd. 2012 Labs, Hangzhou 310052, China)

机构地区：[1]清华大学计算机科学与技术系,北京100084 [2]华为技术有限公司2012实验室,浙江杭州310052

出　　处：《计算机与现代化》2020年第6期60-67,共8页Computer and Modernization

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

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

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]