Search

CPU cache is a limited but crucial storage component in modern processors, whereas the cache timing side-channel may inadvertently leak information through the physically measurable timing variance. Speculative execution, an essential processor optimization, and a source of such variances, can cause severe detriment on deliberate branch mispredictions. Despite static analysis could qualitatively verify the timing-leakage-free property under speculative execution, it is incapable of producing endorsements including inputs and speculated flows to diagnose leaks in depth. This work proposes a new symbolic execution based method, SpecuSym, for precisely detecting cache timing leaks introduced by speculative execution. Given a program (leakage-free in non-speculative execution), SpecuSym systematically explores the program state space, models speculative behavior at conditional branches, and accumulates the cache side effects along with subsequent path explorations. During the dynamic execution, SpecuSym constructs leak predicates for memory visits according to the specified cache model and conducts a constraint-solving based cache behavior analysis to inspect the new cache behaviors. We have implemented SpecuSym atop KLEE and evaluated it against 15 open-source benchmarks. Experimental results show that SpecuSym successfully detected from 2 to 61 leaks in 6 programs under 3 different cache settings and identified false positives in 2 programs reported by recent work. [ABSTRACT FROM AUTHOR]

Message passing is the standard paradigm of programming in highperformance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges the scope of verifiable properties. We have implemented MPI-SV1 and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 61 out of the 111 tasks (55%) within one hour, while in comparison, MPI-SV verifies 100 tasks (90%). On average, compared with pure symbolic execution, MPI-SV achieves 19x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations. [ABSTRACT FROM AUTHOR]

Detecting regression bugs in software evolution, analyzing sidechannels in programs and evaluating robustness in deep neural networks (DNNs) can all be seen as instances of differential software analysis, where the goal is to generate diverging executions of program paths. Two executions are said to be diverging if the observable program behavior differs, e.g., in terms of program output, execution time, or (DNN) classification. The key challenge of differential software analysis is to simultaneously reason about multiple program paths, often across program variants. This paper presents HyDiff, the first hybrid approach for differential software analysis. HyDiff integrates and extends two very successful testing techniques: Feedback-directed greybox fuzzing for efficient program testing and shadow symbolic execution for systematic program exploration. HyDiff extends greybox fuzzing with divergence-driven feedback based on novel cost metrics that also take into account the control flow graph of the program. Furthermore HyDiff extends shadow symbolic execution by applying four-way forking in a systematic exploration and still having the ability to incorporate concrete inputs in the analysis. HyDiff applies divergence revealing heuristics based on resource consumption and control-flow information to efficiently guide the symbolic exploration, which allows its efficient usage beyond regression testing applications. We introduce differential metrics such as output, decision and cost difference, as well as patch distance, to assist the fuzzing and symbolic execution components in maximizing the execution divergence. We implemented our approach on top of the fuzzer AFL and the symbolic execution framework Symbolic PathFinder.We illustrate HyDiff on regression and side-channel analysis for Java bytecode programs, and further show how to use HyDiff for robustness analysis of neural networks. [ABSTRACT FROM AUTHOR]

Floating point is widely used in software to emulate arithmetic over reals. Unfortunately, floating point leads to rounding errors that propagate and accumulate during execution. Generating inputs to maximize the numerical error is critical when evaluating the accuracy of floating-point code. In this paper, we formulate the problem of generating high error-inducing floating-point inputs as a code coverage maximization problem solved using symbolic execution. Specifically, we define inaccuracy checks to detect large precision loss and cancellation. We inject these checks at strategic program locations to construct specialized branches that, when covered by a given input, are likely to lead to large errors in the result.We apply symbolic execution to generate inputs that exercise these specialized branches, and describe optimizations that make our approach practical. We implement a tool named FPGen and present an evaluation on 21 numerical programs including matrix computation and statistics libraries. We show that FPGen exposes errors for 20 of these programs and triggers errors that are, on average, over 2 orders of magnitude larger than the state of the art. [ABSTRACT FROM AUTHOR]

In previous work, we introduced zero-overhead profiling (ZOP), a technique that leverages the electromagnetic emissions generated by the computer hardware to profile a program without instrumenting it. Although effective, ZOP has several shortcomings: it requires test inputs that achieve extensive code coverage for its training phase; it predicts path profiles instead of complete execution traces; and its predictions can suffer unrecoverable accuracy losses. In this paper, we present zero-overhead path prediction (ZOP-2), an approach that extends ZOP and addresses its limitations. First, ZOP-2 achieves high coverage during training through progressive symbolic execution (PSE)--symbolic execution of increasingly small program fragments. Second, ZOP-2 predicts complete execution traces, rather than path profiles. Finally, ZOP-2 mitigates the problem of path mispredictions by using a stateless approach that can recover from prediction errors. We evaluated our approach on a set of benchmarks with promising results; for the cases considered, (1) ZOP-2 achieved over 90% path prediction accuracy, and (2) PSE covered feasible paths missed by traditional symbolic execution, thus boosting ZOP-2's accuracy. [ABSTRACT FROM AUTHOR]

Message Passing Interface (MPI) has become the standard programming paradigm in high performance computing. It is challenging to verify MPI programs because of high parallelism and non-determinism. This paper presents MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for verifying MPI programs having both blocking and non-blocking operations. MPI-SV exploits symbolic execution to automatically generate path-level models, and performs model checking on the models w.r.t. expected properties. The results of model checking are leveraged to prune redundant paths. We have implemented MPI-SV and the extensive evaluation demonstrates MPI-SV's effectiveness and efficiency. [ABSTRACT FROM AUTHOR]

Mutation-based fuzzing is a widely used software testing technique for bug and vulnerability detection, and the testing performance is greatly affected by the quality of initial seeds and the effectiveness of mutation strategy. In this paper, we present SAFL1, an efficient fuzzing testing tool augmented with qualified seed generation and efficient coverage-directed mutation. First, symbolic execution is used in a lightweight approach to generate qualified initial seeds. Valuable explore directions are learned from the seeds, thus the later fuzzing process can reach deep paths in program state space earlier and easier. Moreover, we implement a fair and fast coverage-directed mutation algorithm. It helps the fuzzing process to exercise rare and deep paths with higher probability. We implement SAFL based on KLEE and AFL and conduct thoroughly repeated evaluations on real-world program benchmarks against state-of-the-art versions of AFL. After 24 hours, compared to AFL and AFLFast, it discovers 214% and 133% more unique crashes, covers 109% and 63% more paths and achieves 279% and 180% more covered branches. Video link: https://youtu.be/LkiFLNMBhVE [ABSTRACT FROM AUTHOR]

Random and search-based test generators yield realistic test cases based on program APIs, but often miss structural test objectives that depend on non-trivial data structure instances; Whereas symbolic execution can precisely characterise those dependencies but does not compute method sequences to instantiate them. We present SUSHI, a high-coverage test case generator for programs with complex structured inputs. SUSHI leverages symbolic execution to generate path conditions that precisely describe the relationship between program paths and input data structures, and converts the path conditions into the fitness functions of search-based test generation problems. A solution for the search problem is a legal method sequence that instantiates the structured inputs to exercise the program paths identified by the path condition. Our experiments indicate that SUSHI can distinctively complement current automatic test generation tools. [ABSTRACT FROM AUTHOR]

Symbolic execution is a powerful program analysis technique, but it is dificult to apply to programs built using frameworks such as Swing and Android, because the framework code itself is hard to symbolically execute. The standard solution is to manually create a framework model that can be symbolically executed, but developing and maintaining a model is dificult and error-prone. In this paper, we present Pasket, a new system that takes a first step toward automatically generating Java framework models to support symbolic execution. Pasket's focus is on creating models by instantiating design patterns. Pasket takes as input class, method, and type information from the framework API, together with tutorial programs that exercise the framework. From these artifacts and Pasket's internal knowledge of design patterns, Pasket synthesizes a framework model whose behavior on the tutorial programs matches that of the original framework. We evaluated Pasket by synthesizing models for subsets of Swing and Android. Our results show that the models derived by Pasket are sufficient to allow us to use of-the-shelf symbolic execution tools to analyze Java programs that rely on frameworks. [ABSTRACT FROM AUTHOR]

Analyzing performance and understanding the potential bestcase, worst-case and distribution of program execution times are very important software engineering tasks. There have been model-based and program analysis-based approaches for performance analysis. Model-based approaches rely on analytical or design models derived from mathematical theories or software architecture abstraction, which are typically coarsegrained and could be imprecise. Program analysis-based approaches collect program profiles to identify performance bottlenecks, which often fail to capture the overall program performance. In this paper, we propose a performance analysis framework PerfPlotter. It takes the program source code and usage profile as inputs and generates a performance distribu- tion that captures the input probability distribution over execution times for the program. It heuristically explores high- probability and low-probability paths through probabilistic symbolic execution. Once a path is explored, it generates and runs a set of test inputs to model the performance of the path. Finally, it constructs the performance distribution for the program. We have implemented PerfPlotter based on the Symbolic PathFinder infrastructure, and experimentally demonstrated that PerfPlotter could accurately capture the bestcase, worst-case and distribution of program execution times. We also show that performance distributions can be applied to various important tasks such as performance understanding, bug validation, and algorithm selection. [ABSTRACT FROM AUTHOR]

Automated program repair (APR) seeks to improve the speed and decrease the cost of repairing software bugs. Existing APR approaches use unit tests or constraint solving to find and validate program patches. We propose Canonical Search And Repair (CSAR), a program repair technique based on semantic search which uses a canonical form of the path conditions to characterize buggy and patch code and allows for easy storage and retrieval of software patches, without the need for expensive constraint solving. CSAR uses string metrics over the canonical forms to cheaply measure semantic distance between patches and buggy code and uses a classifier to identify situations in which test suite executions are unnecessary-and to provide a finer-grained means of differentiating between potential patches. We evaluate CSAR on the IntroClass benchmark, and show that CSAR finds more correct patches (96% increase) than previous semantic search approaches, and more correct patches (34% increase) than other previous state-of-the-art in program repair. [ABSTRACT FROM AUTHOR]

Mastering a complex skill like programming takes many hours. In order to encourage students to put in these hours, we built Code Hunt, a game that enables players to program against the computer with clues provided as unit tests. The game has become very popular and we are now running worldwide contests where students have a fixed amount of time to solve a set of puzzles. This paper describes Code Hunt and the contest experience it offers. We then show some early results that demonstrate how Code Hunt can accurately discriminate between good and bad coders. The challenges of creating and selecting puzzles for contests are covered. We end up with a short description of our course experience, and some figures that show that Code Hunt is enjoyed by women and men alike. [ABSTRACT FROM AUTHOR]

Software testing is an expensive and time consuming process, often involving the manual creation of comprehensive regression test suites. However, current testing methodologies do not take full advantage of these tests. In this paper, we present a technique for amplifying the effect of existing test suites using a lightweight symbolic execution mechanism, which thoroughly checks all sensitive operations (e.g., pointer dereferences) executed by the test suite for errors, and explores additional paths around sensitive operations. We implemented this technique in a prototype system called ZESTI (Zero-Effort Symbolic Test Improvement), and applied it to three open-source code bases-GNU Coreutils, libdwarf and readelf-where it found 52 previously unknown bugs, many of which are out of reach of standard symbolic execution. Our technique works transparently to the tester, requiring no additional human effort or changes to source code or tests. [ABSTRACT FROM AUTHOR]

We propose to combine symbolic execution with volume computation to compute the exact execution frequency of program paths and branches. Given a path, we use symbolic execution to obtain the path condition which is a set of constraints; then we use volume computation to obtain the size of the solution space for the constraints. With such a methodology and supporting tools, we can decide which paths in a program are executed more often than the others. We can also generate certain test cases that are related to the execution frequency, e.g., those covering cold paths. [ABSTRACT FROM AUTHOR]

Software ships with known bugs because it is expensive to pinpoint and fix the bug exposed by a failing test. To reduce the cost of bug identification, we locate expressions that are likely causes of bugs and thus candidates for repair. Our symbolic method approximates an ideal approach to fixing bugs mechanically, which is to search the space of all edits to the program for one that repairs the failing test without breaking any passing test. We approximate the expensive ideal of exploring syntactic edits by instead computing the set of values whose substitution for the expression corrects the execution. We observe that an expression is a repair candidate if it can be replaced with a value that fixes a failing test and in each passing test, its value can be changed to another value without breaking the test. The latter condition makes the expression flexible in that it permits multiple values. The key observation is that the repair of a flexible expression is less likely to break a passing test. The method is called angelic debugging because the values are computed by angelically nondeterministic statements. We implemented the method on top of the Java PathFinder model checker. Our experiments with this technique show promise of its applicability in speeding up program debugging. [ABSTRACT FROM AUTHOR]

Privacy and security concerns have adversely affected the usefulness of many types of techniques that leverage information gathered from deployed applications. To address this issue, we present an approach for automatically anonymizing failure-inducing inputs that builds on a previously developed technique. Given an input I that causes a failure f, our approach generates an anonymized input I′ that is different from I but still causes f. I′ can thus be sent to developers to enable them to debug f without having to know I. We implemented our approach in a prototype tool, camouflage, and performed an extensive empirical evaluation where we applied camouflage to a large set of failure-inducing inputs for several real applications. The results of the evaluation are promising, as they show that camouflage is both practical and effective at generating anonymized inputs; for the inputs that we considered, I and I′ shared no sensitive information. The results also show that our approach can outperform the general technique it extends. [ABSTRACT FROM AUTHOR]

Automating software testing activities can increase the quality and drastically decrease the cost of software development. Towards this direction various automated test data generation tools have been developed. The majority of them aim at branch testing, while a quite limited number aim at a higher level of testing thoroughness such as mutation. In this paper an automated framework that makes a joint use of diverse techniques and tools is introduced in the context of automating mutation based test generation. The motivation behind this work is the use of existing techniques and tools such as symbolic execution and evolutionary testing towards automating the test input generation activity according to the weak mutation testing criterion. The proposed framework integrates existing automated tools for branch testing in order to effectively generate mutation test data. To fulfill this suggestion three automated tools are used for illustration purposes and preliminary results are obtained by applying the proposed framework to a set of java program units indicating the applicability and effectiveness of the proposed approach. [ABSTRACT FROM AUTHOR]

Software has bugs, and fixing those bugs pervades the software engineering process. It is folklore that bug fixes are often buggy themselves, resulting in bad fixes, either failing to fix a bug or creating new bugs. To confirm this folklore, we explored bug databases of the Ant, AspectJ, and Rhino projects, and found that bad fixes comprise as much as 9% of all bugs. Thus, detecting and correcting bad fixes is important for improving the quality and reliability of software. However, no prior work has systematically considered this bad fix problem, which this paper introduces and formalizes. In particular, the paper formalizes two criteria to determine whether a fix resolves a bug: coverage and disruption. The coverage of a fix measures the extent to which the fix correctly handles all inputs that may trigger a bug, while disruption measures the deviations from the program's intended behavior after the application of a fix. This paper also introduces a novel notion of distance-bounded weakest precondition as the basis for the developed practical techniques to compute the coverage and disruption of a fix. To validate our approach, we implemented Fixation, a prototype that automatically detects bad fixes for Java programs. When it detects a bad fix, Fixation returns an input that still triggers the bug or reports a newly introduced bug. Programmers can then use that bug-triggering input to refine or reformulate their fix. We manually extracted fixes drawn from real-world projects and evaluated Fixation against them: Fixation successfully detected the extracted bad fixes. [ABSTRACT FROM AUTHOR]

This paper describes Juzi, a tool for automatic repair of complex data structures. Juzi takes a Java class representing the data structure as well as a predicate method that specifies the structural integrity constraints as inputs. Juzi instruments its inputs and generates a new Java class which behaves similarly to the original class, yet automatically repairs itself when the structural integrity constraints are violated. Juzi implements a novel repair algorithm. Given a structure that violates its integrity constraints, Juzi performs a systematic search based on symbolic execution to repair the structure, i.e., mutate it such that the resulting structure satisfies the given constraints. Experiments on structures ranging from library classes to standalone applications, show that Juzi repairs complex structures while enabling programs to recover from erroneous executions caused by data structure corruptions. [ABSTRACT FROM AUTHOR]

This paper describes Juzi, a tool for automatic repair of complex data structures. Juzi takes a Java class representing the data structure as well as a predicate method that specifies the structural integrity constraints as inputs. Juzi instruments its inputs and generates a new Java class which behaves similarly to the original class, yet automatically repairs itself when the structural integrity constraints are violated. Juzi implements a novel repair algorithm. Given a structure that violates its integrity constraints, Juzi performs a systematic search based on symbolic execution to repair the structure, i.e., mutate it such that the resulting structure satisfies the given constraints. Experiments on structures ranging from library classes to standalone applications, show that Juzi repairs complex structures while enabling programs to recover from erroneous executions caused by data structure corruptions. [ABSTRACT FROM AUTHOR]

This paper describes Juzi, a tool for automatic repair of complex data structures. Juzi takes a Java class representing the data structure as well as a predicate method that specifies the structural integrity constraints as inputs. Juzi instruments its inputs and generates a new Java class which behaves similarly to the original class, yet automatically repairs itself when the structural integrity constraints are violated. Juzi implements a novel repair algorithm. Given a structure that violates its integrity constraints, Juzi performs a systematic search based on symbolic execution to repair the structure, i.e., mutate it such that the resulting structure satisfies the given constraints. Experiments on structures ranging from library classes to standalone applications, show that Juzi repairs complex structures while enabling programs to recover from erroneous executions caused by data structure corruptions. [ABSTRACT FROM AUTHOR]

While Graphical User Interfaces (GUIs) have become ubiquitous, testing them remains largely ad-hoc. Since the state of a GUI is defined by a sequence of events on the GUI's widgets, a test input for a GUT is such an event sequence. Due to the combinatorial nature of the sequences, testing a GUT thoroughly is problematic and time-consuming. Moreover, the wide range of possible values for certain GUT widgets, such as a textbox, compounds the problem. This paper presents a novel test generation approach based on symbolic execution to obtain data inputs and enumerate event sequences that are likely to maximize code coverage of a GUI application. Key contributions are introducing the technique of symbolic execution in GUT testing (addressing a common weakness of traditional GUI testing frameworks) and performing symbolic execution over strings (in addition to primitives). Doing so minimizes the number of event sequences that form the resulting test suite. To determine feasibility of path conditions that arise in symbolic execution, we implement a solver for constraints over strings (in addition to primitives). We evaluate our test generation approach. [ABSTRACT FROM AUTHOR]

We present Java StarFinder (JSF), a tool for automated test case generation and error detection for Java programs having inputs in the form of complex heap-manipulating data structures. The core of JSF is a symbolic execution engine that uses separation logic with existential quantifiers and inductively-defined predicates to precisely represent the (unbounded) symbolic heap. The feasibility of a heap configuration is checked by a satisfiability solver for separation logic. At the end of each feasible path, a concrete model of the symbolic heap (returned by the solver) is used to generate a test case, e.g., a linked list or an AVL tree, that exercises that path. We show the effectiveness of JSF by applying it on non-trivial heap-manipulating programs and evaluated it against JBSE, a state-of-the-art symbolic execution engine for heap-based programs. Experimental results show that our tool significantly reduces the number of invalid test inputs and improves the test coverage. [ABSTRACT FROM AUTHOR]

Compiler optimizations influence the effectiveness and efficiency of symbolic execution. In this extended abstract, we report our recent results of recommending compiler optimizations for symbolic execution w.r.t. MC/DC coverage. We carried out extensive experiments to study the influence of compiler optimizations on MC/DC coverage. Then, an SVM-based optimization recommendation method is designed and implementation. The preliminary experimental results are promising. [ABSTRACT FROM AUTHOR]

Static analysis is a great approach to find bugs and code smells. Some of the errors span across multiple translation units. Unfortunately, it is challenging to achieve cross translation unit analysis for C family languages. In this short paper, we describe a model and an implementation for cross translation unit (CTU) symbolic execution for C. We were able to extend the scope of the analysis without modifying any of the existing checks. The analysis is implemented in the open source Clang compiler. We also measured the performance of the approach and the quality of the reports. The implementation is already accepted into mainline Clang. [ABSTRACT FROM AUTHOR]

Unit testing has been widely recognized as an important and valuable means of improving software reliability, as it exposes bugs early in the software development life cycle. However, manual unit testing is often tedious and insufficient. Testing tools can be used to enable economical use of resources by reducing manual effort. Recently parameterized unit testing has emerged as a very promising and effective methodology to allow the separation of two testing concerns or tasks: the specification of external, black-box behavior (i.e., assertions or specifications) by developers and the generation and selection of internal, white-box test inputs (i.e., high-code-covering test inputs) by tools. A parameterized unit test (PUT) is simply a test method that takes parameters, calls the code under test, and states assertions. PUTs have been supported by various testing frameworks. Various open source and industrial testing tools also exist to generate test inputs for PUTs. This tutorial presents latest research on principles and techniques, as well as practical considerations to apply parameterized unit testing on real-world programs, highlighting success stories, research and education achievements, and future research directions in developer testing. The tutorial will help improve developer skills and knowledge for writing PUTs and give overview of tool automation in supporting PUTs. Attendees will acquire the skills and knowledge needed to perform research or conduct practice in the field of developer testing and to integrate developer testing techniques in their own research, practice, and education. [ABSTRACT FROM AUTHOR]