Google Research

Komodo: Using Verification to Disentangle Secure-enclave Hardware from Software

Proceedings of the 26th Symposium on Operating Systems Principles (2017), pp. 287-305

Abstract

Intel SGX promises powerful security: an arbitrary number of user-mode enclaves protected against both physical attacks and privileged software adversaries. However, to achieve this security, Intel extended the x86 architecture with an isolation mechanism approaching the complexity of an OS microkernel, implemented by an inscrutable mix of silicon and microcode. While hardware-based security can improve performance and offer features that are difficult or impossible to achieve in pure software, hardware-only solutions are difficult to update, either to patch security flaws or introduce new features. Such updates are dependent on the slowing deployment of new CPUs - 2.5 years after the specification of SGXv2, there is no announced implementation.This paper presents Komodo, which illustrates an alternative approach to achieving attested, on-demand, user-mode, concurrent isolated execution. We decouple the core underlying hardware mechanisms such as memory encryption, address-space isolation and attestation from a privileged software monitor that in turn implements enclaves. The monitor's correctness is ensured by a machine-checkable proof of both functional correctness and high-level security properties of enclave integrity and confidentiality. We show that the approach is both practical and performant with a concrete implementation of a Komodo prototype in verified assembly code on an ARM TrustZone platform. Our ultimate goal is to achieve security that is equivalent to or better than SGX while decoupling the enclave implementation from the underlying hardware, and enabling the deployment of new enclave features independently of CPU upgrades.

Learn more about how we do research

We maintain a portfolio of research projects, providing individuals and teams the freedom to emphasize specific types of work