More Web Proxy on the site http://driver.im/

research-article

Running symbolic execution forever

Authors:

Cristian CadarAuthors Info & Claims

ISSTA 2020: Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis

Pages 63 - 74

https://doi.org/10.1145/3395363.3397360

Published: 18 July 2020 Publication History

Abstract

When symbolic execution is used to analyse real-world applications, it often consumes all available memory in a relatively short amount of time, sometimes making it impossible to analyse an application for an extended period. In this paper, we present a technique that can record an ongoing symbolic execution analysis to disk and selectively restore paths of interest later, making it possible to run symbolic execution indefinitely. To be successful, our approach addresses several essential research challenges related to detecting divergences on re-execution, storing long-running executions efficiently, changing search heuristics during re-execution, and providing a global view of the stored execution. Our extensive evaluation of 93 Linux applications shows that our approach is practical, enabling these applications to run for days while continuing to explore new execution paths.

References

[1]

Ben Boyter. 2019. Sloc Cloc and Code (scc). https://github.com/boyter/scc

[2]

Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, and Philipp Wendler. 2012. Conditional Model Checking: A technique to pass information between verifiers. In Proc. of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE'12).

Digital Library

[3]

Stefan Bucur, Vlad Ureche, Cristian Zamfir, and George Candea. 2011. Parallel Symbolic Execution for Automated Real-World Software Testing. In Proc. of the 6th European Conference on Computer Systems (EuroSys'11).

Digital Library

[4]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08).

Digital Library

[5]

Cristian Cadar and Koushik Sen. 2013. Symbolic Execution for Software Testing: Three Decades Later. Communications of the Association for Computing Machinery (CACM) 56, 2 ( 2013 ), 82-90.

[6]

Rodrigo Castaño, Víctor Braberman, Diego Garbervetsky, and Sebastian Uchitel. 2017. Model Checker Execution Reports. In Proc. of the 32nd IEEE International Conference on Automated Software Engineering (ASE'17).

Digital Library

[7]

Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley. 2012. Unleashing Mayhem on Binary Code. In Proc. of the IEEE Symposium on Security and Privacy (IEEE S&P'12).

Digital Library

[8]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Eficient SMT Solver. In Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08).

[9]

GNU. 2019. GNU Binutils. https://www.gnu.org/software/binutils/

[10]

GNU. 2019. GNU Coreutils. https://www.gnu.org/software/coreutils/

[11]

GNU. 2019. GNU Difutils. https://www.gnu.org/software/difutils/

[12]

GNU. 2019. GNU Findutils. https://www.gnu.org/software/findutils/

[13]

GNU. 2019. GNU Grep. https://www.gnu.org/software/grep/

[14]

Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated Whitebox Fuzz Testing. In Proc. of the 15th Network and Distributed System Security Symposium (NDSS'08).

[15]

Xiangyang Jia, Carlo Ghezzi, and Shi Ying. 2015. Enhancing Reuse of Constraint Solutions to Improve Symbolic Execution. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'15).

Digital Library

[16]

Chris Lattner and Vikram Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proc. of the 2nd International Symposium on Code Generation and Optimization (CGO'04).

Digital Library

[17]

Steven Lauterburg, Ahmed Sobeih, Darko Marinov, and Mahesh Viswanathan. 2008. Incremental State-space Exploration for Programs with Dynamically Allocated Data. In Proc. of the 30th International Conference on Software Engineering (ICSE'08).

Digital Library

[18]

libspng [n.d.]. libspng. https://github.com/randy408/libspng

[19]

Paul Dan Marinescu and Cristian Cadar. 2012. make test-zesti: A Symbolic Execution Solution for Improving Regression Testing. In Proc. of the 34th International Conference on Software Engineering (ICSE'12).

Digital Library

[20]

Lorenzo Martignoni, Stephen McCamant, Pongsin Poosankam, Dawn Song, and Petros Maniatis. 2012. Path-exploration Lifting: Hi-fi Tests for Lo-fi Emulators. In Proc. of the 17th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'12).

Digital Library

[21]

Rui Qiu, Sarfraz Khurshid, Corina S. Păsăreanu, Junye Wen, and Guowei Yang. 2018. Using Test Ranges to Improve Symbolic Execution. In Proc. of the 10th International Conference on NASA Formal Methods.

[22]

Rui Qiu, Guowei Yang, Corina S. Păsăreanu, and Sarfraz Khurshid. 2015. Compositional Symbolic Execution with Memoized Replay. In Proc. of the 37th International Conference on Software Engineering (ICSE'15).

Digital Library

[23]

Greg Roelofs and Mark Adler. [n.d.]. zlib. https://zlib.net/

[24]

The tcpdump team. [n.d.]. tcpdump. https://www.tcpdump.org/

[25]

Willem Visser, Jaco Geldenhuys, and Matthew B. Dwyer. 2012. Green: reducing, reusing and recycling constraints in program analysis. In Proc. of the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE'12).

[26]

Guowei Yang, Corina S. Păsăreanu, and Sarfraz Khurshid. 2012. Memoized symbolic execution. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'12).

Digital Library

Cited By

Busse FNowack MCadar CBöhme MNoller YSzekeres L(2024)Sparse Symbolic Loop Execution (Registered Report)Proceedings of the 3rd ACM International Fuzzing Workshop10.1145/3678722.3685535(61-69)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3678722.3685535
Wang HTang ZTan SWang JLiu YFang HXia CWang ZRoychoudhury APaiva AAbreu RStorey M(2024)Combining Structured Static Code Information and Dynamic Symbolic Traces for Software Vulnerability PredictionProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639212(1-13)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639212
Barth MJakobs M(2024)Refining CEGAR-Based Test-Case Generation with Feasibility AnnotationsTests and Proofs10.1007/978-3-031-72044-4_3(45-64)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-72044-4_3
Show More Cited By

Index Terms

Running symbolic execution forever
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Runtime exception detection in Java programs using symbolic execution

Most of the runtime failures of a software system can be revealed during test execution only, which has a very high cost. In Java programs, runtime failures are manifested as unhandled runtime exceptions.

In this paper we present an approach and tool ...
Tuning parallel symbolic execution engine for better performance

Symbolic execution is widely used in many code analysis, testing, and verification tools. As symbolic execution exhaustively explores all feasible paths, it is quite time consuming. To handle the problem, researchers have paralleled existing symbolic ...
Combining static analysis error traces with dynamic symbolic execution (experience paper)
ISSTA 2022: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis

This paper reports on our experience implementing a technique for sifting through static analysis reports using dynamic symbolic execution. Our insight is that if a static analysis tool produces a partial trace through the program under analysis, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA 2020: Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis

July 2020

591 pages

ISBN:9781450380089

DOI:10.1145/3395363

General Chair:
Sarfraz Khurshid
University of Texas at Austin, USA
,
Program Chair:
Corina S. Păsăreanu
Carnegie Mellon University Silicon Valley / NASA Ames Research Center, USA

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 July 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

ISSTA '20

Sponsor:

SIGSOFT

ISSTA '20: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis

July 18 - 22, 2020

Virtual Event, USA

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
398
Total Downloads

Downloads (Last 12 months)79
Downloads (Last 6 weeks)10

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Busse FNowack MCadar CBöhme MNoller YSzekeres L(2024)Sparse Symbolic Loop Execution (Registered Report)Proceedings of the 3rd ACM International Fuzzing Workshop10.1145/3678722.3685535(61-69)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3678722.3685535
Wang HTang ZTan SWang JLiu YFang HXia CWang ZRoychoudhury APaiva AAbreu RStorey M(2024)Combining Structured Static Code Information and Dynamic Symbolic Traces for Software Vulnerability PredictionProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639212(1-13)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639212
Barth MJakobs M(2024)Refining CEGAR-Based Test-Case Generation with Feasibility AnnotationsTests and Proofs10.1007/978-3-031-72044-4_3(45-64)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-72044-4_3
Wang HMa PYuan YLiu ZWang STang QNie SWu S(2023)Enhancing DNN-Based Binary Code Function Search With Low-Cost Equivalence CheckingIEEE Transactions on Software Engineering10.1109/TSE.2022.314924049:1(226-250)Online publication date: 1-Jan-2023
https://doi.org/10.1109/TSE.2022.3149240
Kumazawa TTakimoto MKodama YKambayashi Y(2023)Enhancing Safety Checking Coverage with Multi-swarm Particle Swarm OptimizationAdvances in Practical Applications of Agents, Multi-Agent Systems, and Cognitive Mimetics. The PAAMS Collection10.1007/978-3-031-37616-0_12(137-148)Online publication date: 12-Jul-2023
https://doi.org/10.1007/978-3-031-37616-0_12
Tu HJiang LDing XJiang HRoychoudhury ACadar CKim M(2022)FastKLEE: faster symbolic execution via reducing redundant bound checking of type-safe pointersProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3558919(1741-1745)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3558919
Yi QYang G(2022)Feedback-Driven Incremental Symbolic Execution2022 IEEE 33rd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE55969.2022.00055(505-516)Online publication date: Oct-2022
https://doi.org/10.1109/ISSRE55969.2022.00055
Alhanahnah MJain RRastogi VJha SReps T(2022)Lightweight, Multi-Stage, Compiler-Assisted Application Specialization2022 IEEE 7th European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP53844.2022.00024(251-269)Online publication date: Jun-2022
https://doi.org/10.1109/EuroSP53844.2022.00024
Spang CLavan YHartmann MMeisel FKoch A(2022)DExIE - An IoT-Class Hardware Monitor for Real-Time Fine-Grained Control-Flow IntegrityJournal of Signal Processing Systems10.1007/s11265-021-01732-594:7(739-752)Online publication date: 6-Jan-2022
https://doi.org/10.1007/s11265-021-01732-5
He JSivanrupan GTsankov PVechev MKim YKim JVigna GShi E(2021)Learning to Explore Paths for Symbolic ExecutionProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484813(2526-2540)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484813
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents