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

• 作者: 王生原 王蕾 白晓颖 石刚 董渊
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 可信计算 CompCert C安全子集 经过验证的编译器
• 年，卷（期）: 2013,（9）
• 页码范围: 30-34
• 页数: 5页
• 分类号: TP314
• 字数: 5203字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	白晓颖	清华大学计算机科学与技术系	46	752	14.0	26.0
2	董渊	清华大学计算机科学与技术系	33	386	10.0	18.0
3	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
4	王蕾	清华大学计算机科学与技术系	23	85	5.0	8.0
5	石刚	清华大学计算机科学与技术系	11	38	4.0	5.0