Synthesis of Safe Pointer-Manipulating Programs


Nadia Polikarpova, Assistant Professor of Computer Science and Engineering, University of California San Diego
Deian Stefan, Assistant Professor of Computer Science and Engineering, University of California San Diego
Monday, December 3, 2018 @ 11:00am
Room 1202, CSE Building


Nadia: Synthesis of Safe Pointer-Manipulating Programs

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 form 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.

Deian: When Sandboxing Is Not Enough

Modern Web browsers, such as Firefox, rely on dozens of fine-tuned, third-party libraries: libjpeg, libpng, etc. Unfortunately, when incorporating such third-party libraries, applications also incorporate the bugs that come with them---bugs that are often exploitable and can be used to bypass application-level guarantees (e.g., the same-origin policy). Worse yet, simply sandboxing libraries using existing techniques doesn't work: a compromised library can easily break out of the sandbox by abusing the application code that interfaces with the library. In this talk I will describe a new robust library sandboxing technique (RLBox) that bridges this gap. RLBox, at once, ensures that (1) library code is sandboxed and (2) application code fails to type check unless it's robust against malicious library behavior. In the talk I will describe the design of RLBox and our experience sandboxing libraries in the Firefox web browser.



Nadia Polikarpova is an assistant professor at CSE, and a member of the Programming Systems group. She received her Ph.D. in computer science from ETH Zurich in 2014. She then spent three years as a postdoctoral researcher at MIT. Dr. Polikarpova's work spans the areas of programming languages and formal methods; in particular, she is interested in building practical tools and techniques that make it easier for programmers to construct secure and reliable software.

Deian Stefan is an Assistant Professor in the CSE department at UC San Diego. He is also the Chief Scientist at Intrinsic (formerly GitStar), a web security startup he co-founded. Stefan’s research interests are in building principled and practical secure systems. More broadly, he is interested in research that spans systems, security, and programming languages. He works on several systems, including COWL , a browser confinement system designed for modern web applications, Hails , a security-centric framework for building web platforms, LIO , a dynamic information flow control system, and ESpectro , a security architecture for Node.js. At Intrinsic, Stefan puts much of this research into practice by building systems, tools and languages that ultimately make it easier for developers to build and deploy web applications with minimal trust. Stefan completed his Ph.D. in Computer Science at Stanford, and did his undergraduate and Master’s degrees at Cooper Union in Electrical Engineering. He remains interested in hardware architectures, especially in the context of security.