2Abadi M,Budiu M, Erlingsson U,et al. Control-flowintegrity principles, implementations, and applications [J].ACM Trans on Information and System Security, 2009,13(1): 1-40.
3Chen Ping, Xiao Hai,Shen Xiaobin, et al. DROP: Detectingreturn-oriented programming malicious code [C] //Proc of the5th Int Conf on Information Systems Security (ICISS'09).Berlin: Springer, 2009 : 163-177.
4Chen Ping, Xiao Xing, Hao Han, et al. Efficient detection ofthe return-oriented programming malicious code [C] //Proc ofthe 6th Int Conf on Information Systems Security(ICISS,10).Berlin: Springer, 2010: 140-155.
5Bevier W R. A verified operating system lernel [D]. Austin:University of Texas at Austin, 1987.
6Klein G,Elphinstone K,Heiser G, et al. seL4: Formalverification of an OS kernel [C] //Proc of the 22nd ACMSymp on Operating Systems Principles ( SOSP'09 ). NewYork: ACM, 2009: 207-220.
7Gargano M, Hillebrand M, Leinenbach D, et al. On thecorrectness of operating system kernels [G] //LNCS 3603 ?Proc of the 18th Int Conf on Theorem Proving in HigherOrVler Logics(TPHOLs,05). Berlin: Springer, 2005 : 1-16.
8Stampoulis A,Shao Z. VeriML: Typed computation oflogical terms inside a language with effects [C] //Proc of the15th ACM SIGPLAN Int Conf on Functional Programming(ICFP’10). New York: ACM, 2010: 333-344.
9Shapiro J, Doerrie M S, Northup E, et al. Towards averified, general-purpose operating system kernel [C] //Procof the 1st NICTA Workshop on Operating SystemVerification. Sydney: NICTA, 2004 : 1-19.
10Shapiro J S, Smith J M, Farber D J. EROS: A fastcapability system [C] //Proc of 17th ACM Symp onOperating Systems Principles(SOSP,99). New York: ACM,1999: 170-185.
