Application of Formal Methods for Designing a Separation Kernel for Embedded Systems

Authors: Kei Kawamorita, Ryouta Kasahara, Yuuki Mochizuki, Kenichiro Noguchi

Abstract:

A separation-kernel-based operating system (OS) has been designed for use in secure embedded systems by applying formal methods to the design of the separation-kernel part. The separation kernel is a small OS kernel that provides an abstract distributed environment on a single CPU. The design of the separation kernel was verified using two formal methods, the B method and the Spin model checker. A newly designed semi-formal method, the extended state transition method, was also applied. An OS comprising the separation-kernel part and additional OS services on top of the separation kernel was prototyped on the Intel IA-32 architecture. Developing and testing of a prototype embedded application, a point-of-sale application, on the prototype OS demonstrated that the proposed architecture and the use of formal methods to design its kernel part are effective for achieving a secure embedded system having a high-assurance separation kernel.

Keywords: B method, embedded systems, extended state transition, formal methods, separation kernel, Spin.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1071246

References:

[1] J. Rushby, "The design and verification of secure systems," in ACM Operating Systems Review, vol. 15, no. 5, Eighth ACM Symposium on Operating System Principles (SOSP), 1981, pp. 12-21.
[2] J. Rushby, "Proof of SeparabilityÔÇòA verification technique for a class of security kernels," in Proc. 5th International Symposium on Programming, vol. 137 of Lecture Notes in Computer Science, 1982, pp. 352-367.
[3] T. E. Levin, C. E. Irvine, and T. D. Nguyen, "Least privilege in separation kernels," in Proc. International Conf. on Security and Cryptography SECRYPT 2006, 2006, pp 355-362.
[4] C. L. Heitmeyer, M. Archer, E. I. Leonard, and J. D. McLean, "Formal specification and verification of data separation in a separation kernel for an embedded system," in ACM Conf. on Computer and Communications Security, 2006, pp. 346-355.
[5] Common Criteria for Information Technology Security Evaluation, Version 3.1 Revision 2, CCMB-2007-09-003. Common Criteria Project Sponsoring Organizations, 2007.
[6] Y. Nakamura and Y. Sameshima, "SELinux for Consumer Electronics Devices," in Proc. the Linux Symposium, vol. 2, 2008, pp. 125-134.
[7] I. D. Craig, Formal Design for Operating System Kernels. London: Springer-Verlag, 2006.
[8] I. D. Craig, Formal Refinement for Operating System Kernels. London: Springer-Verlag, 2007.
[9] B. Potter, J. Sinclair, and D. Till, An Introduction to Formal Specification and Z. Prentice Hall, 1991.
[10] J.-R. Abrial, The B-Book´╝ìAssigning programs to meanings. Cambridge University Press, 1996.
[11] B Language - Reference Manual. ClearSy. Available: http://www.b4free.com.
[12] B4free. ClearSy. Available: http://www.b4free.com.
[13] K. Noguchi, Logical Method for Software Design. Kyoritsu Publishing, Japan, 1990. (in Japanese)
[14] G. J. Holzmann, The Spin Model Checker: Primer and Reference Manual. Addison Wesley, 2004.
[15] G. J. Holzmann, "The Model Checker Spin," in IEEE Trans. on Software Engineering, vol. 23, no. 5, 1997, pp. 1-17.
[16] IA-32 Intel Architecture Software Developer-s Manuals. Intel Corporation.
[17] D. Bell and L. LaPadula, Secure Computer System: Mathematical Foundations and Model. MITRE Rep. MTR 2547, 1973.