可信编译器构造的翻译确认方法简述

摘要/Abstract

摘要： 编译器的安全可信问题日益引起重视,特别是在安全关键系统中,编译器的误编译将会造成重大的损失。消除误编译的传统方法是大量的测试,但是测试难以达到完全覆盖,并不能充分地保证编译器的安全可信。近年来,形式化验证方法被成功用于可信编译器的构造中。一种方法是对编译器本身进行形式化验证,经过严密的证明,可杜绝误编译的发生。然而,这种方法可能“冻结”编译器的设计,阻碍编译器未来可能的优化和完善。翻译确认是另外一种用于可信编译器构造的形式化方法,它避免了对编译器自身的验证,有很好的可重用性,近年来在编译器验证领域得到了广泛研究,已取得令人瞩目的成果。介绍了翻译确认方法的概念及研究进展。

关键词: 可信编译器,形式化验证方法,翻译确认,确认器中图法分类号TP314文献标识码A

Abstract: 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.

Key words: Trusted compiler,Formal verification method,Translation validation,Validator

刘洋,杨斐,石刚,闫鑫,王生原,董渊. 可信编译器构造的翻译确认方法简述[J]. 计算机科学, 2014, 41(Z6): 334-338. https://doi.org/

LIU Yang,YANG Fei,SHI Gang,YAN Xin,WANG Sheng-yuan and DONG Yuan. Brief Overview of Translation Validation Method in Trusted Compiler Construction[J]. Computer Science, 2014, 41(Z6): 334-338. https://doi.org/

参考文献

[1] Necula G C．Proof-Carrying Code[C]∥POPL’97．ACM press,1997:106-119
[2] Cimatti A,Giunchiglia F,Pecchiari P,et al.A Provably Correct Embedded Verifier for the Certification of Safety Critical Software[C]∥Grumberg O,ed．Proc．9th Intl．Conference on Computer Aided Verification (CA V’97)．Lect．Notes in Comp．Sci.,Springer-Verlag,1997,1254:202-213
[3] Pnueli A,Siegel M,Singerman E．Translation Validation[C]∥Proc．4th Intl．Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98)．1998:151-166
[4] Pnueli A,Shtrichman O,Siegel M．Translation Validation forSynchronous Languages[C]∥Larsen K G,Skyum S,Winskel G,eds.ICALP 1998．LNCS． Heidelberg:Springer,1998:1443:235-246
[5] Pnueli A,Singerman E,Siegel M．Translation Validation:from SIGNAL to C[C]∥Volume 1710of LNCS State-of-the-Art Survey．Springer-Verlag,1999:231-255
[6] Pnueli A,Shtrichman O,Siegel M．Translation validation:FromDC+ to C[C]∥Proceedings of the International Workshop on Current Trends in Applied Formal Method:Applied Formal Methods．Volume 1641of Lect．Notes in Comp.Sci.,1998:137-150
[7] Pnueli A,Siegel M,Shtrichman O．The code validation tool(CVT)-automatic verification of a compilation process[J]．Int．Journal of Software Tools for Technology Transfer (STTT),1999,2(2):192-201
[8] Necula G C．Translation validation for an optimizing compiler[C]∥Programming Language Design and Implementation 2000．ACM Press,2000:83-95
[9] Zuck L,Pnueli A,Leviathan R．Validations of optimizing compliers[R]．Weizmann Institute of Science,2000
[10] Zuck L,Pnueli A,Fang Y,et al．Voc:A methodology for thetranslation validation of optimizing compilers[J]．Jounal of Universal Computer Science,2003,9(3):223-247
[11] Zuck L,Pnueli A,Fang Y,et al．Translation and Run-Time Validation of Optimized Code[C]∥Electronic Notes in Theoretical Computer Science．2002
[12] Zuck L,Pnueli A,Goldberg B,et al．Translation and run-time validation of loop transformations[C]∥Proceedings of the Run-Time Result Verification Workshop,Electronic Notes in Theoretical Computer Science (ENTCS)．volume 70,2002
[13] Ryabtsev M,Strichman O．Translation validation:From Simulink to C[M]∥Computer Aided Verification．Springer,2009
[14] Rival X．Symbolic transfer function-based approaches to certified compilation[C]∥31st symposium Principles of Programming Languages．ACM Press,2004:1-13
[15] Tristan J-B,Leroy X．Formal verification of translation validators:A case study on instruction scheduling optimizations[C]∥35th symposium Principles of Programming Languages．ACM Press,2008:17-27
[16] Tristan J-B,Leroy X．Verified Validation of Lazy Code Motion[C]∥Programming Language Design and Implementation 2009．ACM Press,2009:316-326
[17] Tate R,Stepp M,Tatlock Z,et al.Equality saturation:A new approach to optimization[C]∥36th Principles of Programming Languages．ACM,2009:264-276
[18] Tristan J-B,Leroy X．Evaluating Value-Graph Translation Validation for LLVM[C]∥32nd ACM SIGPLAN conference on Programming language design and implementation．ACM Press,2011:295-305
[19] Tristan J-B,Leroy X．A Simple,Verified Validator for Software Pipelining[C]∥37th symposium Principles of Programming Languages．ACM Press,2010:83-92
[20] Tristan J-B．Formal verification of translation validators[D]．Universite Paris-Diderot-Paris VII,2009
[21] Huang Yu-qiang,Childers B R, Soffa M L．Catching and identifying bugs in register allocation[C]∥Static Analysis,13th Int．Symp.,SAS 2006．volume 4134of Lecture Notes in Computer Science．Springer,2006:281-300
[22] Kanade A,Sanyal A,Khedker U．A PVS based framework for validating compiler optimizations[C]∥SEFM’06:Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods．IEEE Computer Society,2006:108-117
[23] Colby C,Lee P,Necula G C,et al.A certifying compiler for Java[J]．ACM SIGPLAN Notices,2000,35(5):95-107
[24] Chirica L M,Martin D F．An approach to compiler correctness[J]．ACM SIGPLAN Notices,1975,10(6):96-103
[25] Ngo V C,Talpin J-P,Gautier T,et al．Formal Verification ofSynchronous Data-flow Compilers[R]．Project-Team ESPRESSO Research Report,March 2012:7921
[26] Rinard M,Marinov D．Credible compilation with pointers[C]∥Workshop on Run-Time Result Verification．1999
[27] Barret C W,Fang Yi,Goldberg B,et al．TVOC:A translationvalidator for optimizing compilers[C]∥Computer Aided Verification,17th Int．Conf.,CAV 2005．volume 3576of Lecture Notes in Computer Science．Springer,2005:291-295
[28] Zaks A,Pnueli A．Covac:Compiler validation by program analysis of the cross-product[C]∥FM 2008:Formal Methods,15th International Symposium on Formal Methods．volume 5014of Lecture Notes in Computer Science．Springer,2008: 35-51
[29] Leroy X．Formal verification of a realistic compiler[M]∥Communications of the ACM,2009
[30] Leroy X．The Compcert verified compiler,software and commented proof．http://compcert.inria.fr/,Jan．2010
[31] Fang Yi．Translation Validation of Optimizing Compilers[D]．New York University,2005
[32] Goldberg B,Zuck L,Barret C．Into the loops:Practical issues in translation validation for optimizing compilers[C]∥Proc.Workshop Compiler Optimization Meets Compiler Verification (COCV 2004)．volume 132of Electronic Notes in Theoretical Computer Science．Elsevier,2005:53-71
[33] Pnueli A,Zaks A．Translation validation of interprocedural optimizations[C]∥Proceedings of the 4th International Workshop on Software Verification and Validation(SVV)．2006
[34] Stepp M,Tate R,Lerner S．Equality-Based translation validator for LLVM[C]∥CAV’11:Proceedings of the 23rd International Conference on Computer Aided Verification．2011
[35] Barthe G,Demange D,Pichardie D．A formally verified SSA-based middle-end-Static Single Assignment meets CompCert[C]∥ESOP’12．2012
[36] 何炎祥,刘陶,吴伟．可信编译器关键技术研究[J]．计算机工程与科学,2010,32(8):1-6

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed