代碼生成器形式化驗證技術研究

侯榮彬，馬 權，蘭 林，蔣 維，楊 斐，李 昂，李 丹

（中國核動力研究設計院 核反應堆系統設計技術重點實驗室，成都 610213）

0 引言

在安全關鍵嵌入式實時系統中，軟件可靠性方面的問題越來越突出。為了保證系統的安全，認證機構制定系統（系統認證）和系統開發工具（系統開發工具認證資質）開發的指導原則。為了降低系統在驗證規范和設計方面的成本，開發過程中通常使用自動代碼生成器，以便從規范和設計模型自動生成源代碼，然后從源代碼（傳統編譯器）中生成二進制可執行文件。另外，模型驅動工程技術的發展也需要使用代碼生成器，實現從模型語言到通用編程語言的轉化。然而，許多有錯誤的代碼生成器，特別是編譯器，它可以把一個正確的安全程序變成一個不正確的不安全的可執行代碼。因此，應該給予代碼生成器的V&V 以更多的關注。認證機構通常要求代碼生成器必須與它生成系統的部分有相同的安全級別。

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

1 代碼生成器形式化驗證方法

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

I. S 和C 在可觀測行為上是等價的。

II. 如果S 有良好定義的語義（不出錯），那么S 和C是可觀測行為等價的。

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

IV. 如果S 是類型和內存安全的，那C 也是。

V. C 是類型和內存安全的。

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

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

1）經過驗證的編譯器

使用上面的定義，一個經過驗證的編譯器是任何完成下面定理的形式化證明的編譯器Comp：

換句話說，要么編譯器報告錯誤，要么生成滿足所需正確性的屬性的代碼。注意，當Comp(S) = None 時，這一規則也同樣成立。編譯器是否成功地編譯感興趣的源程序不是一個正確性問題，而是一個編譯器實現質量問題，這是由諸如測試之類非形式化方法解決的。從形式化方法的觀點來看，重點是編譯器從不默默地產生錯誤的代碼。

2）攜帶證明的代碼

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

3）翻譯確認

在翻譯確認方法中，標準的編譯器Comp 還輔助于一個驗證器：一個布爾值函數Verif(S, C)通過靜態分析S 和C來驗證屬性Prop(S, C)。為獲得形式化保證，驗證器自身必須被驗證，也就是必須證明：

然而，這種方法不需要對編譯器本身進行形式化驗證。因此，不能保證編譯器產生的代碼總是能夠通過驗證器。

4）混合方法：結合經過驗證的編譯器和驗證編譯器

通過重新組合，可以形式化地結合經過驗證的編譯器方法和驗證編譯器。如果CComp 是一個驗證編譯器并且Verif 是一個正確的驗證器，那么下面的函數是一個經過驗證的編譯器。定理（1）可以直接從定理（2）獲得。

Comp(S) =

match CComp(S) with

|None ->None

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

else None

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

CComp(S) =

match Comp(S) with

| None -> None

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

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

5）編譯過程的組合性

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

Comp(S) =

match Comp1(S) with

| None -> None

| Some(I) -> Comp2(I)

假設屬性Prop 是可傳遞性的，那么Comp 是一個從L1到L3 的經過驗證的編譯器。也就是Prop(S, I)和Prop(I, C)蘊含Prop(S, C)。

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

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 代碼生成器正確性定義

編譯階段的語義正確性是根據形式化源語言和目標語言的模擬關系來定義。上面已經介紹了4 種正確性屬性，其中最重要的是編譯過程的語義保持性（屬性II），這種屬性由向前模擬關系來實現。編譯器正確性的核心是確定計算與編譯交互的精確定義。對于一個編譯階段的源語言Src和目標語言Tgt，可以通過向前模擬關系實現編譯器正確性的定義，如圖1 所示。

其中：

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

2）程序執行過程垂直方向，從上到下。

3）兩種語言的狀態分別為σ_Src 和σ_Tgt。其中，σ_Src = (c1, m1)，σ_Tgt=(c2, m2)。c1 和c2 分別是源語言和目標語言的語句，并且這兩種語言具有獨立的內存。

4）過程→是程序的執行方向，根據編程語言的小步語義關系σ→σ'或多步語義σ→nσ'確定。

5）水平關系采用二元匹配關系的形式，它將源語言狀態與目標語言狀態相關聯，并且在執行過程中保持這一關系。

圖1 向前模擬關系示意圖Fig.1 Diagram of forward simulation relationship

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

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

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

b）如果c1 終止，那么c2 終止，并且返回值和內存都滿足匹配關系。

c）如果是函數調用語句c1 = (f, a1 →) , c2 = (f, a2 →)，要求執行前參數列表a1 →~ a2 →，并且m1~m2，執行完畢后返回值和更新后內存滿足匹配關系。

對于真實的編譯器，編譯器的正確性證明必須沿著編譯過程的各個階段可傳遞性的組合。通過這種方式每個階段可以相互獨立地進行證明，然后將這些證明串聯起來。這明顯比單塊地證明編譯器是正確的更加模塊化，并且簡化了證明難度。

沿著編譯過程的模擬關系的可傳遞組合性可以通過圖2 進行表示。

3 編程語言語法

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

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

4 Lustre和C語義一致性的定義

如圖4 所示，Lustre 語言到C 語言的翻譯過程的語義保持性，實際上就是在相同的初始狀態下，接受相同的輸入，分別執行各自程序的語義，程序執行完畢后，最終的狀態滿足匹配關系，并且在最終狀態中查找到相同的程序輸出值。源語言Luster 和目標語言C 之間通過一個轉換函數Comp 建立聯系。只要完成Lustre 語言到C 語言的語義保持性證明，也就間接證明源語言Lustre 和經過Comp 處理生成的C 之間滿足語義保持性。語義保持性證明基于編程語言的操作語義和狀態的匹配關系以及程序和環境的交互。操作語義是一種基于狀態轉換關系的推理規則，匹配關系表示兩個環境中標識符和值之間的對應和相等關系。程序和環境的交互關系較為復雜如圖5 所示。根據程序的語法結構，程序執行語義分為類型和函數聲明語句與主函數的調用，主函數的調用是函數調用的一個實例，函數調用又分為局部變量聲明和語句執行，語句的執行實際就是控制表達式的求值。其中，聲明類語句，如類型、函數聲明語句和變量聲明語句會創建新的環境和標識符，申請新的內存塊。控制類語句如函數調用、語句執行、表達式求值則會更新狀態，改變標識符對應的值或內存空間。求值類語句，則會根據當前的狀態來確定自身的值。

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

圖5 程序和環境的交互關系Fig.5 Interaction between program and environment

5 結束語

本文針對一種Lustre 到C 的代碼生成器，準備采用形式化方法對其翻譯過程的語義保持性進行證明。第一部分介紹了應用形式化驗證技術構建代碼生成器的方法，包括經過驗證的編譯器、驗證編譯器、翻譯確認、混合方法，以及將翻譯階段分解組合的技術；第二部分介紹了語義保持性定義的方法即單向模擬理論；第三部分介紹了源語言Lustre 和目標語言C 的抽象語法；第四部分定義了Lustre到C 翻譯過程的語義保持性，將前面的理論應用于實際翻譯過程的定義中，并詳細介紹了程序和語言狀態之間的交互。這是程序操作語義的基礎，而操作語義又是語義保持性證明的基礎。本論文為后續實際代碼生成器的開發提供理論指導，也是后續代碼生成器形式化語義保持性定義的依據。