Specification and Verification of Strong Timing Isolation of Hardware Enclaves
Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, Adam J. Chlipala · 2024
The process isolation enforceable by commodity hardware and operating systems is too weak to protect secrets from malicious code running on the same machine: attacks exploit timing side channels derived from contention on shared microarchitectural resources to extract secrets. With appropriate hardware support, however, we can construct isolated enclaves and safeguard independent processes from interference through timing side channels, a step towards confidentiality and integrity guarantees.