Sun 23 Jun 2019 14:00 - 14:45 at 106B - Verifying All the Things Chair(s): Zhong Shao

The traditional answer to the question “how do I control data I have given to someone else?” is that you don’t. Advances in formal methods and the coming availability of strong isolation and remote attestation (aka enclaves) suggest that we may be able to change that answer. Project Oak is an open source project from Google Research that aims to show how that is possible. In short: data always lives in enclaves and only moves from one to another if there’s an assurance the policy associated with that data will be obeyed. In order to do that, we aim to formally verify properties of the entire stack: hardware, hypervisors, compilers, VMs, policy. Where we can’t use formal methods to provide verification, we’ll need to build an ecosystem of third parties who can do this work informally. But in the end, this is pointless if it is not usable, so we are also investing in user experience research from the outset.

Sun 23 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:15
Verifying All the ThingsDeepSpec at 106B
Chair(s): Zhong Shao Yale University
Project Oak: Control Data in Distributed Systems, Verify All The Things
Ben Laurie Google Research
Refinement-Based Game Semantics for CompCert
Jérémie Koenig Yale University