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

计算机与现代化 ›› 2020, Vol. 0 ›› Issue (06): 60-.

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

(1.清华大学计算机科学与技术系，北京100084；2.华为技术有限公司2012实验室，浙江杭州310052)

出版日期:2020-06-24 发布日期:2020-06-28
作者简介:李曈(1993-)，男，山西河津人，硕士研究生，研究方向：程序分析，操作系统，E-mail: lt_cst@163.com；丁国富(1974-)，男，主任工程师，硕士，研究方向：软件项目可信质量保障，智能化测试，复杂系统可靠性测试，E-mail： dingguofu001@163.com。

A Symbolic Execution Technology Supporting Multi-thread Program

(1. Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;
2. Huawei Technologies Co. Ltd. 2012 Labs, Hangzhou 310052, China)

Online:2020-06-24 Published:2020-06-28

摘要/Abstract

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

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

Abstract: 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.

Key words: symbolic execution, multi-thread program, program analysis

中图分类号:

TP312

李曈, 丁国富. 一种支持多线程程序的符号执行技术[J]. 计算机与现代化, 2020, 0(06): 60-.

LI Tong, DING Guo-fu. A Symbolic Execution Technology Supporting Multi-thread Program[J]. Computer and Modernization, 2020, 0(06): 60-.

参考文献

［1］ RUNESON P, ALEXANDERSSON M, NYHOLM O. Detection of duplicate defect reports using natural language processing［C］// The 29th IEEE International Conference on Software Engineering. 2007:499-510.
［2］刘文杰,江贺. 软件缺陷报告严重性属性分析［J］. 计算机工程与应用, 2019,55(14):48-53.
［3］ SONI R. Nginx［M］. Berkeley: Apress, 2016.
［4］ ZACCONE G. Getting Started with TensorFlow［M］. England:Packt Publishing Ltd., 2016.
［5］ BECK P D, NEHMEIER M. Parallel interval newton method on CUDA［C］// International Workshop on Applied Parallel Computing. 2012:454-464.
［6］王戟,詹乃军,冯新宇,等. 形式化方法概貌［J］. 软件学报， 2019（1）:33-61.
［7］ CADAR C, DUNBAR D, ENGLER D R. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs［C］// Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 2008,8:209-224.
［8］ SEN K, MARINOV D, AGHA G. CUTE: A concolic unit testing engine for C［J］. ACM SIGSOFT Software Engineering Notes, 2005,30(5):263-272.
［9］ GODEFROID P, KLARLUND N, SEN K. DART: Directed automated random testing［C］// Proceedings of 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation. 2005:213-223.
［10］BUCUR S, URECHE V, ZAMFIR C, et al. Parallel symbolic execution for automated real-world software testing［C］// Proceedings of the 6th ACM Conference on Computer Systems. 2011:183-198.
［11］SEN K, AGHA G. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools［C］// International Conference on Computer Aided Verification. 2006:419-423.
［12］KHKNEN K, SAARIKIVI O, HELJANKO K. LCT: A parallel distributed testing tool for multithreaded Java programs［J］. Electronic Notes in Theoretical Computer Science, 2013,296:253-259.
［13］MECHTAEV S, YI J, ROYCHOUDHURY A. Angelix: Scalable multiline program patch synthesis via symbolic analysis［C］// Proceedings of the 38th ACM International Conference on Software Engineering. 2016:691-701.
［14］PALIKAREVA H, KUCHTA T, CADAR C. Shadow of a doubt: Testing for divergences between software versions［C］// 2016 IEEE/ACM 38th International Conference on Software Engineering. 2016:1181-1192.
［15］PEDROSA L, FOGEL A, KOTHARI N, et al. Analyzing protocol implementations for interoperability［C］// The 12th USENIX Symposium on Networked Systems Design and Implementation. 2015:485-498.
［16］KUCHTA T, CADAR C, CASTRO M, et al. Docovery: Toward generic automatic document recovery［C］// Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering. 2014:563-574.
［17］SLABY J, STREJ〖XCC1.TIF;%90%90〗EK J, TRTK M. Symbiotic: Synergy of instrumentation, slicing, and symbolic execution［C］// International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2013:630-632.
［18］JIN W, ORSO A. BugRedux: Reproducing field failures for in-house debugging［C］// 2012 34th IEEE International Conference on Software Engineering. 2012:474-484.
［19］NGUYEN H D T, Qi D, ROYCHOUDHURY A, et al. Semfix: Program repair via semantic analysis［C］// 2013 35th IEEE International Conference on Software Engineering. 2013:772-781.
［20］HUANG J, ZHANG C, DOLBY J. CLAP: Recording local executions to reproduce concurrency failures［J］. ACM Sigplan Notices, 2013,48(6):141-152.
［21］The KLEE Team. Publications and Systems Using KLEE ［EB/OL］. ［2019-09-23］. http://klee.github.io/publications/.
［22］李畅,范策,许宪成,等. 进程互斥与同步解析［J］. 现代计算机, 2010(14):6-10.
［23］SEN K. Concolic testing［C］// Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering. 2007:571-572.
［24］SEREBRYANY K, ISKHODZHANOV T. ThreadSanitizer: Data race detection in practice［C］// Proceedings of ACM Workshop on Binary Instrumentation and Applications. 2009:62-71.

[1]	戴延军1，吴志强2，刘杰1，刘朝晖1，陈智2，肖安红2. 一种安全关键软件系统符号执行优化方法[J]. 计算机与现代化, 2020, 0(01): 96-.
[2]	李航，臧洌，甘露. 负载均衡技术在并行化符号执行中的应用[J]. 计算机与现代化, 2018, 0(07): 86-.
[3]	李婧. 基于线程调度顺序控制的多线程程序测试[J]. 计算机与现代化, 2017, 0(6): 50-55.
[4]	宋文灏1，钟浩2，于海波1. 一种有效的API搜索算法[J]. 计算机与现代化, 2016, 0(4): 59-64.
[5]	胡翔1，舒礼莲2. 基于语义网络的海量源码搜索引擎[J]. 计算机与现代化, 2014, 0(7): 19-23.
[6]	范彧. 基于符号执行和数据挖掘的路径可达性检测研究[J]. 计算机与现代化, 2013, 1(3): 74-77.
[7]	夏嘉斌. 基于概率推演的动态程序切片优先度计算方法[J]. 计算机与现代化, 2013, 1(3): 12-16.
[8]	刘刚;胡凯平;宋发兴. 一种用于指针程序的形状分析方法[J]. 计算机与现代化, 2012, 1(200): 82-04.