Abstract
Efforts to validate the Microsoft Hypervisor – a low-level program that partitions a real MP machine into a a number of virtual MP pachines – has led to some interesting formal methods developments. We’ll survey some of these, including
– new algorithms for “optimal” stateless search and symbolic stateless search;
– techniques to make stateless search practical for shared memory programs, including efficient shared memory instrumentation and optimal trace replay using breakpoints;
– new techniques for model-based test generation, including the use of symbolic execution to eliminate redundancy and methods to handle invisible internal nondeterminism;
– formal models of the x86/x64 TLB and cache systems;
– verification of algorithms for efficient MP TLB virtualization, which has uncovered subtle design bugs;
– formal analyses of memory sharing between mutually distrustful partitions, which has revealed some surprising cache attacks;
– techniques for eliminating inductive constructs in first-order verification;
– techniques for specifying and reasoning about C code.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cohen, E. (2006). Validating the Microsoft Hypervisor. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_6
Download citation
DOI: https://doi.org/10.1007/11813040_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37215-8
Online ISBN: 978-3-540-37216-5
eBook Packages: Computer ScienceComputer Science (R0)