Verification of the L4 IPC implementation

doi:10.7523/j.issn.2095-6134.2011.6.012

Abstract

Abstract:

Inter-process communication (IPC) mechanism is one of the key technologies of microkernel operating system. In this paper we present a formal method to model and verify the IPC implementation. The source code of L4 IPC implementation is translated into abstract model which is described in Promela, and the abstract model can be verified with Spin directly. The experimental results show the feasibility and practicality of the method.

Key words: L4 microkernel, inter-process communication(IPC), model checking, Spin

CLC Number:

TP302

GAO Yan-Yan, LI Xi, ZHOU Xue-Hai. Verification of the L4 IPC implementation[J]. , 2011, 28(6): 786-792.

References

[1] Wing J M. A symbiotic relationship between formal methods and security //Workshops on Computer Security, Dependability, and Assurance: From Needs to Solutions. Washington, DC, USA: IEEE Computer Society, 1998.

[2] Klein G. Operating system verification—an overview
[J]. Sādhanā, 2009, 34(1): 26-69.

[3] Cock D, Klein G, Sewell T. Secure microkernels, state monads and scalable refinement //Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics. Berlin, Heidelberg: Springer-Verlag, 2008.

[4] Hillebrand M A, Paul W J. On the architecture of system verification environments //Proceedings of the 3rd International Haifa Verification Conference on Hardware and Software: Verification and Testing. Lecture Notes in Computer Science, 4899. Berlin, Germany: Springer-Verlag, 2008.

[5] Hohmuth M, Tews H, Stephens S G. Applying source-code verification to a microkernel: the VFiasco project //Proceedings of the 10th ACM SIGOPS European Workshop. New York, NY, USA: ACM, 2002.

[6] Endrawaty E. Verification of the fiasco IPC implementation . Department of Computer Science, Institute of Theoretical Computer Science. Dresden University of Technology,Germany. 2005.

[7] Clarke E, Grumberg O, Long D. Verification tools for finite-state concurrent systems //A Decade of Concurrency-Reflections and Perspectives. Lecture Notes in Computer Science, 803. London, UK: Springer-Verlag, 1994: 124-175.

[8] Cattel T. Modelization and verification of a multiprocessor realtime OS kernel //Proceedings of FORTE'94. London, UK: Chapman & Hall, Ltd, 1995:55-70.

[9] Duval G, Julliand J. Modelling and verification of the RUBIS μ-kernel with SPIN //SPIN'95. Workshop on Model Checking of Software, 1995.

[10] Tullmann P, Turner J, McCorquodale J, et al. Formal methods: a practical tool for OS implementors //HotOS-VI. Washington, DC, USA: IEEE Computer Society, 1997.

[11] 姜玉蓉. LINUX内核进程间通信的模型检测研究 . 长沙: 湖南大学, 2009.

[12] Universitt Karlsruhe. L4Ka::Pistachio microkernel. http://l4ka.org/projects/pistachio/.