Formally verified implementation of an idealized model of virtualization

DOI10.4230/LIPICS.TYPES.2013.45MaRDI QIDQ2968409zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Gustavo Betarte, Jesús Mauricio Chimento, Carlos Luna, Juan Diego Campo

Publication date 13 March 2017

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2014/4625/

zbMATH Keywords

cacheerror managementexecutable specificationisolationTLBvirtualization

Mathematics Subject Classification ID

Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Parametric verification of address space separation
• Formal memory models for the verification of low-level operating-system code
• Machine assisted proof of ARMv7 instruction level isolation properties
• Deep specifications and certified abstraction layers
• System-level non-interference of constant-time cryptography. I: Model

Cited in

(8)

• Formal verification of integrity-preserving countermeasures against cache storage side-channels
• System-level non-interference of constant-time cryptography. I: Model
• An impossibility result for virtual implementation with status quo
• Deep specifications and certified abstraction layers
• Parametric verification of address space separation
• High performance and secure device virtualization model on X86 platform
• Compositional verification of a baby virtual memory manager
• Verifying Secure Speculation in Isabelle/HOL

This page was built for publication: Formally verified implementation of an idealized model of virtualization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2968409)