Research on Microkernel Integrity Semantics Model and Formal Verification

QIAN Zhenjiang; LIU Wei; HUANG Hao

Article Contents

Article Navigation > Chinese Journal of Electronics > 2014 > 23(1): 43-48

QIAN Zhenjiang, LIU Wei, HUANG Hao, “Research on Microkernel Integrity Semantics Model and Formal Verification,” Chinese Journal of Electronics, vol. 23, no. 1, pp. 43-48, 2014,

Citation:

QIAN Zhenjiang, LIU Wei, HUANG Hao, “Research on Microkernel Integrity Semantics Model and Formal Verification,” Chinese Journal of Electronics, vol. 23, no. 1, pp. 43-48, 2014,

QIAN Zhenjiang, LIU Wei, HUANG Hao, “Research on Microkernel Integrity Semantics Model and Formal Verification,” Chinese Journal of Electronics, vol. 23, no. 1, pp. 43-48, 2014,

Citation:

QIAN Zhenjiang, LIU Wei, HUANG Hao, “Research on Microkernel Integrity Semantics Model and Formal Verification,” Chinese Journal of Electronics, vol. 23, no. 1, pp. 43-48, 2014,

PDF( 189 KB)

Research on Microkernel Integrity Semantics Model and Formal Verification

1.
State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210046, China;
2.
Department of Computer Science and Technology, Nanjing University, Nanjing 210046, China

Funds: This work is supported by the National High Technology Research and Development Program of China (863 Program) (No.2011AA01A202); the National Natural Science Foundation of China (No.61021062); the "Six Talents Peak" High-Level Personnel Project of Jiangsu Province (No.2011-DZXX-035); University Natural Science Research Program of Jiangsu Province (No.12KJB520001).

Received Date: 2011-04-01
Rev Recd Date: 2012-04-01
Publish Date: 2014-01-05

Abstract

Abstract

Microkernel integrity is an important aspect of security for the whole microkernel system. Many of the research works on microkernel integrity focus on analysis and safeguards against the existing kernel attacks, and security enhancements for the vulnerabilities of system design and implementation aspects. The formal methods for operating system design and verification ensure the system's high level of security. The existing formalization work and research for operating system mainly focus on the code-level verification of program correctness. In this paper, we propose a formal abstraction model of microkernel in order to accurately describe the semantics of every kernel behavior, and achieve the description of the whole kernel. Based on the model we illustrate the microkernel integrity criterions and elaborate on the integrity mechanism. Meanwhile, we formally verify the completeness and consistency between the mechanism and the definition of the microkernel integrity. We use the self-implemented operating system VTOS (Verified trusted operating system) as an example to illustrate the design method for the microkernel integrity.
- Microkernel integrity,
- Integrity mechanism,
- Integrity semantics model,
- Formal verification

FullText(HTML)

References(18)

References

M. Abadi, M. Budiu, U. Erlingsson, J. Ligatti,"Control flow integrity: principles, implementations, and applications", ACM Transactions on Information and System Security, Vol.13, No.1, pp.1-41, 2009.

N.L. Petroni, M. Hicks,"Automated detection of persistent kernel control-flow attacks", Proc. of 14th ACM Conference on Computer and Communications Security (CCS'07), New York: ACM, pp.103-115, 2007.

M. Castro, M. Costa, T. Harris,"Securing software by enforcing data-flow integrity", Proc. of 7th Symposium on Operating Systems Design and Implementation (OSDI'06), CA: USENIX Association Berkeley, pp.147-160, 2006.

B.J. Walker, R.A. Kemmerer, G.J. Popek,"Specification and verification of the UCLA unix security kernel", Communications of the ACM, Vol.23, No.2, pp.118-131, 1980.

R.J. Feiertag, P.G. Neumann,"The foundations of a Provably secure operating system (PSOS)", Proc. of National Computer Conference (1979), AFIPS Press, pp.329-334, 1979.

SRI Website. SRI International [OL]. http://www.sri.com, 2011.

G. Klein, J. Andronick, K. Elphinstone, et al.,"seL4: Formal verification of an operating-system kernel", Communications of the ACM, Vol.53, No.6, pp.107-115, 2010.

NICTAWebsite, NICTA Research Centre, http://www.nicta.com. au/, 2011.

B. O'Sullivan, D. Stewart, J. Goerzen, Real World Haskell, California: O'Reilly, 2008.

University of Cambridge, Isabelle/HOL, http://www.cl.cam.ac. uk/research/hvg/Isabelle/index.html, 2011.

D. Elkaduwe, G. Klein, K. Elphinstone,"Verified protection model of the seL4 microkernel", Proc. of VSTTE'08, LNCS 5295, Berlin: Springer-Verlag, pp.99-114, 2008.

Verisoft Consortium, The Verisoft Project, http://www.verisoft. de/, 2011. a) M. Daum, J. Dörrenbächer, S. Bogan,"Model Stack for the Pervasive Verification of a Microkernel-Based Operating System", Proc. of the 5th International Verification Workshop in Connection with IJCAR 2008, Sydney: CEURWS. org, pp.56-70, 2008.

Yale University, Yale Flint Project, http://flint.cs.yale.edu/, 2011.

A. Stampoulis, Z. Shao,"VeriML: Typed computation of logical terms inside a language with effects", Proc. of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP'10), New York: ACM, pp.333-344, 2010.

X.Y. Feng, An Open Framework for Certified System Software, New Haven: Yale University, 2007.

Z. Shao, B. Ford,"Advanced development of certified OS kernels", Technical Report, New Haven: Yale University, 2010. http://www.cs.yale.edu/publications/techreports/tr1436.pdf.

J.V. Benthem, K. Doets, Higher Order Logic, F. Guenthner, ed. Handbook of Philosophical Logic. Berlin: Springer, 275329, 2007.

B. Nordström, K. Petersson, J.M. Smith, Programming in Martin-Löf's Type Theory: An Introduction, Oxford: Oxford University Press, 1990.

Relative Articles

Supplements(0)

Cited By

Proportional views