随着计算机控制系统在人们生活中的普及,软件自身的可靠性也越来越受到重视.在航空、高铁、核电及军事等高安全要求领域的软件系统——安全关键系统(safety-critical system,简称SCS)更是受到高度的重视.而随着软件系统的复杂度越来越高,软件系统的安全性保证也变得越来越困难.这些系统的开发,仅仅依靠过程规范、代码审核和系统测试来保证软件安全还远远不够,通常需要采用形式化验证方法来保证软件可靠性.全数字实时仿真平台SkyEye的同步数据流语言可信编译器的构造在某些安全性严格要求的领域,不但对目标系统的开发需要形式化方法来保证,而且开发过程所需工具,如编译器等,也必须经过形式化验证.
同步模型与同步数据流语言
工业生产中的很多实时系统(如控制系统)都是响应系统,它是以环境决定的速率对环境做出连续响应的系统.此环境可以随时提供新的输入,系统通过运算产生新的输出,使得程序不断地与环境进行交互,且以并发的方式体现.
同步模型是为了适应响应系统而开发的程序运行模型.它把响应系统分成连续的原子时间片(响应周期),每个时间片又分成事件采集、逻辑运算和事件发射这3个阶段,从而有效地满足响应系统的要求.在同步模型中,事件的采集、逻辑运算和事件的发射必须在同一个响应周期内完成,这称为同步模型的同步假设.时间片的大小是由响应系统的环境决定的.同步假设的有效性检查,就是评估系统对环境的最大响应时间能否满足环境要求.图 1为同步模型示意图.
编译器的可信
对于编译器来说,可信的具体指标就是其正确性,要保证从源程序到目标程序的翻译过程正确,即,保证源语言的特征被正确、完整地实现,能够实现语义保持性,杜绝误编译.
为了保障编译器实现的正确性,传统的方法是通过大量的测试.例如,GCC(4.7版)的torture测试集包含2 853个C源程序用例,商用的Plum Hall Standard Validation Suite for C有29 424个用例,Lustre V6的开源软件包中含有140个左右的源程序用例,等等.还有一些Bug-hunting工具(如Csmith)可能产生更多或更独特的源程序用例.
然而和其他软件一样,通过测试只能发现错误,并不能保证编译器是正确的.Scade工具的代码生成器KCG或许是获得民用航空软件生产许可的第一个商用编译器,其设计开发过程(很严格的V&V过程)符合民航电子系统的国际标准DO-178B,并成功应用于空客(airbus)A340和A380的设计中.尽管如此,这并不足以说明Scade的编译器不存在“误编译”.事实上,业界已经发现Scade KCG的某些翻译漏洞.
为增加编译器的安全和可信程度,仅通过测试和严格的过程管理都是不够的,人们很自然地会想到形式化验证的途径.在CC(common criteria)安全评估标准中,将可信性分为7个级别(EAL1~EAL7),级别越高,形式化规范和验证的程度越高.航空无线电委员会(RTCA)近期也已推出民航电子系统的国际标准DO-178C,与DO-178B相比,增加的内容包括了对形式化规范和验证的要求.
人们在几十年前就开展了编译器形式化验证的工作:McCarthy等人在1967年手工证明了一个简单编译器(从算术表达式翻译到栈式机目标代码)的正确性;随后,Milner等人在1972年给出了相应的机械化证明;Dave于2003年的综述列举了从1967年~2003年的大部分相关工作,包含从针对简单语言的单遍编译器到较成熟的代码优化遍等形形色色的工作.近年来,随着技术的不断进步,已经可以验证较为复杂的编译器.例如,Leroy等人开发的验证过的C编译器CompCert,Chlipala给出一个从非纯函数式的语言到汇编语言的一个经过验证的编译器,Klein等人验证了一个从Java核心子集到Java虚拟机的编译器.
CompCert编译器是经过验证的可信编译器的杰出代表.该编译器将C的一个重要子集Clight翻译为PowerPC汇编代码(目前也支持IA32后端),使其可以直接用于范围广泛的嵌入式应用开发.该编译器包含了许多分析与优化,所生成的代码可与gcc-0产生的代码匹敌.该编译器将编译过程划分为多个阶段,每个阶段的翻译正确性(语义保持性)都借助辅助定理证明器Coq进行了证明,且这些证明可由独立的证明检查器检查,这使得CompCert的中间层转换过程达到了我们所能期望的最高可信程度.最近,Yang等人在关于Csmith的研究工作中对主流的C编译器进行测试,共报告了325个bugs,其中包括Intel CC,GCC和LLVM等.在所比较的11种开源或商用的C编译器中,CompCert表现较为突出,在6个CPU年中,其中间转换过程没有发现bugs.
编译器验证的另外一种可选方案是翻译确认(translation validation).翻译确认(translation validation)是 Pnueli等人首先提出来的.他们采用翻译确认的方法来验证同步数据流语言的翻译(或编译)过程,所给示范例子的源语言是Signal特征的多时钟同步数据流语言,目标语言是C.翻译确认的方法不是直接验证翻译程序,而是用统一的语义框架为某一翻译过程的源和目标代码建模,两个模型之间定义一种求精(refining)等价关系,设计一种可自动证明二者等价性的分析程序(成功时可给出证明脚本,不成功时给出反例),再给出一种独立的证明检查器(proof checker),可最后确认翻译的正确性.
在L2C项目中,我们选择了对编译器本身进行验证.当源语言和目标语言的语义定义达到认可的程度时,原理上可以保证源程序的一般性质都可以保持到目标程序.与上述翻译确认的做法相比,这是一种彻底的做法;而基于翻译确认的方法往往只是关注部分性质的保持性(当然,也可以逐步逼近一般性质).然而,这项工作相当艰巨,正如前述Pouzet等人的项目,是一项长期的工作.然而,我们的考虑是:1) 实际中有值得这样做的需求; 2) 如果在面向验证的编译器结构上下功夫,加强证明过程的局部化和模块化研究,可减轻需要扩展和维护时的负担;3) 在某些扩展和维护工作量过大的翻译阶段,还可以采用翻译确认的方法作为补充,比如CompCert项目,也有个别阶段采用了翻译确认方案;4) CompCert项目的成功,告诉我们这一选择的重要价值和可行性.
标题：全数字实时仿真平台SkyEye的同步数据流语言可信编译器的构造
链接：http://www.digiproto.com
