侯榮彬，馬 權(quán)，蘭 林，蔣 維，楊 斐，李 昂，李 丹

（中國(guó)核動(dòng)力研究設(shè)計(jì)院 核反應(yīng)堆系統(tǒng)設(shè)計(jì)技術(shù)重點(diǎn)實(shí)驗(yàn)室，成都 610213）

0 引言

在安全關(guān)鍵嵌入式實(shí)時(shí)系統(tǒng)中，軟件可靠性方面的問(wèn)題越來(lái)越突出。為了保證系統(tǒng)的安全，認(rèn)證機(jī)構(gòu)制定系統(tǒng)（系統(tǒng)認(rèn)證）和系統(tǒng)開(kāi)發(fā)工具（系統(tǒng)開(kāi)發(fā)工具認(rèn)證資質(zhì)）開(kāi)發(fā)的指導(dǎo)原則。為了降低系統(tǒng)在驗(yàn)證規(guī)范和設(shè)計(jì)方面的成本，開(kāi)發(fā)過(guò)程中通常使用自動(dòng)代碼生成器，以便從規(guī)范和設(shè)計(jì)模型自動(dòng)生成源代碼，然后從源代碼（傳統(tǒng)編譯器）中生成二進(jìn)制可執(zhí)行文件。另外，模型驅(qū)動(dòng)工程技術(shù)的發(fā)展也需要使用代碼生成器，實(shí)現(xiàn)從模型語(yǔ)言到通用編程語(yǔ)言的轉(zhuǎn)化。然而，許多有錯(cuò)誤的代碼生成器，特別是編譯器，它可以把一個(gè)正確的安全程序變成一個(gè)不正確的不安全的可執(zhí)行代碼。因此，應(yīng)該給予代碼生成器的V&V 以更多的關(guān)注。認(rèn)證機(jī)構(gòu)通常要求代碼生成器必須與它生成系統(tǒng)的部分有相同的安全級(jí)別。

編譯器要求在語(yǔ)義上是透明的：編譯后的代碼應(yīng)該按照源程序的語(yǔ)義所規(guī)定的方式運(yùn)行。然而，編譯器尤其是優(yōu)化編譯器是執(zhí)行復(fù)雜符號(hào)轉(zhuǎn)換的復(fù)雜程序。編譯器中錯(cuò)誤引發(fā)的事故，它們會(huì)悄悄地把正確的源程序變成不正確的可執(zhí)行程序。對(duì)于低可靠性要求的軟件，僅通過(guò)測(cè)試驗(yàn)證，編譯器引入的錯(cuò)誤的影響可以忽略不計(jì)。測(cè)試過(guò)程驗(yàn)證的是編譯器生成的可執(zhí)行代碼，經(jīng)過(guò)嚴(yán)格的測(cè)試可發(fā)現(xiàn)源程序的錯(cuò)誤。對(duì)于高可靠性要求軟件，這一問(wèn)題變得至關(guān)重要，需要使用形式化方法（模型檢查、程序驗(yàn)證等）來(lái)保證。使用形式化方法進(jìn)行驗(yàn)證幾乎都是在源代碼級(jí)別，編譯器中的漏洞會(huì)將這些經(jīng)過(guò)驗(yàn)證的源程序轉(zhuǎn)化為可執(zhí)行程序。如果編譯器中存在錯(cuò)誤，則可能使在源程序上的形式化驗(yàn)證失效。從形式化方法的角度看，編譯器是源程序與硬件處理器之間的一個(gè)薄弱環(huán)節(jié)，而后者已經(jīng)被形式化驗(yàn)證。安全關(guān)鍵軟件行業(yè)意識(shí)到了這個(gè)問(wèn)題，并使用了各種技術(shù)來(lái)緩解這個(gè)問(wèn)題，例如在關(guān)閉所有編譯器優(yōu)化之后對(duì)生成的匯編代碼進(jìn)行手動(dòng)代碼審查。然而，這些技術(shù)并不能完全解決這個(gè)問(wèn)題，并且在開(kāi)發(fā)時(shí)間和程序性能方面代價(jià)高昂。更好的方法是將形式化方法應(yīng)用于編譯器本身，以確保它保留源程序的語(yǔ)義。顯然，更好的方法是將形式化方法應(yīng)用于編譯器本身，以確保它保留源程序的語(yǔ)義。目前，已經(jīng)有很多方法和相關(guān)研究，包括書(shū)面、機(jī)器上的語(yǔ)義保持證明[1-3]、證明攜帶代碼[4-8]、可信編譯[9-11]、翻譯確認(rèn)[12-19]。

1 代碼生成器形式化驗(yàn)證方法

編譯器的形式化驗(yàn)證就是證明源程序S 和目標(biāo)程序C之間滿足給定的正確性屬性Prop(S, C)。正確性屬性包括：

I. S 和C 在可觀測(cè)行為上是等價(jià)的。

II. 如果S 有良好定義的語(yǔ)義（不出錯(cuò)），那么S 和C是可觀測(cè)行為等價(jià)的。

III. 如果S 有良好定義的語(yǔ)義并且滿足功能屬性Spec，那么C 滿足Spec。

IV. 如果S 是類型和內(nèi)存安全的，那C 也是。

V. C 是類型和內(nèi)存安全的。

對(duì)于可信代碼生成器的正確性屬性，選擇第2 種。理由如下：完全可觀測(cè)行為等價(jià)（性質(zhì)I）太強(qiáng)，它要求當(dāng)源代碼語(yǔ)義發(fā)生錯(cuò)誤時(shí)，編譯生成的目標(biāo)代碼也會(huì)出錯(cuò)。在實(shí)踐中，編譯器可以為具有未定義行為的源程序自由地生成任意代碼。因此，這個(gè)屬性很難證明。通常情況下，如果規(guī)范Spec 依賴于程序的可觀察行為，則規(guī)范的保持性（屬性III）由屬性II 蘊(yùn)含。因此，一勞永逸地證明屬性II，可滿足很多屬性III 中的規(guī)范。屬性IV 是典型的類型保持編譯器，只是屬性III 的一個(gè)實(shí)例。最后，屬性V 是一個(gè)與源程序無(wú)關(guān)的屬性，這是一種典型的編譯器，要么直接在編譯器代碼上建立感興趣的屬性（類型安全），要么在源程序上建立感興趣的屬性，并在編譯過(guò)程中保存這一屬性。

一個(gè)編譯器Comp 是一個(gè)從源程序到編譯生成的代碼（記作Comp(S) = Some(C)）或錯(cuò)誤（記作：Comp(S) = None）的全函數(shù)。錯(cuò)誤的情況必須考慮，因?yàn)榫幾g器可能生成代碼失敗。例如，源程序有語(yǔ)法或類型錯(cuò)誤、編譯的程序超出了編譯器的能力。

1）經(jīng)過(guò)驗(yàn)證的編譯器

使用上面的定義，一個(gè)經(jīng)過(guò)驗(yàn)證的編譯器是任何完成下面定理的形式化證明的編譯器Comp：

換句話說(shuō)，要么編譯器報(bào)告錯(cuò)誤，要么生成滿足所需正確性的屬性的代碼。注意，當(dāng)Comp(S) = None 時(shí)，這一規(guī)則也同樣成立。編譯器是否成功地編譯感興趣的源程序不是一個(gè)正確性問(wèn)題，而是一個(gè)編譯器實(shí)現(xiàn)質(zhì)量問(wèn)題，這是由諸如測(cè)試之類非形式化方法解決的。從形式化方法的觀點(diǎn)來(lái)看，重點(diǎn)是編譯器從不默默地產(chǎn)生錯(cuò)誤的代碼。

2）攜帶證明的代碼

攜帶證明代碼和可信編譯使用驗(yàn)證編譯器，它可以生成代碼失敗（CComp(S) = None）或返回一個(gè)編譯產(chǎn)生的C代碼和屬性Prop(S, C)的證明π(CComp(S) = Some(C,π))。證明π可以被使用者獨(dú)立檢查。這種方法沒(méi)有必要相信代碼產(chǎn)生者，也不需要驗(yàn)證代碼生成器本身。驗(yàn)證編譯器可以產(chǎn)生正確的證明π，而不是建立Prop(S, C)。

3）翻譯確認(rèn)

在翻譯確認(rèn)方法中，標(biāo)準(zhǔn)的編譯器Comp 還輔助于一個(gè)驗(yàn)證器：一個(gè)布爾值函數(shù)Verif(S, C)通過(guò)靜態(tài)分析S 和C來(lái)驗(yàn)證屬性Prop(S, C)。為獲得形式化保證，驗(yàn)證器自身必須被驗(yàn)證，也就是必須證明：

然而，這種方法不需要對(duì)編譯器本身進(jìn)行形式化驗(yàn)證。因此，不能保證編譯器產(chǎn)生的代碼總是能夠通過(guò)驗(yàn)證器。

4）混合方法：結(jié)合經(jīng)過(guò)驗(yàn)證的編譯器和驗(yàn)證編譯器

通過(guò)重新組合，可以形式化地結(jié)合經(jīng)過(guò)驗(yàn)證的編譯器方法和驗(yàn)證編譯器。如果CComp 是一個(gè)驗(yàn)證編譯器并且Verif 是一個(gè)正確的驗(yàn)證器，那么下面的函數(shù)是一個(gè)經(jīng)過(guò)驗(yàn)證的編譯器。定理（1）可以直接從定理（2）獲得。

Comp(S) =

match CComp(S) with

|None ->None

|Some(C, A) -> if Verif(S, C, A) then Some(C)

else None

類似地，設(shè)Comp 是一個(gè)經(jīng)過(guò)驗(yàn)證的編譯器并且Π 是一個(gè)定理（1）的Coq 證明項(xiàng)。根據(jù)Curry-Howard 同構(gòu)機(jī)制，Π 是一個(gè)函數(shù)包括S，C 和一個(gè)Comp(S) = Some (C)的證明，并且返回一個(gè)Prop(S, C)的證明。一個(gè)驗(yàn)證編譯器定義如下：

CComp(S) =

match Comp(S) with

| None -> None

|Some(C) -> Some(C, Π S Cπeq)

其中，πeq 是命題Comp(S) = Some(C)的證明項(xiàng)。伴隨的驗(yàn)證器是Coq 證明檢查器，就像是攜帶證明代碼方法一樣。

5）編譯過(guò)程的組合性

編譯器通常由很多階段組成，這些階段之間通過(guò)中間語(yǔ)言進(jìn)行連接。上面提到的兩種編譯器構(gòu)造方法，經(jīng)過(guò)驗(yàn)證的編譯器和驗(yàn)證編譯器都可以通過(guò)這種方式進(jìn)行分解。如 果Comp1 和Comp2 分 別 是 從L1 到L2 和L2 到L3 的 經(jīng)過(guò)驗(yàn)證的編譯器，他們的組合：

Comp(S) =

match Comp1(S) with

| None -> None

| Some(I) -> Comp2(I)

假設(shè)屬性Prop 是可傳遞性的，那么Comp 是一個(gè)從L1到L3 的經(jīng)過(guò)驗(yàn)證的編譯器。也就是Prop(S, I)和Prop(I, C)蘊(yùn)含Prop(S, C)。

相似地，如果CComp1 和CComp2 分別是L1 到L2 和L2 到L3 的驗(yàn)證編譯器，Verif1 和Verif2 是伴隨的驗(yàn)證器，那么一個(gè)從L1 到L3 的驗(yàn)證編譯器為：

CComp(S) =

match CComp1(S) with

|None ->None

|Some(I, A1) ->

match CComp2(I) with

|None->None

|Some(C, A2)->Some(C, (A1 ,I, A2))

Verif(S, C, (A1, I, A2)) = Verif1(S, I, A1)/Verif2(I, C, A2)

2 代碼生成器正確性定義

編譯階段的語(yǔ)義正確性是根據(jù)形式化源語(yǔ)言和目標(biāo)語(yǔ)言的模擬關(guān)系來(lái)定義。上面已經(jīng)介紹了4 種正確性屬性，其中最重要的是編譯過(guò)程的語(yǔ)義保持性（屬性II），這種屬性由向前模擬關(guān)系來(lái)實(shí)現(xiàn)。編譯器正確性的核心是確定計(jì)算與編譯交互的精確定義。對(duì)于一個(gè)編譯階段的源語(yǔ)言Src和目標(biāo)語(yǔ)言Tgt，可以通過(guò)向前模擬關(guān)系實(shí)現(xiàn)編譯器正確性的定義，如圖1 所示。

其中：

1）編譯過(guò)程Src →Tgt 沿水平方向演變，從左到右。

2）程序執(zhí)行過(guò)程垂直方向，從上到下。

3）兩種語(yǔ)言的狀態(tài)分別為σ_Src 和σ_Tgt。其中，σ_Src = (c1, m1)，σ_Tgt=(c2, m2)。c1 和c2 分別是源語(yǔ)言和目標(biāo)語(yǔ)言的語(yǔ)句，并且這兩種語(yǔ)言具有獨(dú)立的內(nèi)存。

4）過(guò)程→是程序的執(zhí)行方向，根據(jù)編程語(yǔ)言的小步語(yǔ)義關(guān)系σ→σ'或多步語(yǔ)義σ→nσ'確定。

5）水平關(guān)系采用二元匹配關(guān)系的形式，它將源語(yǔ)言狀態(tài)與目標(biāo)語(yǔ)言狀態(tài)相關(guān)聯(lián)，并且在執(zhí)行過(guò)程中保持這一關(guān)系。

圖1 向前模擬關(guān)系示意圖Fig.1 Diagram of forward simulation relationship

圖2 模擬關(guān)系傳遞組合性示意圖Fig.2 Schematic diagram of simulation relationship transfer combination

為了更清楚地表示程序運(yùn)行的各種情況，匹配關(guān)系(c1,m1)→(c2,m2)蘊(yùn)含如下命題：

a）如果c1, m1 →Src c1'，m1'，那么存在c2' 和m2' 使得c2, m2 →Tgtn c2', m2'，并且(c1', m1')→(c2', m2')。

b）如果c1 終止，那么c2 終止，并且返回值和內(nèi)存都滿足匹配關(guān)系。

c）如果是函數(shù)調(diào)用語(yǔ)句c1 = (f, a1 →) , c2 = (f, a2 →)，要求執(zhí)行前參數(shù)列表a1 →~ a2 →，并且m1~m2，執(zhí)行完畢后返回值和更新后內(nèi)存滿足匹配關(guān)系。

對(duì)于真實(shí)的編譯器，編譯器的正確性證明必須沿著編譯過(guò)程的各個(gè)階段可傳遞性的組合。通過(guò)這種方式每個(gè)階段可以相互獨(dú)立地進(jìn)行證明，然后將這些證明串聯(lián)起來(lái)。這明顯比單塊地證明編譯器是正確的更加模塊化，并且簡(jiǎn)化了證明難度。

沿著編譯過(guò)程的模擬關(guān)系的可傳遞組合性可以通過(guò)圖2 進(jìn)行表示。

3 編程語(yǔ)言語(yǔ)法

圖3 Lustre 和C語(yǔ)言抽象語(yǔ)法Fig.3 Lustre and C language abstract syntax

Lustre 是一種廣泛應(yīng)用于嵌入式控制和信號(hào)處理系統(tǒng)的面向應(yīng)用的編程語(yǔ)言。著名的SCADE[20]和Simulink[21]都是基于Lustre，將Lustre 轉(zhuǎn)換為可執(zhí)行代碼。SCADE 廣泛應(yīng)用于航空控制和反應(yīng)堆監(jiān)視軟件開(kāi)發(fā)中。Lustre 的主要特征包括：易于構(gòu)建反應(yīng)式控制；程序的執(zhí)行有靜態(tài)有界的空間和時(shí)間；具有基于數(shù)據(jù)流的良好數(shù)學(xué)語(yǔ)義；可追溯和模塊編譯框架；可實(shí)現(xiàn)自動(dòng)化程序驗(yàn)證。Lustre 的抽象語(yǔ)法如圖3 所示，這些抽象語(yǔ)法都是通過(guò)遞歸定義的。在表達(dá)式層，可分為一般表達(dá)式，如變量、常量、一元操作表達(dá)式、二元操作表達(dá)式、時(shí)鐘運(yùn)算表達(dá)式等；控制表達(dá)式，如條件表達(dá)式；時(shí)鐘表達(dá)式，如基本時(shí)鐘、子時(shí)鐘。在語(yǔ)句層，Lustre 只有等式語(yǔ)句，等式的類型包括一般賦值、延時(shí)賦值、函數(shù)調(diào)用。一個(gè)完整的Lustre 程序是類型聲明、函數(shù)聲明和主函數(shù)調(diào)用的集合。對(duì)于C 語(yǔ)言，大家都比較熟悉，其抽象語(yǔ)法如右半部分所示，其結(jié)構(gòu)和Lustre 很類似，不再贅述。

4 Lustre和C語(yǔ)義一致性的定義

如圖4 所示，Lustre 語(yǔ)言到C 語(yǔ)言的翻譯過(guò)程的語(yǔ)義保持性，實(shí)際上就是在相同的初始狀態(tài)下，接受相同的輸入，分別執(zhí)行各自程序的語(yǔ)義，程序執(zhí)行完畢后，最終的狀態(tài)滿足匹配關(guān)系，并且在最終狀態(tài)中查找到相同的程序輸出值。源語(yǔ)言Luster 和目標(biāo)語(yǔ)言C 之間通過(guò)一個(gè)轉(zhuǎn)換函數(shù)Comp 建立聯(lián)系。只要完成Lustre 語(yǔ)言到C 語(yǔ)言的語(yǔ)義保持性證明，也就間接證明源語(yǔ)言Lustre 和經(jīng)過(guò)Comp 處理生成的C 之間滿足語(yǔ)義保持性。語(yǔ)義保持性證明基于編程語(yǔ)言的操作語(yǔ)義和狀態(tài)的匹配關(guān)系以及程序和環(huán)境的交互。操作語(yǔ)義是一種基于狀態(tài)轉(zhuǎn)換關(guān)系的推理規(guī)則，匹配關(guān)系表示兩個(gè)環(huán)境中標(biāo)識(shí)符和值之間的對(duì)應(yīng)和相等關(guān)系。程序和環(huán)境的交互關(guān)系較為復(fù)雜如圖5 所示。根據(jù)程序的語(yǔ)法結(jié)構(gòu)，程序執(zhí)行語(yǔ)義分為類型和函數(shù)聲明語(yǔ)句與主函數(shù)的調(diào)用，主函數(shù)的調(diào)用是函數(shù)調(diào)用的一個(gè)實(shí)例，函數(shù)調(diào)用又分為局部變量聲明和語(yǔ)句執(zhí)行，語(yǔ)句的執(zhí)行實(shí)際就是控制表達(dá)式的求值。其中，聲明類語(yǔ)句，如類型、函數(shù)聲明語(yǔ)句和變量聲明語(yǔ)句會(huì)創(chuàng)建新的環(huán)境和標(biāo)識(shí)符，申請(qǐng)新的內(nèi)存塊?？刂祁愓Z(yǔ)句如函數(shù)調(diào)用、語(yǔ)句執(zhí)行、表達(dá)式求值則會(huì)更新?tīng)顟B(tài)，改變標(biāo)識(shí)符對(duì)應(yīng)的值或內(nèi)存空間。求值類語(yǔ)句，則會(huì)根據(jù)當(dāng)前的狀態(tài)來(lái)確定自身的值。

圖4 程序執(zhí)行一致性的定義Fig.4 Definition of program execution consistency

圖5 程序和環(huán)境的交互關(guān)系Fig.5 Interaction between program and environment

5 結(jié)束語(yǔ)

本文針對(duì)一種Lustre 到C 的代碼生成器，準(zhǔn)備采用形式化方法對(duì)其翻譯過(guò)程的語(yǔ)義保持性進(jìn)行證明。第一部分介紹了應(yīng)用形式化驗(yàn)證技術(shù)構(gòu)建代碼生成器的方法，包括經(jīng)過(guò)驗(yàn)證的編譯器、驗(yàn)證編譯器、翻譯確認(rèn)、混合方法，以及將翻譯階段分解組合的技術(shù)；第二部分介紹了語(yǔ)義保持性定義的方法即單向模擬理論；第三部分介紹了源語(yǔ)言Lustre 和目標(biāo)語(yǔ)言C 的抽象語(yǔ)法；第四部分定義了Lustre到C 翻譯過(guò)程的語(yǔ)義保持性，將前面的理論應(yīng)用于實(shí)際翻譯過(guò)程的定義中，并詳細(xì)介紹了程序和語(yǔ)言狀態(tài)之間的交互。這是程序操作語(yǔ)義的基礎(chǔ)，而操作語(yǔ)義又是語(yǔ)義保持性證明的基礎(chǔ)。本論文為后續(xù)實(shí)際代碼生成器的開(kāi)發(fā)提供理論指導(dǎo)，也是后續(xù)代碼生成器形式化語(yǔ)義保持性定義的依據(jù)。