_mJava到Micro-Dalvik虚拟机的编译验证

针对类Java的面向对象语言mJava到类Dalvik的寄存器架构虚拟机Micro-Dalvik的编译验证,给出了mJava语言和Micro-Dalvik的操作语义.从mJava语言程序到Micro-Dalvik虚拟机指令的编译分为两步,首先将mJava语言程序中的本地变量名转换为相应的序号,得到一个中间语言程序,再将该中间语言程序翻译成Micro-Dalvik虚拟机指令程序.在给出中间语言的操作语义后,构造了mJava语言程序与编译后的中间语言程序的语义保持定理并证明,以及构造了中间语言程序的语义与编译后的Micro-Dalvik虚拟机程序的语义保持定理并证明.整个形式化编译验证在定理证明助手Isabelle/HOL中进行了机器检测.mJava语言和Micro-Dalvik虚拟机分别对Java语言和Dalvik虚拟机进行了抽象,是我们兼顾语言的真实性和形式化的清晰性的结果.但是,所有形式化的语义严格遵从语言规范中的定义,并与Dalvik VM的实现保持一致,从这种意义上讲,该编译器并不是一个实验性质的假想编译器,而是有其实用意义的.

面向龙芯处理器的一种CompCert可信编译器重定向实现

CompCert是著名的C语言可信编译器,它借助于交互式定理证明工具Coq实现,能够确保生成的目标汇编代码保持源代码的语义,具有极高的可信度,近年来被广泛应用于学术界和工业界的许多安全攸关任务的研发工作中。CompCert编译器的当前版本支持多种目标机结构,然而目前尚缺乏针对国内自主研发处理器的版本,如龙芯(Loongson)处理器体系结构(LoongArch)。将CompCert重定向到龙芯等国产处理器,对我国安全攸关软件领域的发展大有裨益。本文对CompCert编译器的设计理念、框架结构和龙芯架构的特点进行分析,改造CompCert编译器的后端,使其可以生成能在龙芯处理器上运行的汇编代码,并细致阐述不同模块的工作内容。重定向到龙芯处理器的CompCert编译器具有接近GCC-O1的性能,可满足许多场景的使用。

同步数据流语言可信编译器的构造

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.

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

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

可信编译器L2C的核心翻译步骤及其设计与实现

同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如Comp Cert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(Comp Cert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.

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

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

同步数据流语言可信编译器的研究进展

同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。构造可信编译器的途径可分为两大类:一类是传统的方法,例如通过大量测试和严格的过程管理等手段来实现;另一类是通过形式化方法,例如直接对编译器本身进行形式化证明,采用翻译确认的方法等。近年来,形式化方法作为构造和验证可信编译器的关键途径而得到广泛的重视,有望最大限度地解决"误编译"问题,因而成为新的研究热点。文章在介绍可信编译器的形式化构造和验证方法的基础上,特别聚焦于同步数据流语言可信编译器的相关研究工作,对其现状进行综述和分析。

CompCert编译器目标代码生成机制分析

CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中。CompCert编译器的当前版本支持多种目标机结构。文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其设计逻辑、翻译过程、语义保持性以及代码结构,并给出了CompCert编译器重定向设计的要点。文中工作有助于实现CompCert重定向,比如实现面向重要国产处理器的后端。

同步数据流语言可信编译器Vélus与L2C的比较

同步数据流语言(如Lustre、Signal)在航空、高铁、核电等安全关键领域得到广泛应用。例如,适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言。这类语言相关开发工具,特别是编译器的安全性问题也自然受到高度关注。近年来,基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点之一,也取得了瞩目的成果,如CompCert项目实现了产品级的可信C编译器。同样,人们也采用这种方法开展了同步数据流语言可信编译器的研发工作。主要关注从事这一工作的两个长线项目,二者均研发面向基于Lustre的同步数据流语言编译器,分别以Vélus和L2C代称。对Vélus和L2C从多个重要的角度进行较为深入的分析与比较。

一种适用于可信编译器的源语言转换与检查框架

针对当前可信编译器对源语言处理能力的局限,提出了1个适于可信编译器的源语言转换与检查框架,将命令式源语言程序转换为可信编译器可接受的等价的函数式语言程序,通过语法支持、良构性和异常发生三方面的检查,保证了可信编译器对转换后的代码的可接受性以及代码本身较高的可信性。

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

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

一种类型化低级语言的设计与应用

介绍了以构造一个具有更小的需信任计算基础的Java虚拟机系统为目的的研究工作,将一种类型安全的低级语言TLL应用到Java虚拟机的即时编译器中.TLL的类型系统基于多态的类型化λ演算,它具有丰富的表现力且能够编码各种高级语言的抽象.基于TLL的一个虚拟机原型系统已经实现,它可以作为实现一个具有微小的需信任计算基础的Java虚拟机的起点.

嵌入式处理器P2020机器码程序到C语言源程序的溯源方法

处理器PowerPC P2020在航空航天等嵌入式领域被广泛应用,以RTCA/DO-178C中A级软件的适航要求作为研究的出发点,提出了从文件、函数声明、函数体代码3层次实现P2020机器码程序到C源程序的溯源方法。在获取C语言源程序与PowerPC P2020机器码程序文件名列表的基础上,实现PowerPC P2020机器码文件主名的溯源;通过遍历C源程序抽象语法树和PowerPC P2020机器码获取函数名列表,实现PowerPC P2020机器码函数声明的溯源;通过定义C语言程序抽象语法树节点生成期望汇编指令序列的规则,实现PowerPC P2020机器码函数体的溯源。通过设计245个C源程序文件与345个PowerPC P2020机器码程序文件,1111个C语言函数声明与1273个PowerPC P2020机器码函数声明,以及覆盖C语言程序23类语法结构的460个测试用例,验证了PowerPC P2020机器码程序到C源程序的自动化溯源方法的有效性。结果表明:文件溯源和函数声明溯源的追溯匹配率达100%,程序函数体代码的平均溯源匹配率达97.22%。溯源匹配结果可以检查PowerPC P2020机器码程序是否在编译过程插入例外异常代码,以防止其带来的安全隐患,保证航空航天嵌入式安全关键软件机器码的安全性和可靠性。