张玲波，甘元科，石 刚，王生原，董 渊，张智慧，王沿海

（1.清华大学 计算机科学与技术系，北京100084；2.北京广利核系统工程有限公司，北京100094））

0 引 言

同步数据流语言Lustre［1］广泛应用于航空航天、医疗卫生、高速铁路和核电能源等领域的安全关键系统 （safety－critical system，SCS），但是此类语言的相关开发工具本身的安全性已成为被高度关注的安全隐患之一，同步数据流语言到串行命令式语言的可信编译器的是开发工具的典型代表。普通编译器的确保安全的方法一般有两种，一是通过大量的测试来减少错误，二是通过人工的方法进行检查，这两种方法都是不可靠的，测试的方法无法做到完全覆盖，而人工的方法存在大量不确定因素，因此普通的编译器存在着大量的 “误编译”问题。而采用形式化的方法进行常规编译器的构造和验证已经被证明是成功的，有望最大限度地解决 “误编译”问题。为了实现同步数据流语言可信编译器的形式化验证工作，必须要完成同步数据流语言时态运算向C语言翻译的证明，因此需要采用形式化的方法，从逻辑上对同步数据流语言编译器时态翻译的正确性进行验证，最终将程序的翻译正确性归结到语法抽取和语义定义的正确性上，而成熟的同步数据流语言的语法语义有统一的标准可以借鉴，从而最终在严格的数学逻辑上给出了程序翻译的正确性证明。查，拓扑排序，语言简化，时态消去，最终翻译到Comp－Cert的C前端子集，L2C项目是国际首次对Lustre到C的可信翻译进行的开创性的成功探索。

1 相关研究

Lustre作为一种同步语言［2］，有着严格可靠的数学定义，对于同步范型有着友好的工程设计方法，广泛应用于安全关键系统。同步流语言发展成熟，比较著名的有Lustre，Esterel，Signal，同步语言的一个共同特征是遵循同步假设：当前周期的输入事件出现时，系统能够在下一周期的输入事件出现之前足够快地产生相应于当前周期的输出。Lustre作为同步语言的代表，具有时钟同步和数据流对象的特征，是陈述式语言，具有确定的语义［3］。

Lustre到C语言的翻译已经有比较成功的商用用例，国际著名编译器SCADE［4］已通过多个安全级工业标准 （如军事和航空领域的DO178B）的认证，SCADE成功运用于航空等重要领域，但是SCADE的成功在于对Lustre语言执行的正确性的检测，而对于其中的编译器部分的翻译工作的正确性的验证，仍然是一个急需解决的安全隐患［5］。我们的做法是将Lustre到C语言的翻译，使用Coq［6］定理证明器，通过形式化的定义和证明来机械化的确定程序运行的正确，而Coq除了基本的归纳推导和常规的一阶逻辑外还包含高阶逻辑和依赖类型等高级功能［7］。

形式化的定义和证明有很多成功的例子。学术上著名的CompCert［8］编译器，将C的一个完备子集翻译到Power－PC汇编代码，其正确性证明经过机械化检查，达到了我们所能期望的最高可信程度［9］。X.Yang等关于Csmith的研究工作［10］表明：CompCert在正确性方面的表现明显优于常用的开源或商用C编译器。另一个成功案例是经过验证的内核操作系统seL4［11］，系统在抽象层specification保证了系统运行的内部逻辑正确性，从而提高了系统安全性，进而能有效防止漏洞溢出等攻击手段。

本文源于清华大学软件所Lustre to C（L2C）项目工程。L2C项目的目的是将Lustre语言翻译到C语言的一个完备子集［12］并对翻译进行形式化的验证，保证翻译的正确性。该项目将Lustre语言使用Coq工具定义与验证，由于Lustre语言到C语言跨度较大，因此该项目将划分成多个阶段，保证每个阶段语法或语义跨度不大，用来解决特定的问题。实际上在证明过程中，我们发现本质的问题是无法回避的，但是如果问题叠加在一起，证明的难度将大大增加。图1是L2C项目的阶段图，L2C项目的Lustre语义参考了Lustre v6标准，翻译经历多个阶段，分别是静态检

图1 L2C项目阶段

本文的工作是处于folding层，即将多层周期折叠到一个周期，同时消去时态算子，本层的工作相对独立又非常关键，解决Lustre语言的时态特性，因此翻译相对简单，但是语义跨度较大，证明难度较大，证明是采用构造的方法将中间信息完整的同步到语义分支，并最终完成证明。Lustre语言向C语言翻译的一大障碍就是Lustre的时态特性，这决定Lustre向C翻译的可能性。本文的工作就是将经过简化的Lustre语言的时态特性去掉，即消除Lustre的时钟周期特性，同时还有Lustre的时态操作运算，最终证明时态消去的可行性。

2 Lustre的时钟周期特性

Lustre语言的一个重要特性就是Lustre具有时钟特性，即Lustre语言是一个流语言，具有周期性，并且可以对周期进行操作，比如可以求一个变量的前一个周期的值，而且操作可以互相叠加，因此任意前n个周期的值都是可以求得的，在时钟特性叠加上函数调用就会使得程序比较复杂，但是这在L2C项目S－Lustre＊到Lustre－中已经由化简得到解决。在Lustre－中的变量的表现形式及时态操作运算可以在图2中看到，x在不同周期值可以不同，是一个流数据，arrow操作可以在第一周期赋予表达式不同的值，fby的操作相当于整体往后平移一个周期。

图2 时钟变量及操作

3 Lustre－到LustreF翻译及证明

下面给出Lustre－到LustreF形式化定义和证明的具体做法，为了描述的方便，我们使用M代替Lustre－，F代替LustreF。

3.1 Lustre－和LustreF程序示例

图3 中是M程序的示例，定义了两个节点arrowcall和fbycall，节点中分别使用了arrow和fby的时态操作运算。在arrowcall节点中，输出值y在第一周期的值是0，在后续周期中的值等于输入变量x的值。在fbycall中，输出值z完全等于输入值x，输出值y第一周期值为0，第二周期值为第一周期x的值，第n周期值为第n－1周期x的值：

图3 Lustre程序示便

图4 是图3的M程序翻译对应的F程序，在F中新增加了标志位flagid，每个节点node都有一个flagid，用于区别是否是第一周期，flagid第一周期为false，后续为true，F中节点的调用意义与M是不同的，M是无限流程序，F中对应的就是一个无限循环调用，负责调用节点的外围程序一般调用方法如下：

while（true）

｛

call arrowcall；

call fbycall；

｝

并且在调用之前将会将flagid初始为false。

在图4中，变量p需要特别注意，变量p在最后赋值后，下一轮新的循环开始时，p的值相当于x前一周期的值，从而p起到了 “缓存”的作用，我们称p是自定义变量。

3.2 Lustre－和LustreF的语法和语义

M是经过简化的Lustre，一个完整的M程序主要包含一系列的节点node和指定的主节点node名，主函数作为最初的入口函数，其它节点可以被调用。节点node主要包含参数，返回值，及函数主体，函数主体是有一系列的等式构成，在M中，等式列表中的每个等式都是简化的，仅包含两种基本情况，简单表达式的赋值和函数调用。

图4 LustreF程度示例

简单表达式可以大概的分为两种情况，一种是非时态操作的表达式，包含基本原子，基本原子是指bool、int、real、char等常值或变量，一些基本的运算操作，比如一元运算，二元运算，数据结构，比如结构体，数组，选择表达式，比如if和case，这些表达式是当前时钟当前环境操作，一种是时态操作的表达式，在M中包含arrow和fby两个基本操作，并且操作的元素都是基本原子单元。

F的语法与M的大部分相同，但是没有arrow和fby两个操作，但是在后面可以看到，在新定义的环境下他们的意义将是一样的。这样就是在等价的情况下，去掉了Lustre中时态的部分。

M的语义是用操作语义的形式定义的，在语法基础上进行定义，即判断每一条语法规则所定义内容的语义值，在M的语法大大简化的情况下，M的语义相对比较简单，但由于时态的关系，M的环境仍然是比较复杂的，需要定义保存历史信息的时态环境。

M环境的由全局环境，局部环境组成，每一个节点在每一个周期对应一个局部环境。全局环境存储所有节点node列表，可以通过函数名在全局环境中查找具体的函数。

M局部环境包含时态环境和子环境。本地环境存储一个节点中当前周期的局部变量的信息，这些变量是不重复的，存储的过程也不会出现覆盖的情况，存储的结构体的性质也是经过证明的，保证存和取的都是正确的值，时态环境存储运行至当前周期时所有的本地环境，因此时态环境是一个不断增加的流序列。子环境按照顺序将被调用函数的环境依照链式结构保存下来，节点中被调用函数个数是n，子环境的链式结构长度就是n，而且这个子环境的每个节点都是完整的环境，是递归定义的，因此整个局部环境是复杂的树状结构。

F的环境与M不同的地方在于F没有时态环境，只由本地环境和子环境组成。在F中，子环境需要保存函数调用的情况，因此所有函数的调用，以及被调用函数的函数体的信息都在子环境中定义。

在图5中显示了A调用两次B，一次C，并且C调用B的情况下A的M的环境。A的环境包含历史时态环境te，由本地环境的流序列构成，当需要提取历史信息时，可以通过这个te获得，在本文中我们需要将这个te消除掉，折叠到一个本地环境。函数调用对环境定义的影响也是很大，e＊表示A的子环境，子环境也是一个序列，但是固定长度的序列，长度就是调用node的次数，调用两次B，将会有两个子环境成员，并且两次B的局部环境和子环境都是包含在A的子环境中的，在被调用节点C中也可以调用其它node，比如C调用B，C的子环境将包含被其调用的B的环境，这些都组成了A的环境，可以在上面看到，A的环境是一个复杂并且很完整的信息。在M向F转换的过程中其中的一个目标就是简化这种树状环境，向C语言的扁平的环境靠拢。

图5 环境定义演示

其中arrow和fby的具体语义形式可以在图6中清楚看到，eh表示本地环境，对于arrow来说，第一周期情况下，arrow a1a2的值是a1的值，后续周期情况下是a2的值，对fby来说，fby a1a2的值，第一周期周期情况下为a1的值，后续周期情况下为前一周期局部环境下a2的值。

图6 arrow和fby语义规则

图7 简示函数语义规则

图7 中显示的是F的函数定义的形式描述，函数调用的定义包含了外层调用初始化的情况，在第一周期情况下，第二步flagid初始化是循环外层保证的，下面的三步都是正常的函数调用的基本形式，根据输入执行函数体，得到输出结果，第一步初始化的局部变量locals是M阶段以前翻译过程中形成的变量，在后续周期中，由于只是将局部变量locals初始化，新生成的自定义变量保存了上一个周期的值，fby的上一周期的值能从自定义变量这些 “缓存值”中得到，从而保证能够从M翻译到F中得语义等价，当然这些 “缓存值”在每一次循环中都是不停覆盖的。

3.3 Lustre－与LustreF的翻译

在前面提过M和F的语法相近，但是arrow和fby在语义相同的情况下被替换了，所以重点关注arrow和fby的翻译，为此F的node的形式有了改变，引进两种变量，一种是自定义变量，作为缓存变量存在，用来保存上个周期的值，一种是标志变量，区别是否是第一个周期。有了上面的知识，就可以进行arrow和fby的翻译。

arrow的翻译相对简单，通过选择表达式进行替换，标志变量是分支判断条件，具体形式如下：

｜EarrowM a1a2＝＞

let flag＿atom：＝Avar flagid Tbool in

let clk＿desc：＝EifF flag＿atom a2a1in

let eq：＝EquationF（LhsID lid lty）（ExprF clk＿desc rty）in

（pid，nil，eq，nil）

arrow虽然是时态操作运算，但实际上并不会需要历史周期的值，所以翻译也较为简单，使用EifF语句替换即可。

fby需要保存上一周期值，因此有两个等式来对应翻译，具体如下翻译：

｜EfbyM a1a2＝＞

let flag＿atom：＝Avar flagid Tbool in let pre＿atom：＝Avar pid lty in

let pre＿var：＝VarDeclL pid lty in

let desc1：＝EifF flag＿atom pre＿atom a1in

let eq1：＝EquationF（LhsID lid lty）（ExprF desc1 rty）in

let eq2：＝PequationF（LhsID pid lty）a2in

（Nextpid pid，pre＿var：：nil，eq1，eq2：：nil）

fby需要历史周期的值，所以除了使用EifF语句替换外，还要保存历史周期的值pre＿var。其中第二类等式eq2是特殊等式PequationF，将放在所有其它等式的后面，作为一种新的等式形式，形成的这种新的等式列表的作用主要是用来保存上一个周期的值，这样的翻译也带来了证明的困难，翻译不再是线性的到线性的对应翻译，而是线性的翻译到两段隔开的程序，因此在证明这种非线性映射的需要使用构造的方法，利用构造的定义来描述分割的程序的性质，将在证明阶段给出。

3.4 语义等价的标准

在L2C项目整个翻译的过程中我们进行了多个阶段的分层划分，对于等价的定义我们有比较统一的做法，就是要求程序在输入值相同的情况下，输出结果是一致的，这样在外界调用node将会是一样的效果，从而保证程序的等价。M的语义是一个无限流式的语义，自然在每个周期就会有一组程序输出值，对应的，F的语义将定义成一个无限循环的程序语义，每次循环也将给出一组输出值，然后输入值相同的情况下，M正确执行后的输出值为vrets，推出F正确执行并且输出值为vrets。

语义等价的标准的确定，就是证明目标的确立，证明的过程就从此目标开始一步步证明，因此，等价的标准需要仔细考量，我们对于翻译中统一的标准的也是经过推敲考虑的，一是可以通过这个目标逐步细化到具体的语义定义，第二是能够清楚的反映Lustre程序的特性。具体语义等价的形式如下：

Theorem trans＿programM＿correct：

forall eM eF mainM mainF vargss vretss maxn，

initial＿stateM progM eM mainM－＞

initial＿stateF progF eF mainF－＞

iter＿exec＿programM progM mainM eM 1（S maxn）vargss vretss－＞

iter＿exec＿programF progF mainF eF 1maxn vargss vretss.

这是全时钟周期的等价形式，当化归为每一周期的估值函数时，F中语义的周期数被消除，同时F的语义也消除了时态操作运算。可以在语义等价定义中看到M中的语义是 （S maxn）（即maxn＋1）周期的，而F是执行maxn次的，我们是使用有穷的列表反映周期运行的，在前提对任意maxn而言，既有 （∞＋1）对应∞，具体原因在证明中描述。

3.5 语义等价的证明

上文描述的语义和语义等价是证明的基础，也是问题本质的描述，接下来就是机械化的逻辑证明，而证明的部分也是工作量主要体现的部分和全文难点所在。逻辑证明的过程是分拆的过程，将一些困难的不是显然的大定理拆分成比较容易理解的小定理，证明的过程也是分析的过程，将具体的语义代入到翻译过程中，通过逻辑上推理得出翻译是否正确，证明的最终将分解成最简单的逻辑判断，比如判断id是否相同，结论与条件是否一样等等，而这些都是显而易见的，也是逻辑的基础，Coq也提供了很多的库文件可供使用，而且提供了很多实用的定理，合理的调用能大大的简化证明的过程。总之，证明的方法可以总结为归纳和演绎，归纳是用归纳法从特殊证一般性质，演绎是扩充推广定理，使定理更有普适性，具体证明方法在下面所示。

3.5.1 周期分类证明

在语义中可以看到，M的语义对于第一周期和第二以后的周期是不同的，需要不同的证明处理方法，而第二以后的周期是类似的，证明也可以使用同样的方法，通过这样的观察，我们将证明的过程分两步走，第一步是证明第一周期翻译的正确性，第二步是证明后续周期翻译的正确性，第一周期的正确性证明所需的条件可以在初始化过程中得到，而第二周期后续的证明所缺的条件可以从第一周期中得到。第一周期的执行的过程也是需要注意的，第一周期子环境长度随着代码执行可能会增加 （碰到函数调用增加），其中一些小定理分拆的过程中就需要严格需要这类条件，因此在周期中都是需要仔细的寻找子环境长度这类条件。周期分类最大的作用是区分不同类周期时时态操作运算的前提条件，从而能够成功抽取出不同的条件代入到定理中。

3.5.2 互归纳方法

在语义定义中，函数体执行定义需要使用等式列表执行定义，等式列表执行定义调用了等式执行定义，等式执行定义可能调用了函数而包含了函数体执行定义，所以语义定义是互归纳的方式定义的，证明也必须要用到最小互归纳原理，使用关键词Scheme，即同时假定3个定理原有都是正确的情况下，每次增加特定定理的步长，得到特定定理的增量条件，然后进行证明。由于定理证明的条件较多，因此互归纳增量条件的同步问题是很重要并且富有挑战性的问题，需要对于语义的确切执行有很清楚的认识和预见，增量条件的同步性是很难一步到位的，一般来说，对于互归纳定义的互相调用次数相关，而这种互相调用次数最多可以到是n＊n（n是平行定义个数），所以需要在证明的过程中不断的修改完善增量条件直至证明完成。

3.5.3 构造伴随式定义

在前面已经说明arrow和fby的翻译过程，M与F证明最大的困难来自描述一段代码与对应在两部分不同的位置的代码的信息是一样的，从而M中得一段代码对应F中的一段代码后还有额外的信息，因此在证明中关键是要找一个中间条件，将这额外的信息表述出来，并且传递到第二段代码的证明中。将这个额外的信息传递下去就需要中间条件的定义，这个定义比较复杂，主体的思路是证明F与M的值匹配，这就需要求F的自定义变量在M中的对应表达式，然后再用M中的对应表达式与M中的值进行比对匹配证明，这个定义有两个好处，第一是将F中的自定义变量求值转换为M的表达式的求值，匹配的证明相对容易，第二是定义中间条件将证明的难度拆分开来，分部进行相对容易。而且这个定义也是必须的，缺少中间条件的分支证明条件由于信息缺失而不充分。

下面的伴随式定义就是结合语义构造的给出的解决中间条件问题的方法，而伴随式也是增量条件之一，所以对于不同的定义对应不同的形式，由于F中新定义了一种特殊等式PequationF，所以这种等式不需要互归纳定义。

等式定义对应形式如下：

Definition prevar＿consistance＿peql（ehm ehf：localenvL）（peql：list pequationF）：Prop：＝

forall peq v，

In peq peql－＞

eval＿atomL ehm （atomOfpeq peq）v－＞

ehf！（pidOfpeq peq）＝Some（v，typeOfpeq peq）.

等式定义虽然对应的是当前周期的值，结合M函数体执行定义可知，每次M的历史环境都会增加一个，所以在下一周期中得到了前一个周期的值，这也是恰好能够证明fby算子消去的关键！W函数执行和子函数调用执行对应形式采用互归纳定义，同时函数执行定义对应形式调用等式定义对应形式。

这些伴随式定义在证明的过程中起到了桥梁的作用，自然而然的会在使用的时候需要它们的很多性质作为保证，所以如果定义复杂的伴随式将会极大的增加证明的困难，这也是构造的难点之一，因此伴随式需要在基于语法语义和翻译的观察基础上不停地简化。

3.5.4 消除周期的代价

M时态周期的消除并不是没有代价的，这加大了F中环境的定义信息，F的环境中包含了函数体的信息，这才能完成伴随式函数定义和构造。从而F中子环境定义比较复杂，保存了子函数调用的情况，而子函数调用在等式列表的位置是未知的，需要搜索才能得知，所以在证明的过程中还需要保证子环境与函数体信息的一致性匹配，为此专门定义了F的子环境调用函数的一致性匹配性质，在证明的过程中始终贯穿了这个一致性匹配性质，并且这个性质对证明过程中函数调用情况的也提供了必要的条件信息。实际上最小互归纳原理的其中一个必要条件就是子环境与函数的一致性匹配。

3.5.5 周期的对应

大定理周期是 （maxn＋1）个 M周期对应F中maxn次循环，原因是M中fby时态运算操作中取前一个周期值的原子是不符合拓扑排序关系的，即EfbyM a1a2中得a2可能没有在前面被赋值，而伴随式又需要a2当前周期存在值，解决方法是加入下一个周期的函数执行作为条件，下一个周期函数执行时，对于前一周期的a2有值，而下一周期的前一周期即是当前周期队尾，就满足了伴随式的条件，所以证明是两个周期对应一次循环，即M的一二周期对应F的第一次循环，M的二三周期对应F的第二次循环，以此类推。

总之，证明的过程是个逐步细分的过程，证明的过程中直观的判断往往是正确的证明方向，但是也可能会在细节出现问题，这种情况就是直觉的疏忽错误导致的，也有可能对语义定义的理解虽然相同，但定义方法不同，使程序证明的难度加大，这都需要回溯修改，直至证明完成。证明的最终都是对语法语义的逻辑推理，因此语法语义也是重要和基础的，是对程序运行的理解，而证明的过程是对理解的细化推理，而程序运行的复杂性也将加倍的反映在证明中。证明最重要的结果是逻辑上保证程序翻译的等价性，从而在M程序执行正确的情况下，保证F程序也会正确执行，并输出正确结果。

4 结束语

本文是从一个编译器的时态翻译层出发，演绎了使用Coq程序证明翻译的一般方法，形式化证明了Lustre时态特性与C循环特性的一致性问题，从而保证了Lustre程序向C程序转化过程中时钟可消除的特点。本文使用Coq证明工具实现，Lustre－语法语义定义约140行，LustreF语法语义定义约170行，翻译工作约100行，等价性的证明过程约2500行。

随着计算机软件业务发展，人们对软件的安全可靠的标准越来越高，形式化定义与证明验证为解决这个问题的提供了一个高标准的实现方法，能够从程序本质上进行逻辑推断，从而达到高可靠性，而形式化的方法的工作量相对比较大，因为证明的工作需要从逻辑上遍历程序执行所有可能出现的情况，从而得出程序正确执行的结论，因此在关键代码上使用形式化验证的方法能有效提高整个系统的可靠性。

［1］Pouzet M，Raymond P，Cohen A，et al.Synchronous objects with scheduling policies ［C］／／ACM International Conference on Languages，Compilers，and Tools for Embedded Systems.Springer，2009：11－20.

［2］Benveniste A，Caspi P，Edwards S A，et al.The synchronous languages 12years later［J］.Proceedings of the IEEE，2003，91 （1）：64－83.

［3］Papailiopoulou V，Seljimi B，Parissis I.Automatic testing of LUSTRE／SCADE programs ［J］.Model－Based Testing for Embedded Systems，2012，13：171－194.

［4］Dormoy F X.Scade 6：A model based solution for safety critical software development ［C］／／Proceedings of the 4th European Congress on Embedded Real Time Software，2008：1－9.

［5］Leroy X.Verified squared：Does critical software deserve verified tools？ ［J］.ACM SIGPLAN Notices.ACM，2011，46（1）：1－2.

［6］Paulin－Mohring C.Introduction to the Coq proof－assistant for practical software verification ［G］.LNCS 7682：Tools for Practical Software Verification.Berlin：Springer Berlin Heidelberg，2012：45－95.

［7］Bertot Y.A short presentation of Coq ［G］.Lecture Notes in Computer Science 5170：Theorem Proving in Higher Order Logics.Berlin：Springer Berlin Heidelberg，2008：12－16.

［8］Le Sergent T.SCADE：A comprehensive framework for critical system and software engineering ［G］.Lecture Notes in Computer Science 7083：Integrating System and Software Mode－ling.Berlin：Springer Berlin Heidelberg，2012：2－3.

［9］Morrisett G.Technical perspective a compiler’s story ［J］.Communications of the ACM，2009，52 （7）：106－106.

［10］Yang X，Chen Y，Eide E，et al.Finding and understanding bugs in C compilers［J］.ACM SIGPLAN Notices，2012，47（6）：283－294.

［11］Klein G，Elphinstone K，Heiser G，et al.SeL4：Formal verification of an OS kernel［C］／／Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles.ACM，2009：207－220.

［12］Blazy S，Leroy X.Mechanized semantics for the Clight subset of the C language ［J］.Journal of Automated Reasoning，2009，43 （3）：263－288.