%0 Journal Article
%T 一个c语言安全子集的可信编译器
%A 王蕾？
%A 石刚？
%A 董渊？
%A 白晓颖？
%A 王生原？
%J 计算机科学
%D 2013
%X 以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的compcert编译器。然后以我国安全领域c语言安全子集标准《航天型号软件c语言安全子集》为依据构造测试用例、创新测试方法,并以此对compcert编译器进行测试评估。之后依据测试结果,为compcert编译器增加未支持的c语言标准特性,裁剪不符合c语言安全子集要求的特性,构建符合c语言安全子集标准的可信编译器。最后的实测结果表明,所实现的编译器符合c语言安全子集标准的要求,且没有降低c代码的执行效率。
%K 可信计算
%K compcert
%K c安全子集
%K 经过验证的编译器中图法分类号tp314文献标识码a
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=20130906&flag=1