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.
Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1071246Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1512
 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.
 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.
 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.
 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.
 Common Criteria for Information Technology Security Evaluation, Version 3.1 Revision 2, CCMB-2007-09-003. Common Criteria Project Sponsoring Organizations, 2007.
 Y. Nakamura and Y. Sameshima, "SELinux for Consumer Electronics Devices," in Proc. the Linux Symposium, vol. 2, 2008, pp. 125-134.
 I. D. Craig, Formal Design for Operating System Kernels. London: Springer-Verlag, 2006.
 I. D. Craig, Formal Refinement for Operating System Kernels. London: Springer-Verlag, 2007.
 B. Potter, J. Sinclair, and D. Till, An Introduction to Formal Specification and Z. Prentice Hall, 1991.
 J.-R. Abrial, The B-Book´╝ìAssigning programs to meanings. Cambridge University Press, 1996.
 B Language - Reference Manual. ClearSy. Available: http://www.b4free.com.
 B4free. ClearSy. Available: http://www.b4free.com.
 K. Noguchi, Logical Method for Software Design. Kyoritsu Publishing, Japan, 1990. (in Japanese)
 G. J. Holzmann, The Spin Model Checker: Primer and Reference Manual. Addison Wesley, 2004.
 G. J. Holzmann, "The Model Checker Spin," in IEEE Trans. on Software Engineering, vol. 23, no. 5, 1997, pp. 1-17.
 IA-32 Intel Architecture Software Developer-s Manuals. Intel Corporation.
 D. Bell and L. LaPadula, Secure Computer System: Mathematical Foundations and Model. MITRE Rep. MTR 2547, 1973.