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

摘要：

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

关键词：可信计算、CompCert、C安全子集、经过验证的编译器

所属期刊栏目：40

分类号：TP314(计算技术、计算机技术)

资助基金：国家自然科学基金61170051,61272086,90818019;国家核高基项目2012ZX01039-004-08-02;清华大学基础研究基金2010Z05097;铁道部-清华大学科技研究基金J2010Z064

在线出版日期：2013-11-11（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：30-34