一个C语言安全子集的可信编译器

计算机科学 ›› 2013, Vol. 40 ›› Issue (9): 30-34.

一个C语言安全子集的可信编译器

王蕾,石刚,董渊,白晓颖,王生原

清华大学计算机科学与技术系北京100084;清华大学计算机科学与技术系北京100084;清华大学计算机科学与技术系北京100084;清华大学计算机科学与技术系北京100084;清华大学计算机科学与技术系北京100084

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受国家自然科学基金(61170051,6,90818019),国家核高基项目(2012ZX01039-004-08-02),清华大学基础研究基金(2010Z05097),铁道部-清华大学科技研究基金(J2010Z064)资助

Trusted Compiler for Safe Subset of C Language

WANG Lei,SHI Gang,DONG Yuan,BAI Xiao-ying and WANG Sheng-yuan

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估。之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器。最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率。

关键词: 可信计算,CompCert,C安全子集,经过验证的编译器中图法分类号TP314文献标识码A

Abstract: Using the safety standards of safety-critical areas as the basis,safety-related software coding and compiling requirements as the guideline,this paper introduced the following aspects of research and exploration:first analysed the formal verification technique for trusted compiler,especially emphasized the CompCert verified compiler which is widely concerned,then constructed test cases according to safe subset of C language for space armament software to test and assess the CompCert compiler with the new method．Based on the test results,the project added unsupported features of C language to CompCert and cuts off the features which do not meet the safe subset of C language requirements,built a verified compiler for the safe subset of C language at last．The experimental results show that the compiler we implemented complies with safe subset of C language,but it do not increase the execution time of C code.

Key words: Trustworthy computing,CompCert,Safe subset of C language,Verified compilers

王蕾,石刚,董渊,白晓颖,王生原. 一个C语言安全子集的可信编译器[J]. 计算机科学, 2013, 40(9): 30-34. https://doi.org/

WANG Lei,SHI Gang,DONG Yuan,BAI Xiao-ying and WANG Sheng-yuan. Trusted Compiler for Safe Subset of C Language[J]. Computer Science, 2013, 40(9): 30-34. https://doi.org/

参考文献

[1] CEI/IEC 60880:2006,Nuclear power plants．Instrumenationand control systems important to safety．Software aspects for computer-based systems performing category A functions [S]．Geneva:CEI/IEC,2006
[2] RTCA/DO-178B,Software Considerations in Air-borne Sys-tems and Equipment Certification[S]．Washington DC:RTCA,1992
[3] INRIA．CompCert development team．CompCert[EB/OL]．ht-tp://compcert．inria.fr/index.html,2012-07
[4] Klein G,Elphinstone K,Heiser G,et al．seL4:Formal verifica-tion of an OS kernel[C]∥Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles．NY,USA:ACM New York,2009:207-220
[5] Coq development team．The Coq proof assistant[EB/OL]．ht-tp://coq.inria.fr/,2012-07
[6] Nipkow T,Paulson LC,Wenzel M．Isabelle/HOL:a proof assistant for higher-order logic[M]．London:Springer-Verlag,2002
[7] Xavier L．Formal verification of a realistic compiler[J]．Commun ACM,2009,52(7):107-115
[8] Sandrine B,Xavier L．Mechanized semantics for the Clight subset of the C language[J]．Journal of Automated Reasoning,2009,43(3):263-288
[9] Xavier L．The CompCert C verified compiler Documentation and user’s manual,version 1.11[R]．Paris:INRIA Paris-Rocquencourt,2012
[10] ISO/IEC 9899-1990．Programming languages-C[S]．Geneva:ISO/IEC,1990
[11] GJB 5369-2005．航天型号软件C语言安全子集[S]．北京:国防科学技术工业委员会,2005
[12] GB/T 15272-94．程序设计语言C[S]．北京:国家质量监督检验检疫总局,1994
[13] MISRA．The MISRA C team．MISRA C[EB/OL]．http://www.misra-c.com/Activities/MISRAC/tabid/160/Default.aspx,2012-07

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed