The process isolation enforceable by commodity hardware and operating systems is too weak to protect secrets from malicious code running on the same machine: Spectre-era 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 necessary step towards integrity and confidentiality guarantees.
In this paper, we describe our work on formally specifying and verifying that a synthesizable hardware architecture implements strong timing isolation for enclaves. We reason about the cycle-accurate semantics of circuits with respect to a trustworthy formulation of strong isolation based on "air-gapped machines" and develop a modular proof strategy that sidesteps the need to prove functionalf correctness of processors. We apply our method on a synthesizable, multicore, pipelined RISC-V design formalized in Coq.