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,

Research on Microkernel Integrity Semantics Model and Formal Verification

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
  • 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.
  • loading
  • 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.
  • 加载中


    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (423) PDF downloads(1052) Cited by()
    Proportional views


    DownLoad:  Full-Size Img  PowerPoint