可信編譯器中地址不相交的保持性證明

★北京廣利核系統工程有限公司 谷偉卿，張智慧，白濤，齊敏

可信編譯器中地址不相交的保持性證明

★北京廣利核系統工程有限公司 谷偉卿，張智慧，白濤，齊敏

同步數據流語言是一種廣泛應用于核電及其他安全關鍵領域的語言，在同步數據流語言到順序執行語言的翻譯轉換過程中，語義等價要保證賦值語句的左右值地址互不相交，這至關重要。本文使用形式化方法描述了翻譯過程中地址互不相交的性質，并通過定理證明的方式對其進行了驗證。基于本方法的編譯器在某核電站的安全保護系統中得到了應用。

同步數據流；定理證明；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平臺設計和開發。