Systems & Networks Seminar - Andrew Bauman - Komodo: Using Verification to Disentangle Secure-Enclave Hardware from Software

Explore a systems and networks seminar featuring Andrew Baumann from Microsoft Research as he presents "Komodo: using verification to disentangle secure-enclave hardware from software." Dive into the complexities of Intel SGX and its promise of powerful security for user-mode enclaves. Learn about the challenges of hardware-based security solutions and their dependence on CPU deployments. Discover Komodo, an alternative approach to achieving attested, on-demand, user-mode, concurrent isolated execution by decoupling core hardware mechanisms from a privileged software monitor. Examine the implementation of a Komodo prototype in verified assembly code on an ARM TrustZone platform, showcasing its practicality and performance. Gain insights into the project's goal of achieving security equivalent to or better than SGX while enabling independent deployment of new enclave features. Delve into topics such as Intel SGX complexities, Komodo architecture, verification processes, and future work in this comprehensive lecture on secure enclave systems.

Intro
Intel SGX
SGX is complex
EADD pseudocode
EINIT pseudocode
SGX limitations
Example: memory management
The fundamental problem
Project Komodo
Komodo architecture
Prototype on ARM TrustZone
Komodo API
Verification overview
Proving security via non-interference
Verified assembly in Vale
Implementation
Notary performance
Verification effort
Experiences
Related work
Future work
Conclusion