计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2013年
9期
30-34
,共5页
王蕾%石刚%董渊%白晓颖%王生原
王蕾%石剛%董淵%白曉穎%王生原
왕뢰%석강%동연%백효영%왕생원
可信计算%CompCert%C安全子集%经过验证的编译器
可信計算%CompCert%C安全子集%經過驗證的編譯器
가신계산%CompCert%C안전자집%경과험증적편역기
Trustworthy computing%CompCert%Safe subset of C language%Verified compilers
以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器.然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估.之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器.最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率.
以安全關鍵領域的安全標準為依託、安全相關軟件的語言編碼和編譯要求為指導,進行瞭以下幾方麵的研究和探索:首先對形式化驗證可信編譯技術進行分析研究,特彆著重噹前廣受關註的經過驗證的CompCert編譯器.然後以我國安全領域C語言安全子集標準《航天型號軟件C語言安全子集》為依據構造測試用例、創新測試方法,併以此對CompCert編譯器進行測試評估.之後依據測試結果,為CompCert編譯器增加未支持的C語言標準特性,裁剪不符閤C語言安全子集要求的特性,構建符閤C語言安全子集標準的可信編譯器.最後的實測結果錶明,所實現的編譯器符閤C語言安全子集標準的要求,且沒有降低C代碼的執行效率.
이안전관건영역적안전표준위의탁、안전상관연건적어언편마화편역요구위지도,진행료이하궤방면적연구화탐색:수선대형식화험증가신편역기술진행분석연구,특별착중당전엄수관주적경과험증적CompCert편역기.연후이아국안전영역C어언안전자집표준《항천형호연건C어언안전자집》위의거구조측시용례、창신측시방법,병이차대CompCert편역기진행측시평고.지후의거측시결과,위CompCert편역기증가미지지적C어언표준특성,재전불부합C어언안전자집요구적특성,구건부합C어언안전자집표준적가신편역기.최후적실측결과표명,소실현적편역기부합C어언안전자집표준적요구,차몰유강저C대마적집행효솔.
