Formal Pervasive Verification of a Paging Mechanism

  • Eyad Alkassar
  • Norbert Schirmer
  • Artem Starostin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


Memory virtualization by means of demand paging is a crucial component of every modern operating system. The formal verification is challenging since reasoning about the page fault handler has to cover two concurrent computational sources: the processor and the hard disk. We accurately model the interleaved executions of devices and the page fault handler, which is written in a high-level programming language with inline assembler portions. We describe how to combine results from sequential Hoare logic style reasoning about the page fault handler on the low-level concurrent machine model. To the best of our knowledge this is the first example of pervasive formal verification of software communicating with devices.


Virtual Machine Hard Disk Physical Machine Physical Memory Page Fault 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Alkassar, E., Hillebrand, M., Knapp, S., Rusev, R., Tverdyshev, S.: Formal device and programming model for a serial interface. In: Proc. 4th International Verification Workshop (VERIFY). CEUR-WS Workshop Proc. (2007)Google Scholar
  2. 2.
    Bevier, W., Hunt Jr., W., Moore, J.S., Young, W.: An approach to systems verification. Journal of Automated Reasoning 5(4), 411–428 (1989)Google Scholar
  3. 3.
    Beyer, S., Jacobi, C., Kroening, D., Leinenbach, D., Paul, W.: Putting it all together: Formal verification of the VAMP. International Journal on Software Tools for Technology Transfer 8(4–5), 411–430 (2006)CrossRefGoogle Scholar
  4. 4.
    Condea, C.: Design and implementation of a page fault handler in C0. Master’s thesis, Saarland University (July 2006)Google Scholar
  5. 5.
    Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W.: On the correctness of operating system kernels. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 1–16. Springer, Heidelberg (2005)Google Scholar
  6. 6.
    Heiser, G., Elphinstone, K., Kuz, I., Klein, G., Petters, S.: Towards trustworthy computing systems: Taking microkernels to the next level. In: Operating Systems Review (July 2007)Google Scholar
  7. 7.
    Hillebrand, M.: Address Spaces and Virtual Memory: Specification, Implementation, and Correctness. PhD thesis, Saarland University, Computer Science Department (June 2005)Google Scholar
  8. 8.
    Hillebrand, M., In der Rieden, T., Paul, W.: Dealing with I/O devices in the context of pervasive system verification. In: ICCD 2005, pp. 309–316. IEEE Computer Society Press, Los Alamitos (2005)Google Scholar
  9. 9.
    Hohmuth, M., Tews, H., Stephens, S.: Applying source-code verification to a microkernel: the vfiasco project. In: Proc. 10th ACM SIGOPS, pp. 165–169. ACM Press, New York (2002)Google Scholar
  10. 10.
    Leinenbach, D., Petrova, E.: Pervasive compiler verification – from verified programs to verified systems. In: 3rd SSV 2008, Elsevier Science B. V (to appear, 2008)Google Scholar
  11. 11.
    Neumann, P., Feiertag, R.: PSOS revisited. In: Omondi, A.R., Sedukhin, S. (eds.) ACSAC 2003. LNCS, vol. 2823, Springer, Heidelberg (2003)Google Scholar
  12. 12.
    Shao, Z., Yu, D., Ni, Z.: Using xcap to certify realistic systems code: Machine context management. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 189–206. Springer, Heidelberg (2007)Google Scholar
  13. 13.
    Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technische Universität München (April 2006)Google Scholar
  14. 14.
    Tuch, H., Klein, G.: Verifying the L4 virtual memory subsystem. In: Proc. NICTA Formal Methods Workshop on Operating Systems Verification, NICTA, pp. 73–97 (2004)Google Scholar
  15. 15.
    Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Proc. 34th POPL, pp. 97–108. ACM Press, New York (2007)Google Scholar
  16. 16.
    Walker, B., Kemmerer, R., Popek, G.: Specification and verification of the UCLA Unix security kernel. Commun. ACM 23(2), 118–131 (1980)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Eyad Alkassar
    • 1
  • Norbert Schirmer
    • 1
  • Artem Starostin
    • 1
  1. 1.Computer Science DepartmentSaarland University 

Personalised recommendations