Securing Interruptible Enclaves
summary
Proves that adding interrupts to an enclave can be secure by modeling an ideal interrupt-free language and a realistic low-level language and proving full abstraction proof (preservation + reflection) between them; case study targets Sancus on a TI 16-bit MCU with 64 KB split memory, no cache/speculation, and an attacker modeled as a deterministic automaton that schedules interrupts and has severely limited memory. Implementation requires register erasure and protected saved state, forbids direct device interaction, and the proof closes but leaves speculative-execution composition open.
AI-written summary · about
chapters (5)
- 0:00Start
- 0:20The problem with isolation mechanisms
- 8:36Our model in a nutshell
- 10:11Who are the attackers?
- 16:20Future work
related talks
28mSanctum: Minimal Hardware Extensions for Strong Software Isolation
25mAutomatic Inference of Enclave Placement in LLVM Compiler
23mMorello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…)
38mOne Ring -3 To Secure Them All: Computing with Hardware Enclaves
16mMitigating Transient-Execution Attacks with CHERI Compartments
23mRISC V Enclaves A Clean Slate Approach To Linux Security
19mRethinking Isolation Mechanisms for Datacenter Multitenancy
25mTelling Your Secrets without Page Faults...