Enhanced Symbolic Execution for Improved Software Reliability

Software plays an important role in everyday life, from consumer applications to mission-critical systems. This richness of functionality, however, comes at the price of complexity. Even though software systems are developed manually, they are increasingly too complex to be fully understood by any single programmer. As a consequence, software bugs, which are often the result of programming errors, are commonplace.

In this talk we present two techniques based on dynamic symbolic execution which address the problem of software reliability from two angles: testing software patches and recovering an incorrect program input. Patch testing is a cornerstone of software quality. It helps to prevent introduction of bugs when software is being created, but also it helps to prevent introduction of new bugs along with bug fixes. We present shadow symbolic execution, a technique that generates test inputs exercising the new program behaviours introduced by a software patch.

In practice, even the best software quality measures cannot prevent bugs from escaping to the end-user and it is not always possible to develop and deploy the fix fast enough. Frequently, bugs are triggered by some unusual or an incorrect program input that causes program malfunction or makes the input contents inaccessible to the users. One of the most important and commonly used program input are electronic documents. We present Docovery, a novel input recovery technique applied to the domain of electronic documents, that makes it possible to fix broken documents without any knowledge of the file format.

We show how our two enhancements of dynamic symbolic execution can help to improve software quality during production and after deployment.

Tomasz Kuchta is a computer scientist and a software engineer. He conducted his PhD research in the Department of Computing, Imperial College London, working under the supervision of Dr Cristian Cadar in the Software Reliability Group; the position was generously sponsored by Microsoft Research. His research interests span across the areas of software engineering, software reliability, systems and security. In his research, he explored applications of dynamic symbolic execution technique to the problems of program input recovery and testing software patches. Prior to joining Imperial, Tomasz worked as a software engineer in the telecommunications industry and now he works in the security area. Tomasz holds an MSc degree from Cracow University of Technology.