计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2014年
z1期
334-338
,共5页
刘洋%杨斐%石刚%闫鑫%王生原%董渊
劉洋%楊斐%石剛%閆鑫%王生原%董淵
류양%양비%석강%염흠%왕생원%동연
可信编译器%形式化验证方法%翻译确认%确认器
可信編譯器%形式化驗證方法%翻譯確認%確認器
가신편역기%형식화험증방법%번역학인%학인기
Trusted compiler%Formal verification method%Translation validation%Validator
编译器的安全可信问题日益引起重视,特别是在安全关键系统中,编译器的误编译将会造成重大的损失.消除误编译的传统方法是大量的测试,但是测试难以达到完全覆盖,并不能充分地保证编译器的安全可信.近年来,形式化验证方法被成功用于可信编译器的构造中.一种方法是对编译器本身进行形式化验证,经过严密的证明,可杜绝误编译的发生.然而,这种方法可能“冻结”编译器的设计,阻碍编译器未来可能的优化和完善.翻译确认是另外一种用于可信编译器构造的形式化方法,它避免了对编译器自身的验证,有很好的可重用性,近年来在编译器验证领域得到了广泛研究,已取得令人瞩目的成果.介绍了翻译确认方法的概念及研究进展.
編譯器的安全可信問題日益引起重視,特彆是在安全關鍵繫統中,編譯器的誤編譯將會造成重大的損失.消除誤編譯的傳統方法是大量的測試,但是測試難以達到完全覆蓋,併不能充分地保證編譯器的安全可信.近年來,形式化驗證方法被成功用于可信編譯器的構造中.一種方法是對編譯器本身進行形式化驗證,經過嚴密的證明,可杜絕誤編譯的髮生.然而,這種方法可能“凍結”編譯器的設計,阻礙編譯器未來可能的優化和完善.翻譯確認是另外一種用于可信編譯器構造的形式化方法,它避免瞭對編譯器自身的驗證,有很好的可重用性,近年來在編譯器驗證領域得到瞭廣汎研究,已取得令人矚目的成果.介紹瞭翻譯確認方法的概唸及研究進展.
편역기적안전가신문제일익인기중시,특별시재안전관건계통중,편역기적오편역장회조성중대적손실.소제오편역적전통방법시대량적측시,단시측시난이체도완전복개,병불능충분지보증편역기적안전가신.근년래,형식화험증방법피성공용우가신편역기적구조중.일충방법시대편역기본신진행형식화험증,경과엄밀적증명,가두절오편역적발생.연이,저충방법가능“동결”편역기적설계,조애편역기미래가능적우화화완선.번역학인시령외일충용우가신편역기구조적형식화방법,타피면료대편역기자신적험증,유흔호적가중용성,근년래재편역기험증영역득도료엄범연구,이취득령인촉목적성과.개소료번역학인방법적개념급연구진전.
