Open Science Research Excellence

Open Science Index

Commenced in January 2007 Frequency: Monthly Edition: International Publications Count: 30677


Select areas to restrict search in scientific publication database:
8630
Application of Formal Methods for Designing a Separation Kernel for Embedded Systems
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.
Digital Object Identifier (DOI):

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.
Vol:14 No:09 2020Vol:14 No:08 2020Vol:14 No:07 2020Vol:14 No:06 2020Vol:14 No:05 2020Vol:14 No:04 2020Vol:14 No:03 2020Vol:14 No:02 2020Vol:14 No:01 2020
Vol:13 No:12 2019Vol:13 No:11 2019Vol:13 No:10 2019Vol:13 No:09 2019Vol:13 No:08 2019Vol:13 No:07 2019Vol:13 No:06 2019Vol:13 No:05 2019Vol:13 No:04 2019Vol:13 No:03 2019Vol:13 No:02 2019Vol:13 No:01 2019
Vol:12 No:12 2018Vol:12 No:11 2018Vol:12 No:10 2018Vol:12 No:09 2018Vol:12 No:08 2018Vol:12 No:07 2018Vol:12 No:06 2018Vol:12 No:05 2018Vol:12 No:04 2018Vol:12 No:03 2018Vol:12 No:02 2018Vol:12 No:01 2018
Vol:11 No:12 2017Vol:11 No:11 2017Vol:11 No:10 2017Vol:11 No:09 2017Vol:11 No:08 2017Vol:11 No:07 2017Vol:11 No:06 2017Vol:11 No:05 2017Vol:11 No:04 2017Vol:11 No:03 2017Vol:11 No:02 2017Vol:11 No:01 2017
Vol:10 No:12 2016Vol:10 No:11 2016Vol:10 No:10 2016Vol:10 No:09 2016Vol:10 No:08 2016Vol:10 No:07 2016Vol:10 No:06 2016Vol:10 No:05 2016Vol:10 No:04 2016Vol:10 No:03 2016Vol:10 No:02 2016Vol:10 No:01 2016
Vol:9 No:12 2015Vol:9 No:11 2015Vol:9 No:10 2015Vol:9 No:09 2015Vol:9 No:08 2015Vol:9 No:07 2015Vol:9 No:06 2015Vol:9 No:05 2015Vol:9 No:04 2015Vol:9 No:03 2015Vol:9 No:02 2015Vol:9 No:01 2015
Vol:8 No:12 2014Vol:8 No:11 2014Vol:8 No:10 2014Vol:8 No:09 2014Vol:8 No:08 2014Vol:8 No:07 2014Vol:8 No:06 2014Vol:8 No:05 2014Vol:8 No:04 2014Vol:8 No:03 2014Vol:8 No:02 2014Vol:8 No:01 2014
Vol:7 No:12 2013Vol:7 No:11 2013Vol:7 No:10 2013Vol:7 No:09 2013Vol:7 No:08 2013Vol:7 No:07 2013Vol:7 No:06 2013Vol:7 No:05 2013Vol:7 No:04 2013Vol:7 No:03 2013Vol:7 No:02 2013Vol:7 No:01 2013
Vol:6 No:12 2012Vol:6 No:11 2012Vol:6 No:10 2012Vol:6 No:09 2012Vol:6 No:08 2012Vol:6 No:07 2012Vol:6 No:06 2012Vol:6 No:05 2012Vol:6 No:04 2012Vol:6 No:03 2012Vol:6 No:02 2012Vol:6 No:01 2012
Vol:5 No:12 2011Vol:5 No:11 2011Vol:5 No:10 2011Vol:5 No:09 2011Vol:5 No:08 2011Vol:5 No:07 2011Vol:5 No:06 2011Vol:5 No:05 2011Vol:5 No:04 2011Vol:5 No:03 2011Vol:5 No:02 2011Vol:5 No:01 2011
Vol:4 No:12 2010Vol:4 No:11 2010Vol:4 No:10 2010Vol:4 No:09 2010Vol:4 No:08 2010Vol:4 No:07 2010Vol:4 No:06 2010Vol:4 No:05 2010Vol:4 No:04 2010Vol:4 No:03 2010Vol:4 No:02 2010Vol:4 No:01 2010
Vol:3 No:12 2009Vol:3 No:11 2009Vol:3 No:10 2009Vol:3 No:09 2009Vol:3 No:08 2009Vol:3 No:07 2009Vol:3 No:06 2009Vol:3 No:05 2009Vol:3 No:04 2009Vol:3 No:03 2009Vol:3 No:02 2009Vol:3 No:01 2009
Vol:2 No:12 2008Vol:2 No:11 2008Vol:2 No:10 2008Vol:2 No:09 2008Vol:2 No:08 2008Vol:2 No:07 2008Vol:2 No:06 2008Vol:2 No:05 2008Vol:2 No:04 2008Vol:2 No:03 2008Vol:2 No:02 2008Vol:2 No:01 2008
Vol:1 No:12 2007Vol:1 No:11 2007Vol:1 No:10 2007Vol:1 No:09 2007Vol:1 No:08 2007Vol:1 No:07 2007Vol:1 No:06 2007Vol:1 No:05 2007Vol:1 No:04 2007Vol:1 No:03 2007Vol:1 No:02 2007Vol:1 No:01 2007