Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization

Virtualization platforms allow multiple operating systems to run on the same hardware. One of their central goal 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-channe...

Full description

Saved in:
Bibliographic Details
Main Authors: Barthe, G., Betarte, G., Campo, J. D., Luna, C.
Format: Conference Proceeding
Language:English
Subjects:
Cache-leakage
Cognition
Computational modeling
Isolation
Memory management
Operating systems
Semantics
Switches
Transparency
Virtual machine monitors
Virtualization
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Virtualization platforms allow multiple operating systems to run on the same hardware. One of their central goal 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 Look aside 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 Coqproof assistant.
ISSN:1063-6900
2377-5459
DOI:10.1109/CSF.2012.17