摘要
编译器的安全可信问题日益引起重视,特别是在安全关键系统中,编译器的误编译将会造成重大的损失。消除误编译的传统方法是大量的测试,但是测试难以达到完全覆盖,并不能充分地保证编译器的安全可信。近年来,形式化验证方法被成功用于可信编译器的构造中。一种方法是对编译器本身进行形式化验证,经过严密的证明,可杜绝误编译的发生。然而,这种方法可能"冻结"编译器的设计,阻碍编译器未来可能的优化和完善。翻译确认是另外一种用于可信编译器构造的形式化方法,它避免了对编译器自身的验证,有很好的可重用性,近年来在编译器验证领域得到了广泛研究,已取得令人瞩目的成果。介绍了翻译确认方法的概念及研究进展。
There is a growing awareness of the security and reliability of compilers in recent years.Especially in the safety-critical systems,the miscompilation can make a huge damage.The conventional approach to weeding out miscompilation is heavy test,but test is impossible to achieve full cover and can not guarantee that compiler is safe and trustworthy.In recent years,formal verification method has been successfully used to construct the trusted compiler.One approach is to perform formal verification for compiler itself.It can put an end to miscompilation by strict proof.However,this approach tends to'freeze'the compiler design,and discourages any future improvements and revisions.Translation validation is another formal method that can be used to construct trusted compiler,which avoids the verification for the compiler itself,and has good reusability.It has been widely researched in the compiler verification field,and has already obtained remarkable achievements.The concept and research progress of translation validation are discussed in this paper.
出处
《计算机科学》
CSCD
北大核心
2014年第S1期334-338,共5页
Computer Science
基金
国家自然基金项目(61170051
612702086
90818019)资助
关键词
可信编译器
形式化验证方法
翻译确认
确认器
Trusted compiler,Formal verification method,Translation validation,Validator
