Securing Interruptible Enclaves

Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken the isolation that these mechanisms offer. Extending a processor with new (micro-)architectural features brings a risk of enabling new such side-channel attacks. In particular, interrupt-based attacks are very effective in breaking confidentiality and integrity of code and data in enclaves, i.e., protected memory regions. An attacker capable of raising interrupts at will, and of managing them can observe different timings of enclaved executions, so possibly breaking isolation. Here, we outline our work in extending a microprocessor with carefully designed interruptible enclaves emph{without} weakening security. We started from the existing Sancus platform that supports non-interruptible enclaved execution and we extend it with interrupts. To obtain strong security guarantees, we formalize both versions of Sancus and we prove them fully abstract. Roughly, our full abstraction theorem guarantees that the attacker gains exactly}the same information without and with interrupts: adding interruptibility opens no new avenues of attack. Our result is reflected in the implementation of the secure interrupt handling mechanism in Sancus -- actually this required back-and-forth interactions for tuning the formalization and the implementation.