Completed
EADD pseudocode
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Systems & Networks Seminar - Andrew Bauman - Komodo: Using Verification to Disentangle Secure-Enclave Hardware from Software
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Intel SGX
- 3 SGX is complex
- 4 EADD pseudocode
- 5 EINIT pseudocode
- 6 SGX limitations
- 7 Example: memory management
- 8 The fundamental problem
- 9 Project Komodo
- 10 Komodo architecture
- 11 Prototype on ARM TrustZone
- 12 Komodo API
- 13 Verification overview
- 14 Proving security via non-interference
- 15 Verified assembly in Vale
- 16 Implementation
- 17 Notary performance
- 18 Verification effort
- 19 Experiences
- 20 Related work
- 21 Future work
- 22 Conclusion
