Backsolver: Adapting Preceding Execution Paths to Solve Constraints for Concolic Execution
0
Citation
26
Reference
10
Related Paper
Abstract:
Concolic execution follows the execution paths of concrete inputs, capable of generating new inputs for unexplored code by solving negated path constraints. However, implicit flows can hinder concolic execution, reducing the code coverage. Implicit flows occur when inputs influence control flow, and the control flow variation affects the values of some variables. During concolic execution, the preceding path selections limit the potential values of these variables. This limitation may result in unsolvable constraints, subsequently restricting the generation of new inputs for unexplored paths. Our insight is that following the same preceding paths is unnecessary, and we can adapt preceding paths to make the latest constraints solvable. We divide states into general states and implicit-flow-solving states (IFSSs). We utilize the general states to perform concolic execution. When solving constraints influenced by implicit flows, we switch to the IFSSs. We use the IFSSs to explore the relevant code region and adapt paths. To mitigate path explosion and construct the relation between inputs and the variables, we merge the IFSSs. State merging does not burden the general states, and we limit the code regions for the IFSSs to minimize the introduced overhead. Finally, we replace the variable symbols in the target constraints with new expressions and attempt to solve the new constraints. We implement our approach in Backsolver and build a test suite to evaluate it. Backsolver successfully identifies all the implicit flows in the test suite and resolves most of them. When evaluated on 6 real-world binaries, Backsolver resolves the highest number of branches related to implicit flows in total. Besides, Backsolver has the highest code coverage in PlutoSVG and finds a 0-day vulnerability. We reported the vulnerability and obtained a CVE ID.Keywords:
Concolic testing
JDart is a concolic execution extension for Java PathFinder. Concolic execution executes programs with concrete values while recording symbolic constraints. In this way, it combines the benefits of fast concrete execution, with the possibility of generating new concrete values, triggered by symbolic constraints, in order to exercise additional, potentially rare, program behaviors. As is typical with concolic execution engines, JDart can be used for test-case generation. Beyond this basic mode, it has also been used as a component of other tools. In this paper, we describe the main features of JDart, provide usage examples, and give an overview of applications that use JDart. We particularly concentrate on our efforts into making JDart robust enough to handle large, complex systems.
Concolic testing
Dart
Pathfinder
Component (thermodynamics)
Cite
Citations (3)
It has been a common phenomenon that embedded devices are used ubiquitously while the security of proprietary software running on devices has become more and more significant. These softwares are often presented to researchers in binary forms. Due to the lack of program semantics and meta information, it is very difficult to analyze manually in large-scale binary programs. Therefore, automatic binary program analysis has become a critical research direction. Symbolic execution is an important method of automatic analysis, due to the problem of path explosion in traditional symbolic execution, it is sometimes complecated to explore the deep-level path of the program, and the most of current execution engines using IR translation execution, resulting in symbolic execution velocity has been exceedingly restrained, comparing to native execution. To this end, we propose a binary program oriented partial-lifting-based compile concolic execution approach, which is combined with static analysis to dissect the binary parts that researchers are intrigued in. The program is simultaneously combined with semantic lifting, dynamic memory monitoring, and symbolic compiler to reconstruct it into a symbolic binary program. Users can perform concolic execution on this program repeatly, so as to explore the part of the original binary program at a rate close to native execution.
Concolic testing
Binary code
Binary translation
Cite
Citations (0)
Symbolic execution is a powerful static program analysis technique that has been used for the automated generation of test inputs. Directed Automated Random Testing (DART) is a dynamic variant of symbolic execution that initially uses random values to execute a program and collects symbolic path conditions during the execution. These conditions are then used to produce new inputs to execute the program along different paths. It has been argued that DART can handle situations where classical static symbolic execution fails due to incompleteness in decision procedures and its inability to handle external library calls.
Concolic testing
Symbolic trajectory evaluation
The Symbolic
Random testing
Symbolic data analysis
Cite
Citations (92)
In this talk, I will talk about the recent advances and challenges in concolic testing and symbolic execution. Concolic testing, also known as directed automated random testing (DART) or dynamic symbolic execution, is an efficient way to automatically and systematically generate test inputs for programs. Concolic testing uses a combination of runtime symbolic execution and automated theorem proving techniques to generate automatically non-redundant and exhaustive test inputs. Concolic testing has inspired the development of several industrial and academic automated testing and security tools such as PEX, SAGE, and YOGI at Microsoft, Apollo at IBM, Conbol at Samsung, and CUTE, jCUTE, CATG, Jalangi, SPLAT, BitBlaze, jFuzz, Oasis, and SmartFuzz in academia. A central reason behind the wide adoption of concolic testing is that, while concolic testing uses program analysis and automated theorem proving techniques internally, it exposes a testing usage model that is familiar to most software developers.
Concolic testing
Code coverage
Random testing
IBM
Symbolic data analysis
Fuzz testing
Cite
Citations (6)
Concolic testing
Symbolic data analysis
Code coverage
Cite
Citations (11)
Symbolic execution is being successfully used to automatically test statically compiled code. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monumental effort, and so is keeping it up-to-date as the target language evolves. Furthermore, ambiguous language specifications lead to their implementation in a symbolic execution engine potentially differing from the production interpreter in subtle ways. We address these challenges by flipping the problem and using the interpreter itself as a specification of the language semantics. We present a recipe and tool (called Chef) for turning a vanilla interpreter into a sound and complete symbolic execution engine. Chef symbolically executes the target program by symbolically executing the interpreter's binary while exploiting inferred knowledge about the program's high-level structure. Using Chef, we developed a symbolic execution engine for Python in 5 person-days and one for Lua in 3 person-days. They offer complete and faithful coverage of language features in a way that keeps up with future language versions at near-zero cost. Chef-produced engines are up to 1000 times more performant than if directly executing the interpreter symbolically without Chef.
Concolic testing
Python
Symbolic trajectory evaluation
Compiled language
Cite
Citations (5)
Concolic testing is a software testing technique, which improves the scalability of symbolic execution by allowing efficient concretization of symbolic expressions. Concretization converts a symbolic expression to a concrete value, e.g., when the constraints of a symbolic expression become too complex for the utilized solver to handle. Unfortunately, concretization negatively impacts completeness of the performed analysis. For example, if a branch in the tested program depends on a previously symbolic value, which is now concrete, this branch will not be tracked by the symbolic execution engine. As such, the tested code is not explored in its entirety and errors may remain undetected. In order to allow a verification engineer to identify code parts which have not been tested sufficiently, due to concretization, we propose a novel metric, which quantifies performed concretizations. Furthermore, we contribute a visualization of this metric, which eases identifying code parts, which depend, directly or indirectly, on symbolic values affected by concretization. To the best of our knowledge, this is the first work proposing a concretization metric for concolic testing, to stimulate further research on this topic we have released our implementation as open-source software.
Concolic testing
Solver
Code coverage
Code (set theory)
Symbolic trajectory evaluation
The Symbolic
Symbolic data analysis
Cite
Citations (0)
Concolic testing
Python
Symbolic trajectory evaluation
The Symbolic
Cite
Citations (9)
Concolic testing is a popular method based on symbolic execution and constraint solving, designed for security testing of applications. Unfortunately, the current effectiveness of concolic testing tools are limited when testing large applications due to the enormous number of control paths and limited budget. In this paper, we introduce selective symbolic execution, path selecting, random and incorrect seed input, three approaches to ease the path explosion and speed up bugs exploration. We also develop Crashmaker, a dynamic symbolic execution tool based on Valgrind and constraints solver STP, implementing our three improvement measures. To check the effectiveness and efficiency of Crashmaker, we make experiments with 7 different real-life programs, and compare with Avalanche. The evaluation results show that Crashmaker can effectively find more bugs in a more efficient way.
Concolic testing
Random testing
Satisfiability Modulo Theories
Solver
Fuzz testing
Code coverage
Cite
Citations (9)