杜澤民 王曉玲 陳宜成

摘 要：互聯(lián)網(wǎng)技術(shù)的發(fā)展和應(yīng)用在各個生產(chǎn)領(lǐng)域中發(fā)揮著越來越積極的作用，但隨著網(wǎng)絡(luò)技術(shù)應(yīng)用的深入，網(wǎng)絡(luò)系統(tǒng)的實時性成為影響網(wǎng)絡(luò)安全的一大因素，因此對網(wǎng)絡(luò)模型的通信實時性、威脅分析實時性的驗證成為網(wǎng)絡(luò)安全的重要保障。目前，國內(nèi)外在實時性驗證方面有諸多研究，形成了不同的方法體系。文章把主要的模型實時性驗證方法，從理論和工具角度加以介紹分析，并對各個方法進行了比較。

關(guān)鍵詞：網(wǎng)絡(luò)安全；實時性；模型驗證；實時性驗證

中圖分類號：TP393.0 文獻標識碼：A

1 引言

在互聯(lián)網(wǎng)時代，網(wǎng)絡(luò)安全問題是互聯(lián)網(wǎng)建設(shè)的重要議題，而網(wǎng)絡(luò)系統(tǒng)的實時性是網(wǎng)絡(luò)安全的重要保證[1]。其中，包括通信的實時性以及威脅分析的實時性等。當網(wǎng)絡(luò)受到外界攻擊時，系統(tǒng)應(yīng)該對相應(yīng)的問題快速做出反應(yīng)并處理措施。問題處理完畢后，還應(yīng)將處理結(jié)果在規(guī)定的時間內(nèi)反饋給系統(tǒng)。實時網(wǎng)絡(luò)系統(tǒng)的每一個運行過程都是為了能夠保證整個網(wǎng)絡(luò)系統(tǒng)各項工作的協(xié)調(diào)進行。

模型驅(qū)動方法面對復(fù)雜度、集成性更高的大型系統(tǒng)有著安全性高、開發(fā)成本低等優(yōu)勢。當前的航空、航天控制系統(tǒng)、軍事指揮自動化系統(tǒng)，也逐漸采用基于模型的開發(fā)方式，而這類系統(tǒng)對軟件有著應(yīng)實時性要求，反應(yīng)時間要控制在幾毫秒以內(nèi)，而通常還要求保留一定的反應(yīng)余量。因此，模型驗證在網(wǎng)絡(luò)系統(tǒng)的實時性驗證上具有先天優(yōu)勢。

目前，國內(nèi)外對模型的功能與正確性驗證研究比較豐富，但是實時性驗證研究并不廣泛。因此，本文將介紹當前實時性驗證所面臨的問題，并重點介紹網(wǎng)絡(luò)系統(tǒng)實時性驗證領(lǐng)域的建模方法，并結(jié)合這些方法所依托的工具，分析各種方法所面臨的問題，最后針對檢測方法面臨的挑戰(zhàn)提出一些思路。

2 模型驗證方法及面臨的問題

模型檢測首先要對系統(tǒng)建模，選用一種形式化描述方法，將待驗證的系統(tǒng)設(shè)計轉(zhuǎn)化為工具所能接受的模型，比如狀態(tài)遷移圖。然后，將系統(tǒng)所要驗證的性質(zhì)采用形式化的邏輯公式來描述，比如時態(tài)邏輯。它能夠描述系統(tǒng)隨著時間變化而引起的行為變化。最后是系統(tǒng)驗證，是通過模型檢測算法對系統(tǒng)模型的狀態(tài)空間進行窮盡搜索。如果未發(fā)現(xiàn)違反性質(zhì)描述的狀態(tài)，則表明該模型滿足期望的性質(zhì)，否則給出一個反例路徑，供設(shè)計人員參考。

模型驗證方法應(yīng)用初期，系統(tǒng)的狀態(tài)和狀態(tài)間的遷移都是采用顯式的狀態(tài)遷移圖來表示。這種方法對那些進程數(shù)量較少的網(wǎng)絡(luò)系統(tǒng)非常實用[2]。而當網(wǎng)絡(luò)分量較多時，系統(tǒng)的全局狀態(tài)空間會隨著分量的增加，呈指數(shù)增長，即產(chǎn)生狀態(tài)爆炸問題，狀態(tài)爆炸問題是阻礙模型檢測技術(shù)應(yīng)用的瓶頸。

3 建模方法

3.1 最差情況執(zhí)行時間方法

最差情況執(zhí)行時間（Worst-Case Execution Time，WCET）是驗證系統(tǒng)實時性的主要方法之一，由奧地利維也納技術(shù)大學的Puschner和Burns提出[3]。WCET剛提出時，由于當時計算機軟件需求有限，軟件代碼的執(zhí)行時間未引起人們的重視。但是，隨著軟件技術(shù)的不斷發(fā)展，代碼執(zhí)行時間的越來越復(fù)雜，WCET分析技術(shù)逐漸受到研究者的重視，目前，國內(nèi)外有許多機構(gòu)或大學開始加深對WCET的研究，從2001年開始，國際上每年召開一次WCET研討會。WCET分析技術(shù)與計算方法趨于多樣化，從早期的程序標注和語法制導算法發(fā)展為基于樹和路徑的計算方法。

WCET分析是指計算給定應(yīng)用程序代碼片斷執(zhí)行時間的上限，這里的執(zhí)行時間定義為執(zhí)行代碼片斷所花費的處理器時間。在實時系統(tǒng)中，如果想保證系統(tǒng)整體的實時性得到滿足，就必須要求軟件各部分在最差情況下執(zhí)行的時間也能滿足實時性要求，這樣由部分集成到整體時，整個系統(tǒng)才會滿足實時性的要求。

WCET分析要求安全性和精確性，安全要求不能低估最差執(zhí)行時間，精確要求能夠給出可以接受的高估值。我們假設(shè)程序P的WCET估算值為WCETc （P），P的實際WCET值為WCETA （P），安全性和精確性描述為：

安全性：

WCETc （P） ≥WCETA （P）

精確性：

（WCETc（P） -WCETA（P））/WCETA（P）≤δmax

其中，δmax為系統(tǒng)能夠接受的最大相對誤差。

在程序?qū)哟蔚尿炞C方面，國防科技大學張曦團隊利用WCET技術(shù)對嵌入式實時軟件的驗證進行了深入研究，提出了一種基于WCET分析的模型檢驗方法框架[4]，實現(xiàn)了對源程序的一種實時性驗證方法。

該框架首先對源程序進行WCET分析，其中包括對程序的靜態(tài)分析，劃分出程序代碼的路徑集，然后利用WCET工具進行分析程序執(zhí)行時間上限，分析過程如圖1所示。

利用WCET分析結(jié)果對原有的實時約束進行修正，建立系統(tǒng)的實時性模型，同時在系統(tǒng)需求中提取時態(tài)邏輯作為系統(tǒng)的性質(zhì)描述，其中時態(tài)邏輯反映了程序應(yīng)該遵循的先后順序。結(jié)合實時性模型與時態(tài)邏輯公式通過驗證工具UPPAAL對模型的實時性進行驗證，如果實時性驗證不通過，則返回修改源程序。如圖2所示。

本方法做到了對實時系統(tǒng)的程序?qū)哟蔚尿炞C，較好地解決了狀態(tài)爆炸問題，其中源程序的WCET分析是驗證環(huán)節(jié)的重要一環(huán)，但是當前WCET分析能力有限，比如復(fù)雜程序運算時間估算、估值精確度、誤差控制等問題。另外，對源程序的修正可能會引入新的錯誤，并且修正內(nèi)容無法反映到生成代碼的上層模型中。

3.2 時間自動機建模

為了描述實時系統(tǒng)的時間約束關(guān)系，Alur等人提出了時間自動機（Timed Automata，TA）[5]。時間自動機是一類帶有時鐘變量的有限狀態(tài)自動機，其數(shù)學模型可表述為一個六元組：

Ta= （L，L0，C，A，E，I ）

其中：L是位置的有限集合；l0∈L，為初始位置；C是時鐘有限集合；A是行為的有限集合；"EL×B（C）×A×2c×L是邊的集合，用于描述位置之間的轉(zhuǎn)移；B（C）是使能條件集合，用于描述發(fā)生轉(zhuǎn)移的時間約束，2c為轉(zhuǎn)移發(fā)生時的時鐘集合；映射I："L→ B（C）" 用于給每個位置指定一個時鐘約束。

用時間自動機網(wǎng)對實時系統(tǒng)建模，首先要對系統(tǒng)進行抽象和簡化，子系統(tǒng)要簡化為有限控制結(jié)構(gòu)、時鐘和變量構(gòu)成的時間自動機，子系統(tǒng)之間通過通道進行通訊。然后要分析實時系統(tǒng)的信息處理過程，提煉重要的信息處理狀態(tài)和事件進行建模。子系統(tǒng)的行為抽象為時間自動機，它們之間的信息交互通過通道來完成，各個時間自動機就組成網(wǎng)絡(luò)進而描述整個實時系統(tǒng)的信息處理過程。

時間自動機是一種反映了時間約束的有限狀態(tài)轉(zhuǎn)換圖，通過使用有限的真值時鐘變量表示時間約束，實時系統(tǒng)行為可以通過時間自動機來刻畫，在對實時系統(tǒng)建模后，可以利用時間自動機來驗證系統(tǒng)的實時性。在實時性約束下檢驗狀態(tài)是否可達，因此對狀態(tài)可達性的研究是時間自動機的驗證技術(shù)的關(guān)鍵。

時間自動機技術(shù)也有不足：構(gòu)造時間自動機方法很復(fù)雜，如果發(fā)生錯誤，將導致最終驗證結(jié)果的不準確。另外，時間自動機的時間無限制，會導致狀態(tài)空間的無限性，隨著系統(tǒng)的復(fù)雜程度和進程數(shù)量的增加，將無可避免的發(fā)生狀態(tài)空間爆炸。狀態(tài)空間爆炸也是困擾實時系統(tǒng)驗證的最大問題。

但是，典型的時間自動機組成的平面網(wǎng)絡(luò)作為模型不易于模擬和調(diào)試大規(guī)模的工業(yè)系統(tǒng)。AIexandre David和Wang Yi提出了一種層疊時間自動機（Hierarchical Timed Automata，HTA）模型，它的狀態(tài)既可以是簡單狀態(tài)也可以是組合狀態(tài)，組合狀態(tài)本身就是一個時間自動機。

層疊時間自動機的允許用戶在模擬時，將系統(tǒng)模型的內(nèi)部結(jié)構(gòu)隱藏或者抽象，并且更容易調(diào)試，在處理多層次復(fù)雜系統(tǒng)建模時有較大優(yōu)勢。

3.3 RTCTL模型檢測方法

計算樹邏輯（Computation Tree Logic，CTL）是時序邏輯的一個分支，時序邏輯非常適合于對并發(fā)系統(tǒng)進行驗證與刻畫，即使對于復(fù)雜的并發(fā)系統(tǒng)而言，其刻畫性質(zhì)依然很強。時序邏輯用于描述系統(tǒng)中的狀態(tài)變遷序列，不顯示地表示時間，而是通過語義隱式表達時間。時序邏輯定義時序運算符與邏輯連接詞來表達復(fù)雜的時序性質(zhì)。CTL作為時序邏輯的一個分支主要用來描述計算樹的性質(zhì)[8]。

CTL公式由路徑量詞與時序運算符組成。路徑量詞用于描述計算樹的分支結(jié)構(gòu)，有兩種路徑量詞：A（對于所有計算路徑）和E（對于某些計算路徑），分別表示從某狀態(tài)開始的所有路徑和某些路徑所具有的性質(zhì)。時序運算符描述某條路徑的具體性質(zhì)。有5個基本運算符，意義如下：X（下一個狀態(tài)）F（將來某狀態(tài)）G（將來全局狀態(tài)）U（直到……都滿足）R（直到……才滿足）。

CTL有兩種公式：狀態(tài)公式與路徑公式。令A(yù)P為原子命題集合，狀態(tài)公式語法為：

1） 如果p∈AP，則p是一個狀態(tài)公式；

2） 如果f和g是狀態(tài)公式，則f和f∧g，f∨g是狀態(tài)公式；

3） 如果f是一個路徑公式，則Ef和Af是狀態(tài)公式。

路徑公式的語法為：

如果f是一狀態(tài)公式，則f也是一路徑公式；

如果f和g是路徑公式，則f，f∧g，f∨g，Xf，F(xiàn)f，Gf，fUg和飛fRg是路徑公式[9]。

檢測實時系統(tǒng)的時間約束的有效方法就是擴充CTL運算符，Emerson等人將CTL邏輯擴充為RTCTL?；镜腞TCTL運算符是受限的直到運算符U[a，b]這里[a，b]表示時間間隔，在此間隔內(nèi)這個性質(zhì)必須是真的。fU[a，b]g關(guān)于某條路徑π=s0，s1…為真，僅當g在此路徑上將來的某個狀態(tài)s上滿足，那么f在s0到s上所有狀態(tài)都為真，并且s0到s的距離在間隔[a，b]之間。同樣的，CTL中的其他運算符可以增加時間限制來擴展。[a，b]作為一個時間間隔，可以看做是實時性的約束。

RTCTL模型在CTL的基礎(chǔ)上進行了擴充，繼承了CTL模型的精確性，解決了狀態(tài)空間爆炸問題，同時加入了時間性約束，可以高效地表達實時性要求。目前有很多工具可以完成基于CTL的模型驗證，RTCTL在實時性驗證中的有很好的應(yīng)用前景。

通過對時間進行量化分析，可以得到系統(tǒng)的最大、最小時延，完成實時性驗證。

4 模型驗證常用工具

4.1 UPPAAL

UPPAAL是丹麥Aalborg和瑞士Uppsala大學聯(lián)合開發(fā)[10]，高效實用的基于時間自動機的實時系統(tǒng)模型驗證工具。UPPAAL特別適用于實時系統(tǒng)的安全性和活性的自動驗證。它將每個進程都描述為有限控制結(jié)構(gòu)、時鐘和變量組成的時間自動機，進程之間通過管道共享數(shù)據(jù)變量進行通信，管道用于保證不同自動機中的兩個轉(zhuǎn)換同時執(zhí)行。UPPAAL通過快速搜索機制來驗證時鐘約束和可達性，不僅可以有效地發(fā)現(xiàn)設(shè)計中出現(xiàn)的錯誤，而且可以清楚地顯示導致錯誤的判定路徑。

UPPAAL擁有圖形用戶界面，主要包括三個部分：編輯器（Editor）、模擬器（Simulator）和驗證器（Verifier）。編輯器用于創(chuàng)建和編輯所要分析的系統(tǒng)；模擬器用于模擬系統(tǒng)模型執(zhí)行過程可能出現(xiàn)的錯誤，以便在驗證前發(fā)現(xiàn)潛在的錯誤；驗證器通過快速搜索機制搜索系統(tǒng)的狀態(tài)空間、檢查時鐘約束和響應(yīng)限制性質(zhì)。

UPPAAL體系結(jié)構(gòu)如圖3所示。

UPPAAL的引入，簡化了實時系統(tǒng)驗證的工作量，并且增加了驗證系統(tǒng)的可靠性。首先，UPPAAL中時間自動機網(wǎng)絡(luò)中每個時間自動機都是相對獨立的，又是可以互相通信的，不需要構(gòu)造時間自動機的積，避免了構(gòu)造模型的繁雜。另外，UPPAAL中的模擬器從直觀上可以看到系統(tǒng)的運行過程，發(fā)現(xiàn)存在的問題，而驗證器又嚴格的從語義上保證了系統(tǒng)的安全性。UPPAAL在時間和空間上的性能顯著高于其他的實時驗證工具，能夠處理較為復(fù)雜的系統(tǒng)。

4.2 NuSMV

1987年左右，卡內(nèi)基梅隆大學在讀博士生McMillan開發(fā)出一個符號模型驗證器SMV（Symbolic Model Verifier），首次使用二叉決策圖（Binary Decision Diagram，BDD）來緩解狀態(tài)爆炸問題，實現(xiàn)了符號模型檢測技術(shù)，SMV是第一個基于BDD的符號模型驗證工具[11]。2001年，Carnegie Mellon University（CMU）和Istitutoperla Ricerca Scientificae Techolgica（IRST）聯(lián)合開發(fā)出NuSMV（ New Symbolic Model Verifier）[12]，NuSMV支持計算樹邏輯（Computation Tree Logic，CTL）和線性時序邏輯（Linear Temporal Logic，LTL）描述的所有規(guī)范，作為一款比較成熟的模型檢測工具已經(jīng)發(fā)展到2.6.0版，NuSMV是開源工具，其源代碼和二進制文件可以在官網(wǎng)上獲取。

作為一種通用的模型驗證器，NuSMV的基本運行原理：用戶使用NuSMV提供的輸入語言描述待驗證實時系統(tǒng)和約束性規(guī)范，通過NuSMV自動進行，驗證確定模型在規(guī)范中是否成立，若不成立輸出No，并給出反例，解析為什么規(guī)范在模型中不成立。NuSMV的運行原理如圖4所示。

在功能上，NuSMV支持CTL描述規(guī)范，所以RTCTL同樣可以在NuSMV上得到驗證，NuSMV在實時驗證領(lǐng)域占有一席之地。

在結(jié)構(gòu)上，NuSMV定義了一個良好的軟件系統(tǒng)架構(gòu)，做到了模塊化和開放性，用戶可以自由定制模塊。

在支持性上，NuSMV有豐富的文檔和開放的源碼，作為一種模型檢測的通用平臺，用戶可以在官網(wǎng)和開源社區(qū)獲得幫助。

NuSMV的引入，明顯地簡化了實時系統(tǒng)驗證的工作量，研究者提供了更廣闊的研究空間[13]。

4.3 PAT

PAT[14]是由新加坡國立大學PAT研究小組自主開發(fā)的一套模型檢測工具，支持并發(fā)、網(wǎng)絡(luò)實時系統(tǒng)的建模驗證，能夠?qū)Χ喾N語言進行模擬驗證和反例生成。PAT是一個可擴展、模塊化的通用架構(gòu)，其系統(tǒng)框架如圖5所示。

框架分為四層，方便了模塊的擴展，建模驗證過程分為三步：編譯、抽象和驗證。PAT工具具有良好的擴展性，因此可以利用建模層的抽象功能對建模語言進行抽象，避免狀態(tài)爆炸。擴展PAT的并行模塊可以方便網(wǎng)絡(luò)系統(tǒng)的實時性的建模與驗證。抽象后的語言模塊能夠自動轉(zhuǎn)化為PAT已經(jīng)支持的語言，從而簡化系統(tǒng)描述和實現(xiàn)過程，使得建模過程更人性化、更易使用。借助PAT工具良好的擴展性，可方便對網(wǎng)絡(luò)系統(tǒng)進行實時性建模。

4 結(jié)束語

本文首先介紹了模型驗證的概念與當前的問題，并總結(jié)了三種網(wǎng)絡(luò)實時性模型的驗證方法和主流的實時性驗證工具，對其優(yōu)缺點進行了比較，為今后的研究提供有益參考。網(wǎng)絡(luò)安全領(lǐng)域的模型檢測技術(shù)應(yīng)用越來越廣泛。保障日益復(fù)雜的網(wǎng)絡(luò)空間的安全性，是當前研究的難題，建立在嚴格數(shù)學理論基礎(chǔ)之上的模型驗證必將在其中占據(jù)一席之地。

參考文獻

[1] 劉權(quán)，王超.勒索軟件攻擊事件或?qū)⒁l(fā)網(wǎng)絡(luò)軍備競賽升級[J].網(wǎng)絡(luò)空間安全，2018，01：1-4.

[2] 張修康，金春華，白瑩.應(yīng)對網(wǎng)絡(luò)安全威脅的技術(shù)演變[J].網(wǎng)絡(luò)空間安全，2018，01：46-50.

[3] PETER PUSCHNER and A.Burns. Guest Editorial： A Review of Worst-Case Execution-Time Analysis， Real-Tim Systems， May 2000， 18（2-3）： 115～128.

[4] 張曦.基于WCET分析技術(shù)的程序?qū)崟r性模型檢驗方法研究[D].國防科學技術(shù)大學，2012.

[5] Alur R， Dill DL. A theory of t imed automat a[J] . Theoretical Computer Science， 1994， 126（ 2） ： 183- 235.

[6] David A ， Yi W . Hierarchical Timed Automat a for UPPAAL [ A ] .10th Nordic Workshop on Programming Theory （ NWPT） 98） [ C] .Turku Cent re f or Computer Science （T UCS） ， Finland， 1998.

[7] Michael Huth and Mark Ryan.Logic in Computer Science：Modelling and Reasoning about System，Second Edition.Cambridge University Press，2004.

[8] E.M.Clarke and E.A.Emerson.Synthesis of synchronization skeletons for branching time temporal logic.In Logic of Programs：Workshop，Yorktown，Heights NY May 1981，volume 131 of LNCS.Springer-Verlag，1981.

[9] Emerson E.A..Branching time temporal logic and the design of correct concurrent programs[Ph.D.dissertation].Harvard University，Cambridge，MA，1981

[10] Behrmann G， David A， Larsen KG. A tutorial on UPPAAL. In： Bernardo M， ed. Proc. of the Formal Methods for the Design of Real-Time Systems. Springer-Verlag， 2004. 200?236. [doi： 10.1007/978-3-540-30080-9_7]

[11] 張軍林，張治國.NuSMV模型驗證器實現(xiàn)與分析[D].中山大學，2010.

[12] CIMATTI A，CLARKE E，GIUNCHIGLIA F，et al.NuSMV： a new symbolic model verifier[C]Computer Aided Verification.Berlin： Springer，1999： 495-499.

[13] 劉博，李蜀瑜.基于NuSMV的AADL行為模型驗證的探究[J].計算機技術(shù)與發(fā)展，2012，（2）.

[14] LIU Y， SUNJ， DONGJS.Developing model checkers using PAT[C]//8th International Symposium on Automated Technology for Verification and Analysis. Sydney： Springer Press， 2010：371-377.