期刊文献+

可信编译器关键技术研究 被引量:7

Research on the Key Technology of Trusted Compiler
在线阅读 下载PDF
导出
摘要 软件的可信性很大程度上依赖于程序代码的可信性。影响软件可信性的主要因素包括来自软件内部的代码缺陷、代码错误、程序故障以及来自软件外部的病毒、恶意代码等,因此从代码角度来保证软件的可信性是实现可信软件的重要途径之一。编译器作为重要的系统软件之一,其可信性对整个计算机系统而言具有非常重要的意义。软件程序一般都需要经过编译器编译后方能执行,如果编译器不可信,则无法保证其所生成代码的可信性。本文主要讨论设计和实现可信编译器的主要思路和关键技术。 The trustworthy of software mainly depends on the trustworthy of source codes. Some factors including de- fects,errors and program faults in the source codes, virus from outside and malicious codes etc decide the trustworthy of software, so guaranteeing the trustworthy of software from aspect of source code is one of the most important methods for ensuring the trustworthy of software. As a kind of the most important system software, the trustworthy of compiler plays a critical role in the whole computer system. The software program can only be executed after compiled by compiler, so if the compiler can not be trusted, the trustworthy of executable code outputted can not be guaranteed. The key technologies and thoughts for developing trusted compiler are discussed in this paper.
出处 《计算机工程与科学》 CSCD 北大核心 2010年第8期1-6,35,共7页 Computer Engineering & Science
基金 国家自然科学基金可信软件重大研究计划资助项目(90818018)
关键词 可信编译 代码可信赖性 词法分析 微型编译器 trusted compiler trustworthy of source code lexical analysis micro compiler
  • 相关文献

参考文献27

  • 1Wheeler D A. Countering Trusting Trust Through Diverse Double-Compiling[M]. Tucson, AZ: IEEE Computer Society, 2005.
  • 2Boujarwah A S, Saleh K. Compiler Test Case Generation Methods:A Survey and Assessment[J]. Information and Software Technology, 1997,39(9):617-625.
  • 3Yoshikawa T,Shimura K, Ozawa T. Random Program Generator for Java JIT Compiler Test System[C]//Proc of the 3rd Int'l Conf on Quality Software, 2003:20.
  • 4Miller S P, Anderson E A, Wagner L G, et al. Formal Verification of Flight Critical Software[C]//Proc of the AIAA Guidance Navigation and Control Conf and Exhibit,2005.
  • 5Heitmeyer C L, Archer M, Leonard E, et al. Applying Formal Methods to a Certifiably Secure Software System[J]. IEEE Trans on Software Engineering, 2008,34 ( 1 ) : 82-98.
  • 6Feinerer I, Salzer G. A Comparison of Tools for Teaching Formal Software Verification[J]. Formal Aspects of Computing, 2009,21(3) :293-301.
  • 7Yoo J Jee E, Cha S.Formal Modeling and Verification of Safety- Critical Software[J]. IEEE Software, 2009,26(3) :42-49.
  • 8Cowan C,Pu C, Maier D, et al. StackGuard: Automatic Adaptive Detection and Prevention of Buffer-Overflow Attacks[C] //Proc of the 7th USENIX Security Symp, 1998.
  • 9Thompson K. Reflections on Trusting Trust[J]. Communications of the ACM, 1984,27(8):761-763.
  • 10Palmer E R. An Introduction to Citadel - A Secure Crypto Coprocessor for Workstations[C]//Proc of the IFIP SEC' 94 Conf, 1994.

同被引文献43

  • 1王胜军,郭德贵,张晶,金成植.ACCENT生成的语法分析器中多个语法错误检查的实现[J].计算机应用与软件,2007,24(8):75-76. 被引量:2
  • 2许东,费尔伯特.编译原理教学改革初探[C]∥大学计算机课程报告论坛论文集.北京:高等教育出版社,2008:240-242.
  • 3Randy A, Ken K. Optimizing Compilers for Modern Architectures [M]. San Fransisco: Morgan Kaufmann, 2002.
  • 4Xue Jinyun. A practicable approach for formal development of algorithmic programs [C]//Proc of the Int Symp on Future Software Technology. Tokyo: Software Engineers Association, 1999:158-160.
  • 5Xue Jinyun. PAR method and its supporting platform [C]// Proc of the 1st Int Workshop on Asian Working Conf on Verified Software. Macao, International Institute for Software Technology, United Nations University, 2006: 10-20.
  • 6Goldberg B, Zuck L D, Barrett C W. Into the loops: Practical issues in translation validation for optimizing compilers [J]. Electronic Notes Theory Computer Science, 2005, 132(1):53-71.
  • 7Necula G. Translation validation of an optimizing compiler [C] //Proc of the ACM SIGPLAN Conf on Principles of Programming Languages Design and Implementation (PLDI'2000). New York: ACM, 2000:83-95.
  • 8Rinard M, Marinov D. Credible compilation with pointers [C/OL]//Proc of the Run-Time Result Verification Workshop.2000 [2011-12-01]. http://citeseerx, ist. psu. edu/viewdoc/ summary?doi= 10.1.1. 126. 2671.
  • 9Necula G C. Proof-carrying code [C]//Proc of the 24th ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages (POPL'97). New York: ACM, 1997: 106-119.
  • 10Necula G C, Lee P. The design and implementation of a certifying compilers [C]//Proc of the ACM SIGPLAN Conf on Principles of Programming Languages Design and Implementation (PLDI'1998). New York: ACM, 1998: 333-344.

引证文献7

二级引证文献11

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部