Java Ranger: statically summarizing regions for efficient symbolic execution of Java
Published 7 November 2020
Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, Willem Visser
Citations17
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveWill appear once the snapshot is generated
MethodsWill appear once the snapshot is generated
PopulationWill appear once the snapshot is generated
Sample sizeWill appear once the snapshot is generated
OutcomesWill appear once the snapshot is generated
ResultsWill appear once the snapshot is generated
LimitationsWill appear once the snapshot is generated
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
Abstract
Merging execution paths is a powerful technique for reducing path explosion in symbolic execution. One approach, introduced and dubbed "veritesting" by Avgerinos et al., works by translating abounded control flow region into a single constraint. This approach is a convenient way to achieve path merging as a modification to a pre-existing single-path symbolic execution engine. Previous work evaluated this approach for symbolic execution of binary code, but different design considerations apply when building tools for other languages. In this paper, we extend the previous approach for symbolic execution of Java.
Keywords
Computer Science
Communications of the ACMSymbolic execution and program testing
2,991 Citations1976James C. King
A particular system called EFFIGY which provides symbolic execution for program testing and debugging is described, which interpretively executes programs written in a simple PL/I style programming language.
KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs
2,681 Citations2008Cristian Cadar, Daniel Dunbar +1 more
A new symbolic execution tool, KLEE, capable of automatically generating tests that achieve high coverage on a diverse set of complex and environmentally-intensive programs, and significantly beat the coverage of the developers' own handwritten test suite is presented.
DART
1,501 Citations2005Patrice Godefroid, Nils Klarlund +1 more
DART is a new tool for automatically testing software that combines three main techniques, automated extraction of the interface of a program with its external environment using static source-code parsing, and dynamic analysis of how the program behaves under random testing and automatic generation of new test inputs to direct systematically the execution along alternative program paths.
Automated Software EngineeringModel Checking Programs
1,353 Citations2003Willem Visser, Klaus Havelund +3 more
A verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing, and uses state compression to handle large states and partial order reduction, slicing, abstraction and run-time analysis techniques to reduce the state space.
SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis
911 Citations2016Yan Shoshitaishvili, Ruoyu Wang +9 more
This paper presents a binary analysis framework that implements a number of analysis techniques that have been proposed in the past and implements these techniques in a unifying framework, which allows other researchers to compose them and develop new approaches.
IEEE Transactions on Software EngineeringA System to Generate Test Data and Symbolically Execute Programs
761 Citations1976Lori A. Clarke
A system that attempts to generate test data for programs written in ANSI Fortran by symbolically executing the path and creating a set of constraints on the program's input variables, which facilitates error detection and being a possible aid in assertion generation and automatic program documentation.
Heuristics for Scalable Dynamic Test Generation
402 Citations2008Jacob Burnim, Koushik Sen
Several heuristic search strategies are presented, including a novel strategy guided by the control flow graph of the program under test, which achieves significantly greater branch coverage on the same testing budget than concolic testing with a traditional depth-first search strategy.
Enhancing symbolic execution with veritesting
217 Citations2014Thanassis Avgerinos, Alexandre Rebert +2 more
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.
ACM Transactions on Computer SystemsThe S2E Platform
198 Citations2012Vitaly Chipounov, Volodymyr Kuznetsov +1 more
This article presents S2E, a platform for analyzing the properties and behavior of software systems, along with its use in developing tools for comprehensive performance profiling, reverse engineering of proprietary software, and automated testing of kernel-mode and user-mode binaries.
Automated Software EngineeringSymbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis
173 Citations2013Corina S. Păsăreanu, Willem Visser +4 more
Symbolic PathFinder is a software analysis tool that combines symbolic execution with model checking for automated test case generation and error detection in Java bytecode programs.
Green
154 Citations2012Willem Visser, Jaco Geldenhuys +1 more
This paper describes the key ideas of the approach and its implementation, the Green solver interface, which reduces constraints to a simple form, allows for reuse of constraint solutions within an analysis run, and allows for recycling constraint solutions produced in one analysis run for use in other analysis runs.
Software model checking via large-block encoding
147 Citations2009Dirk Beyer, Alessandro Cimatti +4 more
A generalization of the approach, in which transitions of the ART represent larger portions of the program, is proposed, which leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors.
Statically-directed dynamic automated test generation
120 Citations2011Domagoj Babić, Lorenzo Martignoni +2 more
A new technique for exploiting static analysis to guide dynamic automated test generation for binary programs, prioritizing the paths to be explored and showing that static analysis allows exploration to reach vulnerabilities it otherwise would not, and the generated test inputs prove that the static warnings indicate true positives.
MultiSE: multi-path symbolic execution using value summaries
106 Citations2015Koushik Sen, George C. Necula +2 more
Evaluation of MultiSE on several programs shows that value summaries are an eective technique to take advantage of the sharing of value along multiple execution path, that MultiSE can run significantly faster than traditional dynamic symbolic execution and, 3) MultiSE saves a substantial number of state merges compared to conventional state-merging techniques.
Memoized symbolic execution
105 Citations2012Guowei Yang, Corina S. Păsăreanu +1 more
A new approach for more efficient application of forward symbolic execution, which is a well-studied technique for systematic exploration of program behaviors based on bounded execution paths, with a trie-based data structure that stores the key elements of a run of symbolic execution.
No More Gotos: Decompilation Using Pattern-Independent Control-Flow Structuring and Semantics-Preserving Transformations
73 Citations2015Khaled Yakdan, Sebastian Eschweiler +2 more
DREAM is presented, the first decompiler to offer a goto-free output, a novel patternindependent control-flow structuring algorithm that can recover all control constructs in binary programs and produce structured decompiled code without any goto statements.
Lecture notes in computer scienceJDart: A Dynamic Symbolic Analysis Framework
67 Citations2016Kasper Søe Luckow, Marko Dimjašević +6 more
JDart is described, a dynamic symbolic analysis framework for Java that is able to handle NASA software with constraints containing bit operations, floating point arithmetic, and complex arithmetic operations e.g., trigonometric and nonlinear.
Lecture notes in computer scienceJBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
67 Citations2018Lucas C. Cordeiro, Pascal Kesseli +3 more
Experimental results show that JBMC can correctly verify a set of Java benchmarks from the literature and that it is competitive with two state-of-the-art Java verifiers.
Lecture notes in computer scienceState Joining and Splitting for the Symbolic Execution of Binaries
60 Citations2009Trevor Hansen, Peter Schachte +1 more
This work investigates a "state joining" approach to making symbolic execution more practical and describes the challenges of applying state joining to the analysis of unmodified Linux x86 executables.
ACM SIGPLAN NoticesThe program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages
51 Citations1990Karl J. Ottenstein, Robert A. Ballance +1 more
IEEE Transactions on Software EngineeringDependence Guided Symbolic Execution
45 Citations2016Haijun Wang, Ting Liu +4 more
It is argued that for the purpose of fault detection it is not necessary to systematically explore the paths, and a new symbolic execution approach is proposed to mitigate the path explosion problem by predicting and eliminating the redundant paths based on symbolic value.
Improving the cost-effectiveness of symbolic testing techniques for transport protocol implementations under packet dynamics
14 Citations2017Wei Sun, Lisong Xu +1 more
Two domain-specific heuristic techniques are proposed, called packet retransmission based priority and network state based priority, which are motivated by two common transport protocol properties, which improve the cost-effectiveness of symbolic execution based testing for transport protocols.
ACM SIGPLAN NoticesEfficient building and placing of gating functions
9 Citations1995Peng Tu, David Padua
An almost-linear time algorithm for constructing Gated Single Assignment (GSA), which is SSA augmented with gating functions at -nodes, is presented.
Lecture notes in computer scienceTools and Algorithms for the Construction and Analysis of Systems
8 Citations2019Tomáš Vojnar, Lijun Zhang
Finding Substitutable Binary Code for Reverse Engineering by Synthesizing Adapters
6 Citations2018Vaibhav Sharma, Kesha Hietala +1 more
This paper presents an algorithm that searches for substitutable code segments by attempting to synthesize an adapter between them, and confirms that instances of adaptably substitutable binary functions exist in real-world code, and suggests that adapter synthesis has promising reverse engineering applications.