| 一个C语言安全子集的可信编译器 |
| |
| 引用本文： | 王蕾,石刚,董渊,白晓颖,王生原.一个C语言安全子集的可信编译器[J].计算机科学,2013,40(9):30-34. |
| |
| 作者姓名： | 王蕾 石刚 董渊 白晓颖 王生原 |
| |
| 作者单位： | 清华大学计算机科学与技术系 北京100084 |
| |
| 基金项目： | 本文受国家自然科学基金(61170051,6,90818019),国家核高基项目(2012ZX01039-004-08-02),清华大学基础研究基金(2010Z05097),铁道部-清华大学科技研究基金(J2010Z064)资助 |
| |
| 摘 要： | 以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器.然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估.之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器.最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率.
|
| 关 键 词： | 可信计算 CompCert C安全子集 经过验证的编译器 |
| 收稿时间： | 2012/11/30 0:00:00 |
| 修稿时间： | 2013/3/11 0:00:00 |
Trusted Compiler for Safe Subset of C Language |
| |
| 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. |
| |
| Authors: | WANG Lei SHI Gang DONG Yuan BAI Xiao-ying and WANG Sheng-yuan |
| |
| Affiliation: | Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China;Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China;Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China;Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China;Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China |
| |
| Abstract: | |
| |
| Keywords: | Trustworthy computing CompCert Safe subset of C language Verified compilers |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
