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

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 (opens in new tab). The formal specification, prototype, and proofs are available at GitHub (opens in new tab).