Improving Symbolic Execution via Targeted Program Transformations

Dynamic symbolic execution (DSE) has gained tremendous popularity in the last decade, becoming part of the standard toolbox of techniques in many computer science fields including software engineering, programming languages, software testing, verification, security, and computer systems. The technique has enabled a wide range of applications, including the automatic detection of bugs and security vulnerabilities, recovery of corrupt documents, patch generation, and automatic debugging, among many others.

The effectiveness and scalability of DSE is highly dependent on the structure of the program. That is, semantically-equivalent programs can differ substantially with respect to the effectiveness of DSE to explore the program state space. As a result, this project aims to discover and design automatic semantics-preserving program transformations that improve the scalability of DSE.

The primary non-academic beneficiaries of the proposed research are software companies and the open-source software community. It is well known that software bugs have a large negative impact on the global economy. For example, a report published by the US National Institute of Standards and Technology (NIST) in 2002 found that software bugs cost annually the US economy an estimated $60 billion dollars or 0.6 percent of the gross domestic product, and a recent study from the University of Cambridge estimated the worldwide cost of debugging at $312 billion dollars per year.

As a result, we are witnessing a sustained effort directed toward developing automatic techniques for finding software errors. The current generation of commercial tools use static analysis technology, i.e. they try to find bugs by inspecting the program source code, without actually running the program. While helpful, static analysis is limited in the types of bugs that it can find (e.g., none of the static analysis products on the market today could find the recent Heartbleed vulnerability) and produces false reports, which limits its usefulness. For an additional overhead many times acceptable in practice, dynamic symbolic execution (DSE) can often overcome these limitations, and has already shown promise in industry, with many corporations such as IBM, Fujitsu and Microsoft using it internally. However, DSE still presents significant scalability challenges, which prevent its widespread adoption. This research project could bring significant scalability improvements to DSE, potentially leading to large reductions in the costs associated with software errors and debugging.

Our goal is to disseminate the results of this research from an early stage onwards through a variety of mechanisms: (1) by open-sourcing most of our code to be used directly by software developers on their code; (2) by applying these prototypes to open-source applications to demonstrate the effectiveness of our approach; (3) by communicating the results of our research to the non-academic user community via meetings, extended visits and an engagement workshop; (4) by considering commercialisation opportunities and (5) by teaching and training.