E. Alkassar & W. Paul (2008):
On the verification of a "baby" hypervisor for a RISC machine; draft 0.
available online.
Paul Barham, Boris Dragovic, Keir Fraser, Steven Hand, Tim Harris, Alex Ho, Rolf Neugebauer, Ian Pratt & Andrew Warfield (2003):
Xen and the art of virtualization.
In: SOSP '03: Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles.
ACM,
New York, NY, USA,
pp. 164–177,
doi:10.1145/945445.945462.
William R. Bevier, Warren A. Hunt, Jr., J S. Moore & William D. Young (1989):
An Approach to System Verification.
Journal of Automated Reasoning 5(4),
pp. 411–428.
Sven Beyer, Christian Jacobi, Daniel Kroning, Dirk Leinenbach & Wolfgang J. Paul (2006):
Putting it all together: Formal verification of the VAMP.
International Journal on Software Tools Technology Transfer 8(4),
pp. 411–430,
doi:10.1007/s10009-006-0204-6.
Randal E. Bryant & David O'Hallaron (2003):
Computer Systems: A Programmer's Perspective.
Prentice-Hall,
Upper Saddle River, N.J..
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte & Stephan Tobies (2009):
VCC: A Practical System for Verifying Concurrent C.
In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics,
TPHOLs '09.
Springer-Verlag,
Berlin, Heidelberg,
pp. 23–42,
doi:10.1007/978-3-642-03359-9_2.
Jason Franklin, Arvind Seshadri, Ning Qu, Sagar Chaki & Anupam Datta (2008):
Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor.
submitted to 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08).
David S. Hardin, Eric W. Smith & William D. Young (2006):
A Robust Machine Code Proof Framework for Highly Secure Applications.
In: Proceeding of the 2006 International Workshop on ACL2.
ACM.
(2006):
JOS Operating System.
http://pdos.csail.mit.edu/6.828/2006/overview.html.
M. Kaufmann, P. Manolios & J Moore (2000):
Computer-Aided Reasoning: An Approach.
Kluwer Academic Press,
Boston,
doi:10.1007/978-1-4615-4449-4.
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch & Simon Winwood (2009):
seL4: formal verification of an OS kernel.
In: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles,
SOSP '09.
ACM,
New York,
pp. 207–220,
doi:10.1145/1743546.1743574.
KVM (2011):
Kernel Based Virtual Machine.
www.linux-kvm.org/page/Main_Page.
Rebekah Leslie, Levent Erkök & Flemming Andersen (2007):
Formalizing Information Flow in a Haskell Hypervisor.
In: Microkernels and Embedded Systems Workshop, MIKES'07.
J. Matthews, J S. Moore, S. Ray & D. Vroon (2006):
Verification Condition Generation Via Theorem Proving.
In: M. Hermann & A. Voronkov: Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2006),
LNCS 4246.
Springer,
Phnom Penh, Cambodia,
pp. 362–376,
doi:10.1.1.101.503.
J. McDermott, J. Kirby, B. Montrose, T. Johnson & M. Kang (2008):
Re-engineering Xen internals for higher-assurance security.
Information Security Technical Report 13(1),
pp. 17–24,
doi:10.1016/j.istr.2008.01.001.
John McDermott & Leo Freitas (2008):
A formal security policy for Xenon.
In: FMSE '08: Proceedings of the 6th ACM workshop on Formal methods in security engineering.
ACM,
New York, NY, USA,
pp. 43–52,
doi:10.1145/1456396.1456401.
J S. Moore (2003):
Inductive Assertions and Operational Semantics.
In: CHARME 2003, Volume 2860 of LNCS.
Springer-Verlag,
pp. 289–303,
doi:10.1007/s10009-005-0180-2.
Sandip Ray (2005):
Using Theorem Proving and Algorithmic Design Procedures for Large-Scale System Verification.
University of Texas at Austin.
A. Roscoe, J. Woodcock & L. Wulf (1997):
Non-interference through nondeterminism.
In: Proceedings ESORICS,
pp. 33–52.
Arvind Seshadri, Mark Luk, Ning Qu & Adrian Perrig (2007):
SecVisor: A Tiny Hypervisor to Provide Lifetime Kernel Code Integrity for Commodity OSes.
In: SOSP '07: Proceedings of Twenty-first ACM SIGOPS Symposium on Operating Systems Principles.
ACM,
pp. 335–350,
doi:10.1145/1323293.1294294.
James E. Smith & Ravi Nair (2005):
Virtual Machines: Versatile Platforms for Systems and Processes.
Morgan Kaufmann,
Boston.
Hendrik Tews, Bart Jacobs, Erik Poll, Marko van Eekelen & Peter van Rossum (2005):
Specification and Verification of the Nova microhypervisor.
Project Robin deliverable D.6.
Radboud University Nijmegen.