SHF: Small: Inferring Specifications for Blackbox Code

University Of Pennsylvania, Philadelphia PA

Investigators

Abstract

Writing error-free computer software is notoriously difficult. Yet, software errors (bugs) can have catastrophic consequences, ranging from loss of user data and security vulnerabilities to loss of property and even loss of life. Thus, designing tools that help software developers identify and fix bugs is of critical importance. The goal of this project is to contribute to the development of these kinds of tools. In particular, a key challenge faced by all such tools is the need for specifications that describe the properties of software libraries shared among many applications. Often, without these specifications, the library code cannot be analyzed, substantially diminishing the usefulness of bug-finding tools. This project's novelty lies in the development of algorithms that use machine learning to automatically infer these kinds of specifications. The project outcomes will substantially improve the usefulness of bug-finding tools, thereby reducing the number of bugs in software. As a part of this project, the researchers design novel and general algorithms for inferring specifications for blackbox code (i.e., code that can be executed but not instrumented or analyzed). Focusing on the blackbox setting ensures that the algorithms will work in a broad range of settings, ranging from native code to code only available over a network connection. These algorithms infer specifications by executing the code on carefully chosen inputs, observing the corresponding output, and then generalizing the observed behaviors to specifications. Furthermore, to improve performance, these algorithms use reinforcement-learning to automatically learn domain-specific search strategies, eliminating the need for end users to manually design heuristic search strategies for their problem domain. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.