Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. Barthe, G., Betarte, G., Campo, J. D., & Luna, C. 2012. doi abstract bibtex 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.
@conference {barthe_cache-leakage_2012,
title = {Cache-Leakage Resilient {OS} Isolation in an Idealized Model of Virtualization},
booktitle = {Computer Security Foundations Symposium ({CSF)}, 2012 {IEEE} 25th},
year = {2012},
pages = {186{\textendash}197},
abstract = {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.},
keywords = {abstract treatment, cache attacks, cache storage, cache-based side-channels, Cache-leakage, cache-leakage resilient {OS} isolation, Cognition, Computational modeling, Coqproof assistant, guest operating systems, inference mechanisms, Isolation, Memory management, Operating systems, operating systems (computers), reasoning, security of data, Semantics, side-channel attacks, Switches, theorem proving, Translation Look aside Buffer, Transparency, Virtual machine monitors, virtualisation, Virtualization, virtualization platforms, {TLB}},
doi = {10.1109/CSF.2012.17},
author = {Barthe, G. and Gustavo Betarte and Campo, Juan Diego and Luna, Carlos}
}
Downloads: 0
{"_id":"7sCCBdftayEHhmGJu","bibbaseid":"barthe-betarte-campo-luna-cacheleakageresilientosisolationinanidealizedmodelofvirtualization-2012","downloads":0,"creationDate":"2017-11-14T02:09:30.981Z","title":"Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization","author_short":["Barthe, G.","Betarte, G.","Campo, J. D.","Luna, C."],"year":2012,"bibtype":"conference","biburl":"https://www.fing.edu.uy/~mscalone/Biblio-Bibtex.bib","bibdata":{"bibtype":"conference","type":"conference","title":"Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization","booktitle":"Computer Security Foundations Symposium (CSF), 2012 IEEE 25th","year":"2012","pages":"186\\textendash197","abstract":"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.","keywords":"abstract treatment, cache attacks, cache storage, cache-based side-channels, Cache-leakage, cache-leakage resilient OS isolation, Cognition, Computational modeling, Coqproof assistant, guest operating systems, inference mechanisms, Isolation, Memory management, Operating systems, operating systems (computers), reasoning, security of data, Semantics, side-channel attacks, Switches, theorem proving, Translation Look aside Buffer, Transparency, Virtual machine monitors, virtualisation, Virtualization, virtualization platforms, TLB","doi":"10.1109/CSF.2012.17","author":[{"propositions":[],"lastnames":["Barthe"],"firstnames":["G."],"suffixes":[]},{"firstnames":["Gustavo"],"propositions":[],"lastnames":["Betarte"],"suffixes":[]},{"propositions":[],"lastnames":["Campo"],"firstnames":["Juan","Diego"],"suffixes":[]},{"propositions":[],"lastnames":["Luna"],"firstnames":["Carlos"],"suffixes":[]}],"bibtex":"@conference {barthe_cache-leakage_2012,\n\ttitle = {Cache-Leakage Resilient {OS} Isolation in an Idealized Model of Virtualization},\n\tbooktitle = {Computer Security Foundations Symposium ({CSF)}, 2012 {IEEE} 25th},\n\tyear = {2012},\n\tpages = {186{\\textendash}197},\n\tabstract = {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.},\n\tkeywords = {abstract treatment, cache attacks, cache storage, cache-based side-channels, Cache-leakage, cache-leakage resilient {OS} isolation, Cognition, Computational modeling, Coqproof assistant, guest operating systems, inference mechanisms, Isolation, Memory management, Operating systems, operating systems (computers), reasoning, security of data, Semantics, side-channel attacks, Switches, theorem proving, Translation Look aside Buffer, Transparency, Virtual machine monitors, virtualisation, Virtualization, virtualization platforms, {TLB}},\n\tdoi = {10.1109/CSF.2012.17},\n\tauthor = {Barthe, G. and Gustavo Betarte and Campo, Juan Diego and Luna, Carlos}\n}\n","author_short":["Barthe, G.","Betarte, G.","Campo, J. D.","Luna, C."],"key":"barthe_cache-leakage_2012","id":"barthe_cache-leakage_2012","bibbaseid":"barthe-betarte-campo-luna-cacheleakageresilientosisolationinanidealizedmodelofvirtualization-2012","role":"author","urls":{},"keyword":["abstract treatment","cache attacks","cache storage","cache-based side-channels","Cache-leakage","cache-leakage resilient OS isolation","Cognition","Computational modeling","Coqproof assistant","guest operating systems","inference mechanisms","Isolation","Memory management","Operating systems","operating systems (computers)","reasoning","security of data","Semantics","side-channel attacks","Switches","theorem proving","Translation Look aside Buffer","Transparency","Virtual machine monitors","virtualisation","Virtualization","virtualization platforms","TLB"],"downloads":0},"search_terms":["cache","leakage","resilient","isolation","idealized","model","virtualization","barthe","betarte","campo","luna"],"keywords":["abstract treatment","cache attacks","cache storage","cache-based side-channels","cache-leakage","cache-leakage resilient os isolation","cognition","computational modeling","coqproof assistant","guest operating systems","inference mechanisms","isolation","memory management","operating systems","operating systems (computers)","reasoning","security of data","semantics","side-channel attacks","switches","theorem proving","translation look aside buffer","transparency","virtual machine monitors","virtualisation","virtualization","virtualization platforms","tlb"],"authorIDs":[],"dataSources":["huj7WmEoKzoYMwcB9"]}