可信编译器中地址不相交的保持性证明

★北京广利核系统工程有限公司 谷伟卿，张智慧，白涛，齐敏

可信编译器中地址不相交的保持性证明

★北京广利核系统工程有限公司 谷伟卿，张智慧，白涛，齐敏

同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言，在同步数据流语言到顺序执行语言的翻译转换过程中，语义等价要保证赋值语句的左右值地址互不相交，这至关重要。本文使用形式化方法描述了翻译过程中地址互不相交的性质，并通过定理证明的方式对其进行了验证。基于本方法的编译器在某核电站的安全保护系统中得到了应用。

同步数据流；定理证明；Coq；语义等价；地址不相交

1 引言

核电等安全关键领域中的软硬件系统的可靠性越来越受到重视，这些系统的设计错误会带来巨大的人身财产损失，所以对其功能设计的正确性验证越来越受到重视。而传统的编码设计方式对工程设计人员带来很大的困扰——开发效率低下、质量没有保证[1]，故算法组态软件成为工程设计应用的主流软件，组态软件的核心是编译器，如果编译器不可信，则很难保证系统所运行软件的可信性。[2]

核电领域应用甚广的设计语言为Lustre——同步数据流语言，而我们的目标代码为C语言。目前大多使用国际著名的SCADE工具[3]来将Lustre编译成C代码。SCADE工具虽然已获得广泛的应用，但是其编译器KCG尚未经过严格的形式化验证，它采用传统的测试方法无法达到全覆盖，在高可靠领域的应用仍然存在考验。

形式化验证[4]根据某些形式规范或属性，使用数学的方法证明系统的正确性或非正确性，包括等价性验证、模型检测和定理证明[5]。其中定理证明用数学方法表达系统的规范和性质，从逻辑上判断设计的正确性，是最为严格和规范的方法，其结论的可信度也最高。定理证明系统基于已有的推理规则、公理和定理对要验证的系统进行建模和推理，定理证明系统包含的理论库越多，其建模和推理能力就越强。其中交互式定理证明工具Coq是在工业界和研究领域被广泛应用的。它提供大量的基础性质的形式化证明库和证明策略。Coq有坚实的数学基础，并能用同一语言描述程序、性质和证明等形式化验证的全过程。[6]

为提升核电系统设计的安全性，我们开发了一款经过形式化验证的自动化工具“Lustre编译器”，将图形化控制逻辑自动翻译为符合IEC60880要求的C程序。编译器是将高级语言转换为较为低级的语言，将一个高级语言的操作进行拆分转换为多步简单的操作。由于同步数据流语言Lustre和Clight（C的一个子集）存在着巨大的差异，Lustre具有时钟同步、数据流、并发及流数据对象等特征，而Clight则具有顺序控制流特征，在翻译转换的过程中，会新产生中间变量或赋值结构，我们在编译器的前端检查保证了源语言中变量和赋值语句左右值互不相交，如何将此性质始终贯穿翻译过程，保证在每一层的转换之后地址互不相交至关重要。

本文其余部分组织如下：第一部分介绍相关工作。第二部分介绍Lustre编译器的总体实现框架。第三部分介绍其中一次转换前后的语法语义定义。第四部分介绍关键性质——左右值不相交的保持性定义和证明。第五部分总结与展望。

2 相关工作

工业组态软件SCADE的内置编译器为KCG，其采用严格的V&V过程管控实现了从Lustre到C的可靠翻译，然而，这些方法并不能完全避免误编译的发生。[7]

国外的Compcert是一款经过形式化验证的，采用Coq来分步实现C的子集Clight到PowerPC汇编代码的翻译过程的C编译器。[8]其采用Coq来分步实现C的子集Clight到汇编的翻译过程，用Coq定义中间过程的语义，并用交互式定理证明器证明每个步骤在对应的语义中执行等价。相比普通的验证技术，形式化验证能在数学的层面对软件的逻辑进行抽象和证明，因此具备更高的安全性。

目前，业界还没有经形式化验证的方法来实现从Lustre到C的编译器。由于同步数据流语言Lustre和Clight之间的巨大差异，为降低证明过程的复杂程度，我们将翻译过程拆分成多个层次，保证每个层次语法和语义跨度不大，每个层完成特定的工作，比如时钟归一化、拓扑排序、消去高阶运算等工作[7-13]已由合作者完成，本文的研究工作基于前面的翻译证明工作展开。

3 Lustre编译器实现框架

如图1所示，为Lustre编译器总体结构。

图1 Lustre编译器总体结构

转换过程分为以下步骤：Lustre＊到Well-Typed Lustre＊（又称LustreI）：前端的词法、语法分析及静态语义分析；LustreI到LustreS（PreProcessing）：翻译全局常量、拆分表达式列表、翻译类型、消去枚举类型和化简高阶运算；L u s t r e S上的（TopoSorting）：拓扑排序；LustreS（排序后）到LustreQ（ClassifyConstVar）：将常量变量从变量列表分离；LustreQ到LustreT：高阶操作符的语义变换；LustreT到LustreT1（TransHighorder）：将高阶统一翻译成for循环的形式；LustreT1到LustreT2（TransMainArgs）：主节点的输入参数翻译为结构体；LustreT2到LustreT3（TransMainRets）：主节点的输出参数翻译为结构体；LustreT3到LustreR（TransTypecmp）：生成数组和结构体比较函数；LustreR到LustreN（Lr2ln）：对节点列表中的函数和节点的分类；LustreN到LustreF（TransTempo）：消去时态运算；LustreF到LustreE1（Lf2le）：生成节点对应的结构体类型；LustreE1到LustreE2（ClassifyRetsVar）：从变量列表中分离节点返回值；LustreE2到LustreE3（TransReset）：生成初始化函数列表；LustreE3到LustreE4（SimplEnv）：将所有节点的返回值翻译成结构体，并将调用节点的call运算翻译成结构体的一个实例的调用；LustreE4到LustreD（ClassifyArgsVar）：从变量列表中分离节点输入参数；LustreD到Clight（ClightGen：CtempGen、TransCtemp）：到C的语法翻译和证明，将memcpy内存拷贝语义翻译为内存拷贝函数。

本文所做的工作主要是对翻译过程中左右值地址不相交性质的保持性进行形式化定义和证明。

4 语法和语义定义

在翻译过程中左右值地址不相交性质贯穿始终，对于普通类型的赋值运算可直接赋值，而对复杂类型，如结构体和数组类型的赋值需要满足左右值地址不相交的性质，因为复杂类型的赋值需要翻译到memcpy，memcpy的运算需要左右值地址范围不相交。另外结构体和数组类型的输入参数在Clight中需要翻译为指针的形式，返回值也需要翻译为指针，这就要求call调用的左右值地址范围也不能相交。

在以上翻译过程中：

（1）将高阶统一翻译成for循环形式的过程（TransHighorder）；

（2）将所有节点的返回值翻译成结构体，并将调用节点的call运算翻译成结构体的一个实例调用过程（SimplEnv）；

（3）到C的语法翻译和证明，将memcpy内存拷贝语义翻译为内存拷贝函数过程（CtempGen）；

这三个步骤包含了生成结构体、数组和call调用的过程，本文针对SimplEnv的翻译转换过程进行左右值地址不相交证明进行举例说明。

4.1 语法

虽然在翻译过程中分成多层，但是有些中间语言与其他语言的语法相同或相似，差别很少。为了简化定义，我们将中间语言公用的抽象语法定义在公共语法文件中。有program、node、stmt和sexp四个层次，分别表示程序、函数节点、语句和表达式。

其中program表示整个程序，由类型定义列表、常量定义列表、node列表和主节点id组成。程序执行会通过主node的id定位并执行主node。

node为Lustre的程序执行节点，相当于C程序的函数，由节点类型、输入参数、返回值、局部变量、语句列表五部分组成。

stmt为Lustre程序的语句，由普通赋值语句、函数调用语句、for循环语句、数组和结构体赋值语句和跟时序相关的语句，LustreE3、LustreE4层的语法与LustreF层的定义上相同，它们的stmt已消去了时态运算，具体定义如下：

stmt ：：= lh = sexp // 赋值语句。为方便，lh等同于 (id,)，下同。

| (oid, lhs) = call (calldef, sexp＊) // call 语句。

| Sfor (eqf, sexp, eqf, stmt) // 高阶执行语句。

| Sifs (sexp, stmt, stmt) // 条件语句

| Scase (sexp, sexp, (＜patn,sexp＞)＊) // case语句

| Sseq (stmt, stmt) // 序列语句。

| skip // 空语句。

sexp为Lustre程序的表达式，包括常量表达式、普通变量id、常量id、结构体变量id、输入变量id、数组子元素求值、结构体子元素求值、类型转化表达式、一元表达式和二元表达式。

4.2 语义环境

语义环境由全局和局部环境组成，对于node，由于要考虑时态特征，局部环境env的定义比普通串行语言的情形复杂很多：

Inductive env： Type ：= mkenv {

le： locenv;

sube： PTree.t (list env)

}.

其中，le和传统语言语义的局部环境类似，刻画了node在某个时钟周期的局部环境。locenv的定义：

Definition locenv：= PTree.t (mvl＊type).

sube维护了本节点实例与子节点实例中局部变量、输入和输出变量的历史取值。其中，类型PTree.t取 CompCert C中的定义，相当于一个（带索引的）容器类型的数据结构，方便增、删、改以及检索。

全局常量对应的环境gc定义为

gc： PTree.t (mvl＊type)或gc： locenv

我们用gc表示全局常量环境，当前局部环境中，用te表示普通变量环境，用se表示自定义变量环境，用ta表示输入变量环境，用eh表示本地局部环境变量列表。

翻译前的语义环境为：

gc, eh, te├ lvalue_list_norepet (lhs) // lhs中所有id互不相交

gc, eh, te├ assign_list_disjoint (lhs, args) // args的类型列表与fd定义中的参数类型列表相匹配

翻译后的语义环境为：

gc, ta, te, e├ lvalue_list_norepet (lhs) // lhs中所有id互不相交

gc, ta, te, e├ assign_list_disjoint (lhs, args) // args的类型列表与fd定义中的参数类型列表相匹配

翻译前后将原有的树形环境env简化为简单环境locenv。

5 地址不相交的保持性定义和证明

第3节描述的翻译过程中，每两层之间的翻译都要保证语义的等价性，其中高阶消去[6]、可信排序[11]和消去时态运算[12]的证明思想已在其他文章中介绍过，下面介绍左右值地址不相交的保持性定义和证明。

结构体和数组类型赋值运算要翻译为Clight中memcpy运算。在memcpy中需要满足以下对地址的限制：要么源地址和目的地址的指针不同；要么源地址和目的地址的偏移量相同；要么源地址范围和目的地址范围不相交。而Lustre的值中不存在指针，在证明这一步的证明之前也没有对Lustre赋值运算左右值的地址进行限制，所以需要定义Lustre中赋值的左右值地址不相交。而且在call运算的证明中也需要类似的定义，call运算中数组和结构体类型的输入参数会被翻译成指针，输出参数都会被翻译成指针。同样需要提供数组和结构体类型的输入参数和call的左值地址不相交；call的左值列表的地址不重复。

5.1 地址不相交的定义

在翻译过程中，我们要保证语句左值和等式右值的地址范围不相交，才能保证翻译的正确性，其中语句的左右值不相交包括三种情况：

（1）数组和结构体赋值语句的左右值地址不能相交

因为数组和结构体赋值不能直接通过赋值符号来赋值，需要借助memcpy来完成，而通过memcpy的赋值操作需要满足上述定义中的性质。

（2）Call运算左值不相交定义

Call运算会生成新的变量作为左值，我们要保证新生成的变量id和已有的左值列表地址互不相交。

（3）Call运算左值和输入参数地址不相交

Call运算新生成的变量id与原左值列表构成的新左值列表还必须与输入参数列表地址不相交。

LsemF中地址值不相交的定义：

（1）数组和结构体赋值中不相交的形式化定义

assign_disjoint te e a1 a2 ：=

|- (普通变量赋值语句：chunk, a2的值访问方式为值访问方式=＞a1与a2地址不相交)

/ (数组结构体赋值语句：id1 id2 o1 o2 k1 k2, a2的值访问方式为指针或memcpy，a1的类型k1为局部变量或结构体变量，(id1 ＜＞ id2 / Int.unsigned o1 + sizeof (typeof_s a1) ＜= Int.unsigned o2 /

Int.unsigned o2 + sizeof (typeof_s a2) ＜= Int. unsigned o1)%Z =＞

assign_disjoint te e a1 a2=＞l1与l2地址不相交）

其中te为普通变量环境，e为局部历史环境，a1、a2分别表示赋值语句的左值和右值，chunk表示数据块，id1为a1的左值id，o1为id1的起始地址，k1为a1的变量类型，id2为a2的左值id，o2为id2的起始地址，k2为a2的变量类型。当k1为局部变量或结构体变量时，若id1不等于id2，或o1+a1的长度＜o2，或o2+a2的长度＜o1，则在普通变量环境te和局部历史环境e下，a1和a2左值地址不相交。

（2）Call运算左值不相交的形式化定义

lval ue_disjoint te e a1 a2 ：=

eval_lvalue te e a1 id1 o1 k1 -＞

eval_lvalue te e a2 id2 o2 k2 -＞

k1 = Lid / k1 = Sid -＞

k2 = Lid / k2 = Sid -＞

(id1 ＜＞ id2 / Int.unsigned o1 + sizeof (typeof_ s a1) ＜= Int.unsigned o2 /

Int.unsigned o2 + sizeof (typeof_s a2) ＜= Int. unsigned o1)%Z -＞

lvalue_disjoint te e a1 a2.

其中te表示普通变量环境，e表示局部历史环境，a1、a2分别表示不同的call运算表达式，id1为a1的左值id，o1为id1的起始地址，k1为a1的变量类型，id2为a2的左值id，o2为id2的起始地址，k2为a2的变量类型，当k1、k2为局部变量或结构体变量时，若id1不等于id2，或o1+a1的长度＜o2，或o2+a2的长度＜o1，则在普通变量环境te和局部历史环境e下，a1和a2左值地址不相交。

其次，列表形式的形式化定义如下：

Definition lvalue_disjoints(te e： locenv)(a：sexp)(l： list sexp)： Prop ：=a1, In a1 l =＞ lvalue_ disjoint te e a a1.

（3）Call运算左值和输入参数不相交的形式化定义

Definition assign_list_disjoint(te e： locenv)(l1 l2： list sexp)： Prop ：=

a1 a2, In a1 l1 -＞ In a2 l2 -＞ assign_disjoint te e a1 a2.

对所有a1、a2，a1属于表l1，a2属于表l2，则在普通变量环境te和局部历史环境e下，a1、a2不相交。

5.2 左右值不相交的保持性证明

左右值不相交的保持性证明分为以下三种，主要是针对数组和结构体类型的左右值变量的地址范围不相交的性质的保持性证明。

（1）等式赋值左右值不相交的保持性定理

Lemma assign_disjoint_env_match：

assign_disjoint gc te eh a1 a2 -＞

env_match nd (mkenv eh se) e2 -＞

Z.max 1 (sizeof_struct (nd_fld (snd nd)) 0) ＜= Int.max_unsigned -＞

eval_sexp gc te eh a2 v -＞

locenv_getmvl gc te eh a1 v1 -＞

te ∃ OUTSTRUCT = None -＞

gc ∃ OUTSTRUCT = None -＞

assign_disjoint gc te e2 (trans_expr (makevar (snd nd)) a1) (trans_expr (makevar (snd nd)) a2).

其中，assign_disjoint表示等式左右值不相交，a1表示翻译前的左值，a2表示翻译前的右值。

对所有的全局常量环境gc、普通变量环境te、本地局部环境变量列表eh、自定义变量环境se、局部历史环境e2、等式左值a1等式右值a2、局部环境nd，变量v、v1，若满足①在gc、te、eh下a1、a2左右值不相交，②nd和eh与se构成的环境相匹配，③nd的结构体变量大小小于最大无符号数，④表达式a2在gc、te下执行结果为v，⑤在环境gc、te、eh下，a2执行结果为v，⑥在gc、te、eh下a1存储方式为v1，⑦在te下，存在输出结构体为空，⑧在gc下，存在输出结构体为空，则有在gc、te、e2下，a1和a2经表达式翻译后的id列表不相交。

通过证明表达式执行等价、表达式左值范围为静态、结构体中变量的域互不重叠便可得证。

（2）call左值列表不重复的保持性定理

Lemma lvalue_list_norepet_env_match：

lvalue_list_norepet gc te eh l -＞

env_match nd (mkenv eh se) e2 -＞

Z.max 1 (sizeof_struct (nd_fld (snd nd)) 0) ＜= Int.max_unsigned -＞

locenv_getmvls gc te eh l vl -＞

te ∃ OUTSTRUCT = None -＞

gc ∃ OUTSTRUCT = None -＞

lvalue_list_norepet gc te e2 (trans_exprs (makevar (snd nd)) l).

该定理表示若①对所有的全局常量环境gc、普通变量环境te、本地局部环境变量列表eh、表达式列表l，若满足左值列表不重复，②对所有的自定义变量se、局部历史环境e2、局部环境nd和变量vl，若满足nd和eh与se构成的环境匹配，③ nd的结构体变量大小小于最大无符号数，④在环境gc、te、eh下，1的存储方式为v1，⑤在te下，存在输出结构体为空，⑥在gc下，存在输出结构体为空，则有在gc、te、e2下，经表达式翻译后的l的左值列表不重复。

通过展开表达式转换的定义，证明左值不相交的保持性便可得证。

（3）call左值列表和右值表达式不相交的保持性定理

Lemma assign_list_disjoint_env_match：

assign_list_disjoint gc te eh l args -＞

env_match nd (mkenv eh se) e2 -＞

Z.max 1 (sizeof_struct (nd_fld (snd nd)) 0) ＜= Int.max_unsigned -＞

te ∃ OUTSTRUCT = None -＞

gc ∃ OUTSTRUCT = None -＞

eval_sexps gc te eh args vargs -＞

locenv_getmvls gc te eh l vl -＞

assign_list_disjoint gc te e2 (trans_exprs (makevar (snd nd)) l) (trans_exprs (makevar (snd nd)) args).

该定理表示若①对所有的全局常量环境gc、普通变量环境te、本地局部环境变量列表eh、表达式列表l，输入参数列表args，若满足在gc、te、eh下l与args列表地址不相交，②对所有的自定义变量se、局部历史环境e2、局部环境nd、输入参数列表args和变量vl，若满足nd和eh与se构成的环境匹配，③nd的结构体变量大小小于最大无符号数，④在te下，存在输出结构体为空，⑤在gc下，存在输出结构体为空， ⑥在环境gc、te、eh下，args的执行语义结果为vargs，⑦在环境gc、te、eh下，1的存储方式为v1，则有在gc、te、e2下，经表达式翻译后的l与经表达式翻译后的args的地址不重复。

该定理可先证明非列表的形式成立，并通过Coq中的list函数库的性质得证。

证明过程通过前提列表中的定义展开，并结合Coq的自动推理能力得以证明。证明了以上三个情况的地址不相交，即包含了Lustre到C转换中赋值语句变化部分的全部证明。

6 总结与展望

核电系统的开发流程必须满足NUREG/CR-6463 1996国际标准。Lustre编译器是广利核系统工程有限公司提供的满足NUREG/CR-6463 1996国际标准的，同时遵循IEC 60880-2006、MISRA-C：2004和ISO/ IEC 9899：1990编码规范的代码产生器。由于Lustre编译器本身满足这一标准并保证了代码的正确性，它不仅大大节省了编码工作，而且完全免去了代码的单元测试，很大程度地节省了验证工作和验证时间。

本文基于高阶逻辑定理证明器Coq，实现了Lustre到C的可信翻译及证明，并列举了左右值地址不相交性质的证明，本文所描述的Lustre编译器已经过大量的测试及验证确认工作，已经过验证并获得国际验证机构ISTec的认可，并获颁国内首张第三方验证与确认（IV&V）证书，且Lustre编译器已应用在核电系统神经中枢的某系统中。地址不相交保持性证明在编译器可信翻译中的应用为以后的相关转换工具的可信研发奠定了坚实的基础。

[1] 高玉娜. 基于SCADE的嵌入式软件开发方法研究[J]. 电子设计工程, 2015, 21： 103 - 105.

[2] 何炎祥, 吴伟, 刘陶, 等. 可信编译理论及其核心实现技术：研究综述[J]. 计算机科学与探索, 2011, 05( 1 ) ： 1 - 22.

[3] Berry G. Synchronous design and verification of critical embedded systems using SCADE and Esterel[C]. Formal methods for industrial critical systems, 2007： 2 - 2.

[4] Clarke E M, Wing J M. Formal methods： state of the art and future directions[J]. Acm Computing Surveys, 1996, 28 ( 4 )： 626 - 643.

[5] 韩俊刚, 杜慧敏. 数字硬件的形式化验证[M]. 北京：北京大学出版社, 2001, 12.

[6] Coqdevelopmentteam B. The coq proof assistant reference manual - version 8.0[C]. INRIA, INRIA Rocquencourt. 2010.

[7] 刘洋, 甘元科, 王生原, 等. 同步数据流语言高阶运算消去的可信翻译[J]. 软件学报, 2015, 26 ( 2 ) ： 332 - 347.

[8] Yang X, Chen Y, Eide E, et al. Finding and understanding bugs in C compilers.[J]. Acm Sigplan Notices, 2015, 46 ( 6 ) ：283 - 294.

[9] 张智慧, 齐敏, 冀建伟, 等. 核安全级控制算法描述语言的可信编译研究[C]. 2011.

[10] 石刚, 王生原, 董渊, 等. 同步数据流语言可信编译器的构造[J]. 软件学报, 2014, 25 ( 2 ) ： 341 - 356.

[11] 王蕾, 石刚, 董渊, 等. 一个C语言安全子集的可信编译器[J]. 计算机科学, 2013, 40 ( 9 ) ： 30 - 34.

[12] 甘元科, 张玲波, 石刚, 等. 同步数据流程序的可信排序[J]. 计算机应用与软件, 2014 ( 5 ) ： 1 - 5.

[13] 张玲波, 甘元科, 石刚, 等. 同步数据流语言时态消去的可信翻译[J]. 计算机工程与设计, 2014, 35 ( 1 ) ： 137 - 143.

Proof of the Preservation Property of Address Disjointness in Trustworthy Complier

Synchronous data-flow language is widely used in safety critical control system such as nuclear power systems. In the process of translation from synchronous data-flow language to order execution language, it is essential to guarantee the address disjointness between left and right values in assignment statement in semantic equivalence. In this paper, we formalized the property of address disjointness during the translation process, and verified the property via theorem proving. Compiler based on this method has been applied in safety protection system at some nuclear power plant.

Synchronous Data-Flow; Theorem Proving; Coq; Semantic Equivalence; Address Disjointness

谷伟卿（1987-），女，河北人，工程师，硕士，现就职于北京广利核系统工程有限公司，主要研究方向为编译系统，形式化验证。

张智慧（1982-），男，内蒙古人，工程师，硕士，现就职于北京广利核系统工程有限公司，主要研究方向为安全级算法组态软件、编译系统、基于语言的可信软件。

白 涛（1973-），男，河北人，高级工程师，硕士，现任北京广利核系统工程有限公司总工程师，主要研究方向为核电站数字化仪控。

齐 敏（1974-），女，河南人，工程师，硕士，现就职于北京广利核系统工程有限公司，主要研究方向为核电站反应堆保护系统安全级DCS平台设计和开发。