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

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.

• Kei Kawamorita
• Ryouta Kasahara
• Yuuki Mochizuki
• Kenichiro Noguchi

• B method
• embedded systems
• extended state transition
• formal methods
• separation kernel
• Spin.

[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.