前言

随着信息技术的发展和普及,软件在计算机系统中的作用越来越重要.软件的可信性受到了日益广泛的关注.高级语言编写的软件必须经过编译才能在硬件上执行,因此编译器的可信性直接影响软件的可信性.概括地讲,可信编译是指编译器在保证编译过程正确性(编译前的源代码和编译后的目标代码语义一致)的同时,确保生成的目标代码是可信的.可信编译器不仅仅实现语义保持的代码转换功能,还     

可信编译理论及其核心实现技术:研究综述

编译器是重要的系统软件之一,高级语言编写的软件都必须经过编译器的编译才能成为可执行程序。编译器的可信性对于整个计算机系统而言具有非常关键的意义,如果编译器不可信,则很难保证系统所运行软件的可信性。可信编译是指编译器在保证编译正确的同时提供相应的机制保证编译对象的可信性,对可信编译理论和技术的研究具有重要理论意义和实用前景。阐述了可信编译器的概念,介绍了编译过程正确性的形式化定义,对可信编译的主要研究进行了概括。在全面分析可信编译研究现状的基础上,从编译器自身可信性和确保编译对象可信性两个方面,对可信编译器设计和实现的相关理论和方法进行了分类和总结。最后,讨论了可信编译有待解决的问题和未来的研究方向。     

一个面向方面的可信软件开发平台TSCE*

随着软件规模和复杂度的增加,软件失效和故障问题日益加剧。如何在开发阶段利用开发环境为实现软件可信性提供有效支撑,从而确保软件运行行为与预期保持一致,具有重要的研究价值。借助面向方面的设计思想,把可信性作为一种方面融入软件的开发环境,研究实现了可信软件开发平台TSCE。该平台能够在软件研制过程中,一体化地提供可信性需求定制、可信代码自动生成、可信代码自动织入等辅助开发手段。利用该平台,开发人员不用额外编写可信性实现的相关代码,便可在部署运行阶段使软件具有一定的可信性判断能力和故障预警与修复能力。     

信息安全中的可信软件编程计算研究

针对IT产业迅速发展、互联网广泛应用和渗透,各种各样的威胁模式不断涌现的现状,结合传统软件质量的对比分析,提出了信息安全中的重要因素——可信软件编程计算。重点研究代码可信性分析、计算和度量方面,涵盖软件的复杂性、可用性和可靠性等质量特性及可信属性,对于软件质量保证和信息安全具有非常重要的现实意义和实用价值。     

基于形式化监控的可信软件构造模型

传统的形式化方法和软件运行时监控都是提高软件可信性的有效途径,但存在监控需求表达能力不强及代码分散等问题。针对该问题,提出基于形式化监控的可信软件构造技术FM-TSPM,将形式化方法和运行时监控相结合,实现跨领域的方法融合。用形式化方法描述监控约束,根据监控约束生成方面监控代码,解决代码分散问题。采用AOP编织器将方面代码编织到目标系统中,构造出带监控能力的可信软件。     

一种基于中间件的可信软件保护模型

软件的可信性是可信计算的研究热点之一。首先描述了可信计算平台和可信平台模块的基本概念,接着结合安全中间件和可信计算模型,在现有的PC体系结构下,提出了一种具体的基于中间件的可信软件保护模型,着重介绍了新模型的体系结构和系统组成,最后通过实例对软件保护机制进行了详细的说明。新模型具有通用性强和易于实现的特点,对于软件可信性保证的研究以及软件可信保护系统的建立具有一定的意义。     

软件可信性动力学特征及其演化复杂性

可信软件已成为现代软件技术发展和应用的重要趋势和必然选择,而软件可信性建模已成为构造可信软件的先决条件和必要手段.为了探讨和阐明软件可信性的基本科学问题、建立软件可信性度量的理论基础,文中结合动力系统的基本思想探讨软件可信性及其演化规律,研究在各种内部和外部因素作用下软件可信性演化的动力学机制,并建立相应的动力学模型,从而软件系统的可信性可以认为是软件系统在动态开放环境下其行为的统计特性.通过对两个简单实例的建模分析,说明了软件系统可信属性的极限演化行为与动力系统特征的对应关系,诠释了软件可信性的动力学特征及其演化复杂性.     

基于构件的可信软件系统冗余机制及可靠性分析

在高可信软件的设计和开发中,软件容错是提高系统可信性的一种实现技术之一. 容错性就是指软件在故障出现时保证提供服务的能力,对退化故障进行容错的一种处理方式就是依靠冗余技术. 本文在分析结构冗余及其对可信性的影响的基础上,在基于构件的可信软件系统中提出了对核心构件进行冗余的机制,包括单个构件的双模冗余结构、组合构件的双模冗余结构和构件的三取二冗余及其扩展结构,并给出了其故障检测和判断方法. 同时,在各种冗余结构的基础上对系统可靠性能进行分析.     

一个C语言安全子集的可信编译器

以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器.然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估.之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器.最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率.     

同步数据流语言输入结构体的可信翻译

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.     

Deriving correctness properties of compiled code

When developing safety-critical software, it is the correctness of the object code that is paramount. However, it is desirable to perform formal verification on the source program. To ensure that correctness results proved about the source program do apply to the object code, the compiler used can be formally verified. However, care must be taken to ensure that the compiler correctness theorem proved is suitable. We have combined a derived programming logic with a verified compiler for a generic subset of the Vista structured assembly language. We show how correctness properties of object code can be formally derived from corresponding correctness properties of the source program which have been proved using the programming logic. Thus we can be sure the results do apply to the object code. The work described has been performed using the HOL system and so is machine-checked.     

基于确认式编译技术的移动代码安全性研究

应用确认式编译技术解决移动代码的安全性问题是国际上新近开始研究的方法,其最大特点是把确保满足安全策略的主要任务由代码消费方转移到代码生产方,可以有效解决代码消费方运行时负担过重的问题;此外,它是对代码本身进行验证,而不是对代码产生方的身份进行验证,因而可信度更高并可以支持匿名代码。本文对该研究技术进行了分析,从中可了解到：支持更高级别的安全性是这种技术获得更广泛应用的焦点;并针对这种需求,在该文中穿插介绍了我们的工作设想,以期与同行分享。     

一种基于可信计算技术的源代码安全审查模型

在现阶段的大规模软件工程开发中,源代码数量已经变得越来越庞大,动辄就是数百万,甚至是数千万行以上.随着源代码数量的激增,代码的逻辑越来越复杂,相互之间的调用关系越来越繁复,代码的安全漏洞也越来越容易出现.常规的人工检查和调试已经完全不能满足庞大的系统软件的审查需求.此时,常在源代码正式发布之前,使用安全代码审查机制来快速找出系统中绝大多数的安全漏洞.针对这一问题,文章结合传统的代码安全审查原理和当前流行的可信计算技术,提出了一种基于可信计算技术的源代码安全审查模型.在代码的安全审查过程中,利用可信计算的可信度量原理的审查方法,结合运用安全操作系统的访问控制机制,检测出源代码中可能不符合可信计算理论的系统资源访问,防止主体触发来源不可信或已被篡改的代码,从而实现对各种已知和未知恶意代码的防御,让最终的代码在运行时符合可信计算标准.该模型通过将不同的软件进行类型分级,从而确定不同软件对系统资源的不同使用权限.使用文中规范开发的代码遵循可信计算标准,可以杜绝恶意代码对系统资源的不安全访问.     

Evaluation of fortran vector compilers and preprocessors

Many scientific codes can achieve significant performance improvement when executed on a computer equipped with a vector processor. Vector constructs in source code should be recognized by a vectorizing compiler or preprocessor. This paper discusses, from a general point of view, how a vectorizing compiler/preprocessor can be evaluated. The areas discussed include data dependence analysis, IF loop analysis, nested loops, loop interchanging, loop collapsing, indirect addressing, use of temporary storage, and order of arithmetic. The ideas presented are based on vectorization of over a million lines of production codes and an extensive test suite developed to evaluate preprocessors under varying degrees of code complexity. Areas for future research are also discussed.     

Do you trust your compiler?

As our society becomes more technologically complex, computer systems are finding an alarming number of uses in safety-critical applications. In many such systems, the software component's reliability is essential to the system's safe operation, so it becomes natural to ask, “How can software be made to behave correctly when executed?” Using program transformations to produce trusted software simplifies verification. Program transformations use proven laws to manipulate programs in a manner analogous to algebraic transformations. The authors sketch how a formal method based on program transformations can be used to construct a verified compiler. Such a compiler has been proved to correctly compile any correct program into assembly language. While the compiler itself may not execute efficiently-after all, you need only use the verified compiler the last time you compile a program-the transformational approach should enable the verified compiler to produce efficient assembly code     

为VLIW处理器的特殊功能部件生成代码的新方法

通用的高级程序设计语言的编译器,比如C的编译器,不会为VLIW处理器的特殊功能部件自动生成代码。通常通过汇编语言来使用这些特殊功能部件,但是这个方案有着它的不足。笔者提出了一种新的方法来解决这些问题。定义了一种可视化并行建模语言VRTL-P,使用它来描述不同操作间逻辑上的可并行性。笔者还实现了一个VRTL-P的在线分析器,它可以根据VLIW处理器的具体实现来判断一组操作是否可以拼装到一条VLIW的指令中。还进一步研究了从VRTL-P生成目标代码和仿真执行VRTL-P的方法。通过使用这些技术,可以为VLIW处理器的特殊功能部件生成高质量的代码,并且可以提高软件的生产率。     

一种用于Java虚拟机的类型化低级语言

为了能够减小运算系统的需信任计算基础、描述较小粒度的安全策略，目前的研究倾向于从程序设计语言和编译器入手来提高软件的安全性．基于以上研究背景设计了一种类型化的低级语言TLL,TLL是一种为Java虚拟机即时编译器设计的类型安全中间语言，以构造一个具有更小需信任计算基础的Java虚拟机系统为目的．TLL的类型系统基于多态的类型化λ演算，它具有丰富的表现力且能够编码各种高级语言的抽象．基于TLL的一个虚拟机原型系统已经实现，它可以作为实现一个高安全且面向多种源语言的运行时系统的起点．     

基于硬件cache锁机制的Java虚拟机即时编译器优化

Java虚拟机即时编译器以方法为单位进行编译,编译器将字节码方法编译成可执行代码,并经过数据cache存入内存中,当再次执行到该代码段时,处理器需要从包含该代码段的内存区域取指令执行,如果该内存区域在数据cache中已经建立映射,就可以直接从数据cache中读取数据,读数据的性能就会有大幅度的提高.但是编译生成的大量可执行代码在cache中频繁替换,当生成代码被替换出cache后,代码再次执行时处理器必须访问速度较慢的主存储器,成为编译器的性能瓶颈.设计并实现了硬件cache锁机制,提出了一种软硬件协同设计的即时编译方法.通过该方法,生成代码执行时的cache失效次数降低了6.9%,SPECjvm2008中程序最高获得了17.9%的性能提升,平均性能提升4.2%.