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

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