Enhancing Symbolic Execution with Veritesting

被引：126

作者：

Avgerinos, Thanassis ^{[1
]}

Rebert, Alexandre ^{[1
]}

Cha, Sang Kil ^{[1
]}

Brumley, David ^{[1
]}

机构：

[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA

来源：

36TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2014) | 2014年

基金：

美国国家科学基金会;

关键词：

Veritesting; Symbolic Execution; Verification;

D O I：

10.1145/2568225.2568293

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present MergePoint, a new binary-only symbolic execution system for large-scale testing of commodity off-the-shelf (COTS) software. MergePoint introduces veritesting, a new technique that employs static symbolic execution to amplify the effect of dynamic symbolic execution. Veritesting allows MergePoint to find twice as many bugs, explore orders of magnitude more paths, and achieve higher code coverage than previous dynamic symbolic execution systems. MergePoint is currently running daily on a 100 node cluster analyzing 33,248 Linux binaries; has generated more than 15 billion SMT queries, 200 million test cases, 2,347,420 crashes, and found 11,687 bugs in 4,379 distinct applications.

引用

页码：1083 / 1094

页数：12

共 47 条

[1]

Allen J.R., 1983, Proc. of the Symposium on Principles of Programming Languages. POPL, P177

[2]

Anand S, 2008, LECT NOTES COMPUT SC, V4963, P367, DOI 10.1007/978-3-540-78800-3_28

[3]

[Anonymous], 2006, P 13 ACM C COMP COMM

[4]

[Anonymous], 2007, Compilers: principles, techniques and tools

[5]

[Anonymous], 2008, P 15 NETW DISTR SYST

[6]

Babic D, 2008, ICSE'08 PROCEEDINGS OF THE THIRTIETH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, P211, DOI 10.1145/1368088.1368118

[7]

Babic Domagoj, 2008, THESIS

[8]

Bardin Sebastien, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P165, DOI 10.1007/978-3-642-22110-1_13

[9]

Beyer D, 2007, LECT NOTES COMPUT SC, V4590, P504

[10]

Boonstoppel P, 2008, LECT NOTES COMPUT SC, V4963, P351, DOI 10.1007/978-3-540-78800-3_27

← 1 2 3 4 5 →