Synthesis of Safe Pointer-Manipulating Programs - Nadia Polikarpova
Workshop on Dependable and Secure Software Systems 2021
Low-level pointer-manipulating programs form the backbone of our digital infrastructure. Unfortunately, they are susceptible to memory safety bugs, such as buffer overflows and use-after-free, which lead to crashes and security vulnerabilities. A promising approach to eliminating memory safety bugs is to use program synthesis technology to generate provably safe low-level code automatically from high-level specifications. In this talk I will present a program synthesizer SuSLik, which accepts a logical specification as input, and produces a provably safe C program as output. SuSLik is the first synthesizer capable of generating a wide range of operations on linked data structures (such as singly- and doubly-linked lists, sorted lists, and trees) without additional hints from the user. To make this possible, SuSLik relies on a novel proof system—synthetic separation logic—to derive correct-by-construction programs directly from their specifications.