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

deepspec-2019-papers
14:00 - 15:15: DeepSpec 2019 - Verifying All the Things at 106B
Chair(s): Zhong ShaoYale University
deepspec-2019-papers14:00 - 14:45
Talk
Ben LaurieGoogle Research
deepspec-2019-papers14:45 - 15:15
Talk
Jérémie KoenigYale University