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