Advertisement

Formal Verification of a Microkernel Used in Dependable Software Systems

  • Christoph Baumann
  • Bernhard Beckert
  • Holger Blasum
  • Thorsten Bormer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5775)

Abstract

In recent years, deductive program verification has improved to a degree that makes it feasible for real-world programs. Following this observation, the main goal of the BMBF-supported Verisoft XT project is (a) the creation of methods and tools which allow the pervasive formal verification of integrated computer systems, and (b) the prototypical realization of four concrete, industrial application tasks.

In this paper, we report on the Verisoft XT subproject Avionics, where formal verification is being applied to a commercial embedded operating system. The goal is to use deductive techniques to verify functional correctness of the PikeOS system, which is a microkernel-based partitioning hypervisor.

We present our approach to verifying the microkernel’s system calls, using a system call for changing the priority of threads as an example. In particular, (a) we give an overview of the tool chain and the verification methodology, (b) we explain the hardware model and how assembly semantics is specified so that functions whose implementation contain assembly can be verified, and (c) we describe the verification of the system call itself.

Keywords

System Call Assembly Code Branch Instruction Hardware Model Assembly Instruction 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Airlines Electronic Engineering Committee. Avionics Application Software Standard Interface. Aeronautical Radio, Inc., 2551 Riva Road, Annapolis, MD 21401, ARINC specification 653 (1997)Google Scholar
  2. 2.
    Alglave, J., et al.: The semantics of Power and ARM multiprocessor machine code. In: DAMP 2009: Proceedings of the 4th Workshop on Declarative Aspects of Multicore Programming, Savannah, GA, USA, pp. 13–24. ACM, New York (2009)Google Scholar
  3. 3.
    Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Better avionics software reliability by code verification. In: Proceedings, embedded world Conference, Nuremberg, Germany (2009)Google Scholar
  4. 4.
    Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 460–475. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: TPHOLs 2009. LNCS, vol. 5674, Springer, Heidelberg (2009)Google Scholar
  6. 6.
    Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A practical verification methodology for concurrent programs. Technical Report MSR-TR-2009-15, Microsoft Research (2009), http://research.microsoft.com/vcc
  7. 7.
    Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contract-based modular verification of concurrent C, http://research.microsoft.com/vcc
  8. 8.
    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)Google Scholar
  10. 10.
    Freescale Semiconductor. MPC5200B User’s Manual, Rev. 1.3 (September 2006), http://www.freescale.com/files/32bit/doc/ref_manual/MPC5200BUM.pdf
  11. 11.
    In der Rieden, T., Tsyban, A.: CVM: A verified framework for microkernel programmers. In: Huuck, R., Klein, G., Schlich, B. (eds.) 3rd International Workshop on Systems Software Verification (SSV 2008). ENTCS, vol. 217, pp. 151–168. Elsevier Science B.V, Amsterdam (2008)Google Scholar
  12. 12.
    Kaiser, R., Wagner, S.: Evolution of the PikeOS microkernel. In: Kuz, I., Petters, S.M. (eds.) MIKES: 1st International Workshop on Microkernels for Embedded Systems (2007), http://ertos.nicta.com.au/publications/papers/Kuz_Petters_07.pdf
  13. 13.
    Klein, G.: Operating system verification: An overview. Technical Report NRL-955, NICTA, Sydney, Australia (June 2008), http://wwwbroy.informatik.tu-muenchen.de/~kleing/papers/os-overview.pdf
  14. 14.
    Klein, G., Norrish, M., Elphinstone, K., Heiser, G.: Verifying a high-performance micro-kernel. In: Proceedings, 7th Annual High-Confidence Software and Systems Conf., Baltimore, USA (2007)Google Scholar
  15. 15.
    Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–515. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. 16.
    Maus, S., Moskal, M., Schulte, W.: Vx86: x86 assembler simulated in C powered by automated theorem proving. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 284–298. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Pelzl, J., Wolf, M., Wollinger, T.: Virtualization technologies for cars: Solutions to increase safety and security of vehicular ECUs. In: Proceedings, embedded world Conference, Nuremberg, Germany (2009)Google Scholar
  18. 18.
    Radio Technical Commission for Aeronautics. Integrated Modular Avionics (IMA) Development Guidance and Certification Considerations. DO-297. Radio Technical Commission for Aeronautics (RTCA), Inc., 1828 L Street NW, Suite 805, Washington, D.C. 20036 (November 2005)Google Scholar
  19. 19.
    Starostin, A., Tsyban, A.: Correct microkernel primitives. In: Huuck, R., Klein, G., Schlich, B. (eds.) 3rd International Workshop on Systems Software Verification (SSV 2008). ENTCS, vol. 217, pp. 169–185. Elsevier Science B. V, Amsterdam (2008)Google Scholar
  20. 20.
    SYSGO AG press releases. PikeOS selected for traffic control system (August 07, 2007), Flight management system will run on SYSGO’s PikeOS in the DIANA project (July 17, 2008), AIRBUS selects SYSGO’s PikeOS as DO-178B reference platform for the A350 XWB (November 18, 2008), Rheinmetall selects DO178B certifiable PikeOS from SYSGO for A400M project (December 10, 2008), http://www.sysgo.com
  21. 21.
    Zucker, S., Karhi, K.: System V Application Binary Interface: PowerPC Processor Supplement. SunSoft, Mountain View, CA, USA, 802-3334-10 edn. (September 1995), http://refspecs.freestandards.org/elf/elfspec_ppc.pdf

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Christoph Baumann
    • 1
  • Bernhard Beckert
    • 2
  • Holger Blasum
    • 3
  • Thorsten Bormer
    • 2
  1. 1.Dept. of Computer ScienceSaarland UniversitySaarbrückenGermany
  2. 2.Dept. of Computer ScienceUniversity of KoblenzGermany
  3. 3.SYSGO AG, Klein-WinternheimGermany

Personalised recommendations