University of California, San Diego
(joint with LICS)
Title: Synthesis of Safe Pointer-Manipulating Programs
Low-level pointer-manipulating code is ubiquitous in operating systems, networking stacks, and browsers, which form the backbone of our digital infrastructure.
Unfortunately, this code is susceptible to many kinds of bugs, which lead to crashes and security vulnerabilities. Read More
In this talk I will present a program synthesizer SuSLik, which accepts as input a specification written in separation logic, and produces as output a provably correct C program. SuSLik is the first synthesizer capable of generating a wide range of operations on linked data structures (such as singly- and doubly-linked lists, binary trees, and rose trees) without additional hints from the user. It is also the first synthesizer to automatically discover recursive auxiliary functions required for nested data structure traversal. To make this possible, SuSLik relies on a novel proof system-synthetic separation logic-to derive correct-by-construction programs directly from their specifications. Program proofs generated by SuSLik can be automatically translated into three foundational verification frameworks embedded in Coq: Hoare Type Theory (HTT), Iris, and Verified Software Toolchain (VST).
University of Sheffield
Title: Bounded-Deducibility Security
Starting from 2013, together with colleagues I have developed a framework for the specification and verification of information-flow security. The framework is called Bounded-Deducibility (BD) Security because it generalises Sutherland’s notion of Nondeducibility: from entirely preventing to only bounding the allowed flows of information. It was born from the challenges of expressing fine-grained confidentiality policies, as required by many multi-user web-based systems.Read More
BD Security was formalised in the proof assistant Isabelle/HOL and was used for verifying desirable confidentiality aspects of some running systems: CoCon, a practical conference management system that was deployed for two international conferences (one of them being the 2016 edition of ITP), CoSMed, a prototype social media platform, and CoSMeDis, a distributed extension of CoSMed (the last two developed in collaboration with a social media company). These systems were implemented from the ground up with verifiability in mind, using Isabelle/HOL’s specification language and code generator.
In this talk, I will describe the design principles behind BD Security and the eventful journey of deploying this framework to verify running systems. I will also discuss newer developments that further extend the framework’s flexibility and improve the resilience of verification code under system extensions with new features.
Several colleagues have participated in various parts of this work:
Thomas Bauereiss, Sergey Grebenshchikov, Ping Hou, Peter Lammich, Sudeep Kanav, Ondrej Kuncar, Armando Pesenti Gritti and Franco Raimondi.
Title: The CakeML Project’s Quest for Ever Stronger Correctness Theorems
The CakeML project has developed a proof-producing code generation
mechanism for HOL4, a verified compiler for ML and, using these, a number of verified application programs that are proved correct down to the machine code that runs them. Read More
In this talk, I will tell the story behind the project, point curious listerners to papers where they can read more about specific parts; and I will share some thoughts on where the
project might go next.