Komodo: Using verification to disentangle secure-enclave hardware from software

Established: March 1, 2016

Komodo is a formally-verified reference monitor for an attested, secure isolated execution environment (“enclave”) on ARM TrustZone. It illustrates an alternative approach to Intel’s SGX, achieving similar security guarantees through formal verification, and allowing enclave features to evolve independently of the underlying hardware.

Komodo is described by our paper in SOSP’17. The formal specification, prototype, and proofs are available at GitHub.



Portrait of Andrew Baumann

Andrew Baumann

Principal Researcher

Portrait of Andrew Ferraiuolo

Andrew Ferraiuolo

Student / Former intern

Cornell University

Portrait of Chris Hawblitzel

Chris Hawblitzel

Senior Researcher

Portrait of Bryan Parno

Bryan Parno

Associate Professor, Carnegie Mellon University