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.