Testing, Verifying, and Generating Software Patches Using Dynamic Symbolic Execution

A large fraction of the costs of developing and maintaining software is associated with detecting and fixing software errors. As a result, the last decade has seen a sustained research effort directed toward designing and developing techniques for automatically detecting software errors, with some of these techniques making their way into commercial and open-source tools. However, detecting an error is only the first step toward fixing it. In fact, many known errors remain unpatched due to the high cost required to diagnose and repair them, combined with the fear that patches are more likely to introduce failures compared to other types of code changes.

The goal of this research project is to address both of these problems, by devising novel techniques based on dynamic symbolic execution for:
(1) automatically testing and verifying the correctness of software patches, and
(2) (semi-)automatically generating candidate patches for software bugs.

The strength of dynamic symbolic execution lies in its ability to precisely model the behaviour of program paths using mathematical constraints. However, the cost associated with this level of precision is poor scalability. The number of paths in a program is usually exponential in the number of branches, which makes it difficult to scale the analysis to very large programs. However, by focusing the analysis on the incremental changes introduced by program patches, we hope to significantly reduce the cost of symbolic execution and significantly increase its applicability in practice. Furthermore, the ability to check software patches opens up the possibility of performing patch generation in an automatic or semi-automatic fashion. In particular, starting from the mathematical constraints gathered from a buggy execution path -- and with the potential addition of a manually-written patch template -- we plan to design techniques for generating a set of candidate patches resembling the ones that would be generated manually by developers.

Key Non-Academic Beneficiaries: 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 has found that software bugs cost annually the US economy an estimated $60 billion dollars or 0.6 percent of the gross domestic product [G. Tassey, The economic impacts of inadequate infrastructure for software testing, NIST 2002], and a similar impact is to be expected in other developed countries like the UK. A large fraction of this cost is associated with writing patches---either to fix existing bugs or to add new features---which is one of the critical software development and maintenance activities. This research project plans to investigate mechanisms for improving the quality of patches and for (partially) automating their development, which on the long term might bring significant economic benefits.

In addition to the commercial and open-source software development communities---who will directly benefit from improving the software patching process---the resulting increase in software quality will positively affect software users across a wide variety of industrial sectors. In particular, the NIST study cited above mentions the financial services and the automotive and aerospace industry as major sectors affected by software errors.

Mechanisms for Exploitation and Application: Our goal is to disseminate the results of this research from an early stage through a variety of mechanisms: (1) by applying it to open-source and commercial code to demonstrate the effectiveness of our approach; (2) by open-sourcing our initial prototype to be used directly by software developers on their code; and (3) by communicating the results of our research to the non-academic user community.

On the short-term, we will apply our technique to widely-used open-source software, and report any errors found to developers. Furthermore, we will send automatically generated patches to developers, use the feedback they provide response to these patches will be used to improve our techniques and associated prototype.

After the initial evaluation on open-source software, we plan to apply our approach to commercial code. We have already discussed our technique with Maxeler Technologies, who are interested in applying our initial prototype to their software (please see the attached letter of support). We also intend to seek further contacts with the software industry, in order to better assess the applicability of our technique, and in particular its integration into the development process.

One of the key ways in which we plan to disseminate our results to the user community is by releasing our initial prototype under an open-source license. This would allow developers from both the commercial and open-source communities to directly apply our technique to their code. Our previous experience releasing our tool KLEE (http://klee.llvm.org) as open-source software should prove beneficial in making sure that our prototype reaches a wide audience. (Since being open-sourced in June 2009, KLEE has been used and extended by a variety of users, with some of these extensions being contributed back to the main branch.)

Communicating the results of our research to a non-academic audience will play an important role in our dissemination strategy. In conjunction with open-sourcing our prototype system, we plan to set up a dedicated website for the project to introduce our research to a general audience. In a similar spirit, we plan to integrate our research into the PI's teaching activities, through group and individual projects offered to undergraduate and Master's students at Imperial College.