形式化驗證技術在核電廠DCS中的應用研究

侯榮彬，馬 權，蘭 林，李 勇，楊 斐，薛 凱，吳亞波

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

0 引言

目前保證軟件可靠性的方法主要有兩類：①傳統方法：測試和軟件過程管理；②形式化方法：主要包括定理證明、模型檢測、翻譯確認等。傳統測試方法，實施過程較為簡單，但測試用例數量龐大，并且測試只能發現軟件錯誤，不能證明其沒有錯誤。采用形式化方法是提高軟件可靠性的有效途徑，隨著形式化驗證技術的成熟，人們逐漸意識到形式化方法的發展潛力。在一些安全攸關領域的軟件開發標準中也逐步新增了與形式化方法相關的要求和建議，如安全評估標準[1]、DO-178C[2]、ISO26262-6[3]推薦在系統軟件開發中運用形式化方法。在核領域IAEA 的核能系列《核電廠儀控系統安全級軟件可靠性評估》[4]將形式化方法作為重要的評估證據來源。近年來隨著形式化技術的普及和開發工具的進步，已經達到了實用化水平，因此在未來新的工業標準中極有可能引入形式化方法的要求。對此有必要在核電廠安全軟件中引入形式化方法，一方面提高開發可靠性；另一方面滿足未來需求。基于對形式化方法的理論研究和核安全級DCS 系統的實際需求，本文主要討論形式化技術在核電廠儀控工程應用軟件、代碼生成器、操作系統的應用。

1 核電廠儀控工程應用軟件的正確性驗證

1.1 模型檢測

模型檢測：通過搜索待驗證軟件系統模型的有窮狀態空間來檢查系統的行為是否具備預定屬性的一種自動驗證技術。模型檢測方法最初由E.M.Clark 等人于1981 年提出，他們設計了檢驗有窮狀態并發系統是否滿足給定分支時序邏輯公式的算法。模型檢測方法大致可以分為以下3 個基本步驟：建模——將實際的系統轉換為模型檢測工具所能夠接受的形式；規約——采用邏輯公式描述系統的屬性；驗證——基于狀態空間搜索的方法對系統進行形式驗證。該方法的優點為驗證過程自動化，缺點為因其基礎狀態空間搜索，會引起狀態空間爆炸。

比較著名的模型檢測工具包括：針對C 語言的模型檢測器CBMC[5]、基于時間自動機的UPPAAL[6]、用于驗證線性時序邏輯的SPIN 和開源模型檢測工具NuSMV。

1.2 程序驗證

程序驗證是使用邏輯推理的方法來證明程序滿足其規范所描述的性質。可以通過對程序進行歸納證明避免狀態搜索，進而避免狀態空間爆炸。程序規范是某種邏輯表達式構成的斷言，用于描述程序應滿足的性質。根據程序的語義可以建立一套特定的推理規則用于程序驗證。如果能得到程序的一個證明，則表示程序滿足程序規范。形式化程序驗證研究始于Hoare 等提出的霍爾邏輯理論。經典霍爾三元組：{P}C{Q}是一個數理邏輯斷言。把狀態斷言對（P，Q）看作描述程序行為的規范，那么證明霍爾三元組為真的數理邏輯證明也就是對應程序滿足其規范的證明。為了表述復雜數據類型和指針，在霍爾邏輯的基礎上建立了離散邏輯，但其基本思想相同，只不過引入離散算術以適應高級語言特性。常見的程序驗證工具包括Smallfoot[7]、Boogie[8]等。

核電廠儀控工程應用軟件屬于安全級軟件，主要實現反應堆監測、控制、保護功能邏輯。其開發過程如圖1 所示，包括：需求分析階段、設計階段、實現階段、測試階段。其中，需求分析階段主要對軟件的需求進行描述，包括非形式化描述和形式化描述；設計階段將需求定義轉化為功能塊圖的形式；實現階段將功能塊圖轉化為C 代碼，再經過編譯器編譯為嵌入式設備中可運行的二進制文件；最后，在硬件設備上對程序進行測試，或對功能塊圖進行仿真測試。核電廠儀控工程應用軟件控制邏輯相對簡單，很適合使用形式化方法進行驗證。如圖1 所示，可考慮將模型檢測方法應用于需求階段的形式化需求模型和設計階段的功能圖塊，在開發早期對模型進行驗證，盡早發現問題。這一過程可以替代測試階段對功能塊圖的測試，另一方面也可以考慮對實現階段的C 代碼進行程序驗證，以替代C 代碼的測試。

圖1 模型檢查和程序驗證在核電廠儀控工程應用軟件開發過程中的應用Fig.1 Application of model check and program verification in the development process of application software for nuclear power plant instrumentation and control engineering

圖2 代碼生成器和編譯器關系示意圖Fig.2 Schematic diagram of the relationship between code generator and compiler

2 可信編譯器的開發

通常可信編譯程序分為兩種，一種是實現兩種高級語言之間的轉化程序，通常稱為代碼生成器。另一種是實現高級語言到機器語言的翻譯稱為編譯器。二者關系如圖2所示。

圖3 可信編譯技術在核電廠儀控工程應用軟件開發過程中的應用Fig.3 Application of trusted compilation technology in the development process of nuclear power plant instrumentation and control engineering application software

采用形式化方法構造可信編譯器或代碼生成器的方法主要有以下3 種：①攜帶證明的編譯器：不但能夠編譯器生成目標代碼，另外還生成與之對應的證明，通過一個額外的驗證器來檢查證明目標代碼是否滿足給定的性質。提出攜帶證明代碼的概念最先由Necula 等提出[9]，并為一個類型安全的C 語言子集實現了一個攜帶證明的編譯器[10]。Colby 等人采用同樣的方法實現對java 語言的字節碼編譯到目標代碼的攜帶證明編譯器[11]；②翻譯確認：翻譯確認的方法不是對編譯本身進行驗證，而是自動驗證源代碼和目標代碼滿足相同的規范，主要做法是用同一語義框架為翻譯過程的源代碼和目標代碼建模，通過實現一個額外的驗證器來自動驗證源程序和目標程序滿足相同的規范。翻譯確認方法可用于完整編譯器的構建，也可用于編譯器的優化。Pnueli[12,13]等最早提出了翻譯確認的概念并用于實現同步數據流語言Signal 到C 的編譯器的翻譯確認。Ngo和Talpin[14-19]等采用翻譯確認方法，針對同步數據流語言Signal 到C 的編譯器，為源代碼和目標代碼建立了一套統一的語義框架；定義了一種源和目標之間的抽象時鐘等價關系；通過對等價關系進行驗證來保證編譯器時鐘語義的一致性。翻譯確認方法的優點在于不依賴于翻譯的具體過程，相比對翻譯過程進行驗證的方法更輕便和靈活并具有較高的自動化水平，更適合用于編譯器的局部優化；③定理證明：該方法是對翻譯過程進行證明，也是最為直接徹底的方法。該方法需要嚴格定義源語言和目標語言的操作語義，并基于一種單向模擬原理定義源語言和目標語言的語義一致性。根據操作語義進行推理證明源語言和目標語言的語義一致性，這一過程可以通過定理輔助證明工具來實現。使用定理證明方法開發的編譯器的成功案例為Compcert[20]和Velus[21]。國內王生原團隊用此方法開發一個針對一種同步數據流語言到C 的代碼生成工具[22,23]。

上節介紹了核電廠儀控系統應用軟件的開發流程，在需求、設計和實現階段分別對應著一種模型描述語言，需求階段對應形式化需求定義語言、設計階段對應功能圖塊語言、實現階段對應C 語言和機器語言。在實際開發過程中，可以使用代碼生成工具實現上述語言的自動轉化。通常代碼生成工具不僅需要完成語言的轉換，還要求保證轉換前后語義具有一致性，使用可信編譯技術開發的代碼生成工具恰好具備上述性質。如圖2 所示，可考慮可信編譯技術在需求定義語言到功能圖塊和功能圖塊到C 語言的轉換過程的應用，至于C 到二進制文件的編譯可使用著名的Compcert，這樣一來就構成一套完整的可信編譯工具鏈，另外代碼生成技術還可應用于測試用例的自動生成。

圖4 操作系統的微內核架構Fig.4 The microkernel architecture of the operating system

3 操作系統驗證

操作系統的安全性對信息安全和嵌入式系統功能安全至關重要。操作系統作為基礎軟件，因其復雜性，往往存在系統漏洞，因此無法提供安全服務和安全保障。造成這些文題的主要原因包括兩個方面：①操作系統的頂層設計和代碼實現不一致；②操作系統功能定義與實際安全目標不一致。通過采用形式化的方法對操作系統進行設計和驗證可有效提高設計和實現的一致性，保證操作系統的安全目標。

國內相關機構開展了有關操作系統形式化驗證的研究工作。陳超超[24]等對L4 內核操作系統的內存管理機制進行了形式化驗證。錢振江等[25-27]提出了操作系統對象語義模型（OSOSM），驗證了操作系統的安全屬性和微內核架構的中斷機制的正確性。程亮[28]針對SELinux 的安全策略，使用模型檢測方法驗證策略實現與安全需求之間的一致性。張忠秋等[29]應用霍爾邏輯，以定理證明的方式完成機載嵌入式操作系統軟件的形式化驗證。

圖5 操作系統的形式化設計和驗證框架Fig.5 Formal design and verification framework of operating system

目前，核電廠儀控系統的操作系統一般是使用自主研發微內核的操作系統，任務順序執行無中斷，要求具有確定性，相較于傳統的操作系統有所簡化。操作系統的微內核架構如圖4 所示，包括硬件層，運行在特權模式下的微內核與運行在用戶模式下的應用程序、驅動程序、文件系統等。微內核的優點在于驅動程序和文件系統等從操作系統中剝離出來，運行在自己單獨的內存區域中，因此驅動程序和文件系統的錯誤只會涉及到自身的區域，不會對整個系統造成大的危害。操作系統是一個很復雜的軟件，因此難免出現需求與設計、設計與實現的不一致問題。圖5給出了操作系統的形式化設計和驗證的框架。主要包括三層：分別是需求概念層、形式化描述層、代碼實現層。需求概念層包括操作系統的設計描述和功能需求，涉及操作系統的工作原理、安全屬性、策略等。形式化描述層主要實現操作系統的形式化建模和規范的形式化定義（規范說明和系統安全屬性），這一過程需要對操作系統形式化模型是否滿足操作系統的規范說明和安全屬性進行驗證。最后，驗證操作系統的代碼實現與操作系統形式化模型是否一致。

4 開發工具-高階邏輯和證明助手

高階定理證明器也稱為證明助手。使用證明助手進行證明的過程類似在紙面上進行證明的過程，證明者需要定義相關的引理，并可以借助于證明策略提高證明的效率，每個命題的證明通常采用從后向前推理證明方法。復雜的證明目標可通過分解成子目標，子目標再分解成更小的目標，直到公理級別和已知前提，最后完成證明。如果一個子目標不容易被直接證明，則可引入一條輔助引理，單獨進行證明。證明策略用于對子目標進行組織、分解及證明。證明助手不僅提供基本的證明策略，還提供證明策略的構造方法即泛策略，用戶可以通過構造新的證明策略加速證明過程，也可以通過定義復雜策略，可實現一類問題的自動化證明，這些復雜策略中可以融合一些自動證明算法。常用的機械化定理證明器如下：

1）德克薩斯大學奧斯汀分校：ACL2

2）INRIA：Coq

3）劍橋大學：HOL

4）劍橋大學：Isabelle

5）MIT：Larch 系統

6）康奈爾大學：Nuprl

7）斯坦福研究所：PVS

8）卡耐基-梅隆大學：TPS

5 結束語

本文首先通過調研相關標準和文獻，論述形式化方法在軟件可靠性中的意義和必要性。接下來主要考慮模型檢測和程序驗證方法在核電廠控制邏輯驗證中的應用，主要是簡述模型檢測和程序驗證方法的原理、應用實例及相關工具。代碼生成器和編譯器作為工具軟件在安全關鍵領域至關重要，根據現有可信編譯技術包括出具證明編譯器、翻譯確認方法、定理證明方法，考慮將可信編譯技術應用到核電廠儀控工程組態程序的自動生成中，擬使用形式化方法開發代碼生成器。操作系統作為儀控系統中的基礎軟件，目前儀控系統使用的是微內核的操作系統。調研發現目前有很多關于操作系統形式化驗證的研究，可以將形式化技術應用到儀控系統的微內核的驗證中，進一步增加儀控系統的安全性。最后，介紹應用于形式化驗證的工具，簡要介紹了其原理。總而言之，形式化方法在提高核電廠儀控系統軟件可靠性方面有很多的應用場景，但是形式化方法涉及很多的技術分支，并且形式化方法的實施有技術上的難度，從技術理論到實際應用仍然需要進一步探索研究。