形式化驗證技術(shù)在核電廠DCS中的應(yīng)用研究

侯榮彬，馬 權(quán)，蘭 林，李 勇，楊 斐，薛 凱，吳亞波

（中國核動力研究設(shè)計院 核反應(yīng)堆系統(tǒng)設(shè)計技術(shù)重點實驗室，成都 610213）

0 引言

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

1 核電廠儀控工程應(yīng)用軟件的正確性驗證

1.1 模型檢測

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

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

1.2 程序驗證

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

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

圖1 模型檢查和程序驗證在核電廠儀控工程應(yīng)用軟件開發(fā)過程中的應(yīng)用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 代碼生成器和編譯器關(guān)系示意圖Fig.2 Schematic diagram of the relationship between code generator and compiler

2 可信編譯器的開發(fā)

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

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

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

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

圖4 操作系統(tǒng)的微內(nèi)核架構(gòu)Fig.4 The microkernel architecture of the operating system

3 操作系統(tǒng)驗證

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

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

圖5 操作系統(tǒng)的形式化設(shè)計和驗證框架Fig.5 Formal design and verification framework of operating system

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

4 開發(fā)工具-高階邏輯和證明助手

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

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

2）INRIA：Coq

3）劍橋大學：HOL

4）劍橋大學：Isabelle

5）MIT：Larch 系統(tǒng)

6）康奈爾大學：Nuprl

7）斯坦福研究所：PVS

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

5 結(jié)束語

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