Document Open Access Logo

Formally Verified Implementation of an Idealized Model of Virtualization

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

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2013.45.pdf
  • Filesize: 0.52 MB
  • 19 pages

Document Identifiers

Author Details

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

Cite AsGet BibTex

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, and Carlos Luna. Formally Verified Implementation of an Idealized Model of Virtualization. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 45-63, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/LIPIcs.TYPES.2013.45

Abstract

VirtualCert is a machine-checked model of virtualization that can be used to reason about isolation between operating systems in presence of cache-based side-channels. In contrast to most prominent projects on operating systems verification, where such guarantees are proved directly on concrete implementations of hypervisors, VirtualCert abstracts away most implementations issues and specifies the effects of hypervisor actions axiomatically, in terms of preconditions and postconditions. Unfortunately, seemingly innocuous implementation issues are often relevant for security. Incorporating the treatment of errors into VirtualCert is therefore an important step towards strengthening the isolation theorems proved in earlier work. In this paper, we extend our earlier model with errors, and prove that isolation theorems still apply. In addition, we provide an executable specification of the hypervisor, and prove that it correctly implements the axiomatic model. The executable specification constitutes a first step towards a more realistic implementation of a hypervisor, and provides a useful tool for validating the axiomatic semantics developed in previous work.
Keywords
  • virtualization
  • Cache and TLB
  • Executable specification
  • Error management
  • Isolation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. June Andronick. Modélisation et Vérification Formelles de Systèmes Embarqués dans les Cartes à Microprocesseur - Plate-Forme Java Card et Système d'Exploitation. PhD thesis, Université Paris-Sud, 2006. Google Scholar
  2. Antonia Balaa and Yves Bertot. Fix-point equations for well-founded recursion in type theory. In Mark Aagaard and John Harrison, editors, TPHOLs, volume 1869 of LNCS, pages 1-16. Springer, 2000. Google Scholar
  3. P. Barham, B. Dragovic, K. Fraser, S. Hand, T. Harris, A. Ho, R. Neugebauer, I. Pratt, and A. Warfield. Xen and the art of virtualization. In SOSP'03: Proceedings of the 19th ACM Symposium on Operating Systems Principles, pages 164-177, New York, NY, USA, 2003. ACM Press. Google Scholar
  4. G. Barthe, G. Betarte, J. D. Campo, and C. Luna. Formally verifying isolation and availability in an idealized model of virtualization. In FM 2011, pages 231-245. Springer-Verlag, 2011. Google Scholar
  5. G. Barthe, G. Betarte, J. D. Campo, and C. Luna. Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. In CSF 2012, pages 186-197, 2012. Google Scholar
  6. G. Barthe, J. Forest, D. Pichardie, and V. Rusu. Defining and reasoning about recursive functions: A practical tool for the coq proof assistant. In M. Hagiya and P. Wadler, editors, FLOPS, volume 3945 of LNCS, pages 114-129. Springer, 2006. Google Scholar
  7. Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Formal certification of code-based cryptographic proofs. SIGPLAN Not., 44(1):90-101, January 2009. Google Scholar
  8. Stefan Berghofer, Lukas Bulwahn, and Florian Haftmann. Turning inductive into equational specifications. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, TPHOLs, volume 5674 of LNCS, pages 131-146. Springer, 2009. Google Scholar
  9. Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer-Verlag, 2004. Google Scholar
  10. G. Betarte, E. Giménez, C. Loiseaux, and B. Chetali. FORMAVIE: Formal Modeling and Verification of the Java Card 2.1.1 Security Architecture. In Proceedings of eSmart'02, 2002. Google Scholar
  11. Boutheina Chetali and Quang-Huy Nguyen. About the world-first smart card certificate with eal7 formal assurances. Slides 9th ICCC, Jeju, Korea, September 2008. Google Scholar
  12. M. R. Clarkson and F. B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157-1210, 2010. Google Scholar
  13. E. Cohen. Validating the microsoft hypervisor. In J. Misra, T. Nipkow, and E. Sekerinski, editors, FM'06, volume 4085 of LNCS, pages 81-81. Springer, 2006. Google Scholar
  14. Thierry Coquand and Gérard P. Huet. The calculus of constructions. Inf. Comput., 76(2/3):95-120, 1988. Google Scholar
  15. Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors, Conference on Computer Logic, volume 417 of Lecture Notes in Computer Science, pages 50-66. Springer, 1988. Google Scholar
  16. J.-Y. Hwang, S.-B. Suh, S.-K. Heo, C.-J. Park, J.-M. Ryu, S.-Y. Park, and C.-R. Kim. Xen on arm: System virtualization using xen hypervisor for arm-based secure mobile phones. In 5th IEEE Consumer and Communications Networking Conference, 2008. Google Scholar
  17. G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. Communications of the ACM (CACM), 53(6):107-115, June 2010. Google Scholar
  18. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an OS kernel. In SOSP 2009, pages 207-220. ACM, 2009. Google Scholar
  19. D. Leinenbach and T. Santen. Verifying the microsoft hyper-v hypervisor with vcc. In A. Cavalcanti and D. Dams, editors, FM 2009, volume 5850 of LNCS, pages 806-809. Springer, 2009. Google Scholar
  20. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52:107-115, July 2009. Google Scholar
  21. P. Letouzey. Programmation fonctionnelle certifiée - L'extraction de programmes dans l'assistant Coq. PhD thesis, Université Paris-Sud, July 2004. Google Scholar
  22. Pierre Letouzey. A New Extraction for Coq. In Herman Geuvers and Freek Wiedijk, editors, Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, volume 2646 of Lecture Notes in Computer Science. Springer-Verlag, 2003. Google Scholar
  23. Silvio Micali and Leonid Reyzin. Physically observable cryptography (extended abstract). In TCC 2004, pages 278-296, 2004. Google Scholar
  24. T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein. seL4: from General Purpose to a Proof of Information Flow Enforcement. In Proc. of the 2013 IEEE Symp. on Security and Privacy (SP'13), pages 415-429, 2013. Google Scholar
  25. David von Oheimb. Information flow control revisited: Noninfluence = Noninterference + Nonleakage. In P. Samarati, P. Ryan, D. Gollmann, and R. Molva, editors, Computer Security - ESORICS 2004, volume 3193 of LNCS, pages 225-243. Springer, 2004. Google Scholar
  26. David von Oheimb, Volkmar Lotz, and Georg Walter. Analyzing SLE 88 memory management security using Interacting State Machines. International Journal of Information Security, 4(3):155-171, 2005. Google Scholar
  27. C. Paulin-Mohring. Inductive definitions in the system coq - rules and properties. In M. Bezem and J. F. Groote, editors, 1st Int. Conf. on Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 328-345. Springer-Verlag, 1993. Google Scholar
  28. The VirtualCert project. Supporting Coq formalization. See URL: http://www.fing.edu.uy/inco/grupos/gsi/proyectos/virtualcert.php.
  29. Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, and Gerwin Klein. seL4 enforces integrity. In ITP 2011, Nijmegen, The Netherlands, 2011. Google Scholar
  30. Zhong Shao. Certified software. Commun. ACM, 53(12):56-66, 2010. Google Scholar
  31. The Coq Development Team. The Coq Proof Assistant Reference Manual, 2012. Google Scholar
  32. T. Terauchi and A. Aiken. Secure information flow as a safety problem. In C. Hankin and I. Siveroni, editors, Proceedings of SAS'05, volume 3672 of LNCS, pages 352-367. Springer-Verlag, 2005. Google Scholar
  33. Pierre-Nicolas Tollitte, David Delahaye, and Catherine Dubois. Producing certified functional code from inductive specifications. In Chris Hawblitzel and Dale Miller, editors, CPP, volume 7679 of LNCS, pages 76-91. Springer, 2012. Google Scholar
  34. Eran Tromer, Dag Arne Osvik, and Adi Shamir. Efficient cache attacks on AES, and countermeasures. J. Cryptology, 23(1):37-71, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact