References

  1. Advanced Micro Devices (2005): AMD64 virtualization: Secure virtual machine architecture reference manual. AMD Publication no. 33047 rev. 3.01.
  2. E. Alkassar & W. Paul (2008): On the verification of a "baby" hypervisor for a RISC machine; draft 0. available online.
  3. 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.
  4. 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.
  5. 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.
  6. Randal E. Bryant & David O'Hallaron (2003): Computer Systems: A Programmer's Perspective. Prentice-Hall, Upper Saddle River, N.J..
  7. 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.
  8. Intel Corporation (1999): Preboot Execution Environment, Verion 2.1. Technical Report. Intel Corporation.
  9. 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).
  10. 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.
  11. Kenneth Hess & Amy Newman (2010): Practical Virtualization Solutions. Pearson Education, Boston.
  12. Sarah Hoffmann (2003): Formalising PC Hardware: A Model of the x86 Architecture. Technische Universitat Dresden.
  13. Intel Corporation (2006): LaGrande technology preliminary architecture specification. Intel Publication no. D52212.
  14. (2006): JOS Operating System. http://pdos.csail.mit.edu/6.828/2006/overview.html.
  15. M. Kaufmann, P. Manolios & J Moore (2000): Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston, doi:10.1007/978-1-4615-4449-4.
  16. 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.
  17. KVM (2011): Kernel Based Virtual Machine. www.linux-kvm.org/page/Main_Page.
  18. Rebekah Leslie, Levent Erkök & Flemming Andersen (2007): Formalizing Information Flow in a Haskell Hypervisor. In: Microkernels and Embedded Systems Workshop, MIKES'07.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. Sandip Ray (2005): Using Theorem Proving and Algorithmic Design Procedures for Large-Scale System Verification. University of Texas at Austin.
  24. A. Roscoe, J. Woodcock & L. Wulf (1997): Non-interference through nondeterminism. In: Proceedings ESORICS, pp. 33–52.
  25. 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.
  26. James E. Smith & Ravi Nair (2005): Virtual Machines: Versatile Platforms for Systems and Processes. Morgan Kaufmann, Boston.
  27. 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.
  28. Verisoft (2008): Verisoft Repository. www.verisoft.de/VerisoftRepository.html.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org