CAREER: Fuzzing Formal Specifications

University Of Maryland, College Park, College Park MD

Investigators

Abstract

Formal specifications can serve as the foundation of strong safety and security guarantees by precisely describing the behavior of a program. However, they are underutilized in practice, being perceived as complex and cost-ineffective. The goal of this project is to use randomized testing (fuzzing) to make it easier to write, debug, and reason about specifications. The project's novelties are: studying the theory and practice of fuzzing with high-level specifications that traditionally operate on highly structured and highly constrained data; developing a theory of feedback-based generation of such data; and streamlining the evaluation of how these (and future) techniques perform in practice. The project's impacts are increased developer productivity and software quality, rendering the benefits of specifications accessible to more programmers through a combined research and educational effort. The project targets the problem of generating random structured test data with semantic constraints, with a particular focus on two synergistic thrusts: (1) how to make the most out of every test run by gathering additional information and revealing which tests led to previously unseen or otherwise interesting behavior; and (2) how to mutate such tests while staying within the structural and semantic constraints imposed, maximizing the chance to uncover errors. Techniques developed in this project will be evaluated by constructing a benchmark suite of functional programs with ground truth, as well as by carrying out an extended empirical evaluation of their effectiveness in an educational setting. 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.