Virtualization platforms allow multiple operating systems to run on the same hardware. One of their central goals is to provide strong isolation between guest operating systems; unfortunately, they are often vulnerable to practical side-channel attacks. Cache attacks are a common class of side-channel attacks that use the cache as a side channel.

We formalize an idealized model of virtualization that features the cache and the Translation Lookaside Buffer (TLB), and that provides an abstract treatment of cache-based side-channels. We then use the model for reasoning about cache-based attacks and countermeasures, and for proving that isolation between guest operating systems can be enforced by flushing the cache upon context switch.

In addition, we show that virtualized platforms are transparent, i.e. a guest operating system cannot distinguish whether it executes alone or together with other guest operating systems on the platform.

The models and proofs have been machine-checked in the Coq proof assistant.