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.