SHF: Small: NSF-BSF: Synthesis of Safe Pointer-Manipulating Programs

University Of California-San Diego, La Jolla CA

Investigators

Abstract

Low-level pointer-manipulating programs form the backbone of our digital infrastructure: web browsers, operating systems, and cryptographic libraries are all implemented in low-level languages like C. These programs are both expensive to develop and susceptible to memory-safety bugs, which lead to crashes and security vulnerabilities, such as the infamous Heartbleed bug. This project's impact is to address both the cost and the safety issue at the same time, by generating low-level code automatically from high-level specifications in a way that guarantees absence of memory-safety bugs. This project's novelty is to advance the state of the art in program synthesis by developing a new synthesis technique that is both efficient and capable of generating memory-safe pointer-manipulating code. Pointer-manipulating programs have been largely beyond the capabilities of the state-of-the-art program synthesizers due to the difficulty of reasoning automatically about their behavior and lack of structural constraints, such as strict typing, that are traditionally used to prune the search space the synthesizer has to explore. To enable efficient synthesis of safe pointer-manipulating programs, the investigators combine state-of-the-art program verification techniques based on separation logic with deductive program synthesis, a method for deriving provably correct programs directly from their specifications. This research addresses both challenges outlined above: (1) separation logic enables automatic reasoning about pointer-manipulating programs, and (2) deductive synthesis leverages the specification to preemptively prune unsafe programs from the search space. This approach is implemented in the SafeSpace synthesis framework, which accepts separation logic specifications as input, and produces C programs as output. 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.