Verifying Linearizability of Intel® Software Guard Extensions

Autor:	Caspi Dror, Matthew Fernandez, Rebekah M. Leslie-Hurd
Rok vydání:	2015
Předmět:	Model checking Guard (information security) Linearizability business.industry Computer science Usability computer.software_genre Rendering (computer graphics) Software Linearization Operating system Compiler business computer
Zdroj:	Computer Aided Verification ISBN: 9783319216676 CAV (2)
DOI:	10.1007/978-3-319-21668-3_9
Popis:	Intel® Software Guard Extensions (SGX) is a collection of CPU instructions that enable an application to create secure containers that are inaccessible to untrusted entities, including the operating system and other low-level software. Establishing that the design of these instructions provides security is critical to the success of the feature, however, SGX introduces complex concurrent interactions between the instructions and the shared hardware state used to enforce security, rendering traditional approaches to validation insufficient. In this paper, we introduce Accordion, a domain specific language and compiler for automatically verifying linearizability via model checking. The compiler determines an appropriate linearization point for each instruction, computes the required linearizability assertions, and supports experimentation with a variety of model configurations across multiple model checking tools. We show that this approach to verifying linearizability works well for validating SGX and that the compiler provides improved usability over encoding the problem in a model checker directly.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::75fff1b35bbb8ed4127fa0d84fc3cb7c https://doi.org/10.1007/978-3-319-21668-3_9 Zobrazit plný text záznamu