一種面向UEFI模塊的形式化建模與驗證方法

王 冠，郝曉星

(1.北京工業(yè)大學 信息學部，北京 100124；2.北京市可信計算重點實驗室，北京 100124)

0 引 言

UEFI作為定義在平臺固件層與操作系統(tǒng)層之間的一個開放且抽象的業(yè)界標準編程接口，與傳統(tǒng)的BIOS相比絕大部分代碼采用C語言編寫，提升了UEFI固件的開發(fā)效率，并且采用驅(qū)動模塊化設計提高了UEFI系統(tǒng)的可擴展性，使得UEFI迅速取代BIOS。與此同時，UEFI固件程序容量幾何數(shù)量增長，功能愈加復雜，新穎的接口以及驅(qū)動加載模式，再加上大量的C語言源碼問題，使得UEFI固件的安全問題更加明顯，更由于UEFI固件在計算機中的特殊位置，使其成為攻擊操作系統(tǒng)的跳板[1]。目前針對UEFI固件的安全檢測技術主要是模糊測試技術、污點分析技術、符號執(zhí)行技術。模糊測試技術[2-3]在大體量軟件漏洞檢測中具有先天優(yōu)勢，可重用性高，但自動化程度不高，效率低下，代碼覆蓋率不高。污點分析技術[4]可提供精確的信息流傳播跟蹤，但需要額外的系統(tǒng)開銷與大量的先驗分析，檢測條件苛刻。符號執(zhí)行技術[5]由于對路徑敏感，狀態(tài)爆炸問題嚴重，沒有很高的分析精度。

形式化方法[6-8]是基于嚴格的數(shù)學基礎，對計算機硬件、軟件系統(tǒng)進行形式規(guī)約、開發(fā)和驗證的技術。形式化驗證方法對程序模型和安全屬性進行自動驗證且驗證時能覆蓋整個程序空間，漏報率低，非常適合高安全級別系統(tǒng)或程序的安全驗證及分析。為對UEFI模塊中安全漏洞進行分析與檢驗，提高UEFI固件的安全性，該文提出一種針對UEFI模塊的形式化建模與驗證的方法。該方法先對UEFI模塊中可能存在的安全漏洞屬性和UEFI模塊進行形式化建模分析，再利用數(shù)據(jù)抽象技術[8-9]緩解形式化驗證過程中的狀態(tài)爆炸問題。

1 相關技術

1.1 形式化方法

形式化方法的兩項主要研究內(nèi)容為形式規(guī)約與形式化驗證。形式規(guī)約利用形式規(guī)約語言描述整個系統(tǒng)的模型或者系統(tǒng)需要滿足的安全屬性[7]。形式化驗證就是驗證現(xiàn)有的程序或者系統(tǒng)是否滿足其形式規(guī)約。形式化驗證有兩種形式，基于演繹的定理證明和基于算法的模型檢驗。定理證明的基本思想為：程序或系統(tǒng)滿足其形式規(guī)約，然后通過一系列推理規(guī)則，以演繹推理的方式來證明此邏輯命題的正確性[7]。模型檢驗[7,9-10]提出的基本思想是：隨著計算機并發(fā)系統(tǒng)的高速發(fā)展，驗證一個程序或系統(tǒng)是否滿足一個公式要比證明該公式在所有情況下均被滿足要容易得多，所以提出了在有限狀態(tài)自動機模型上來驗證公式的可滿足性的新思路。模型檢驗通過自動遍歷程序或系統(tǒng)的有限狀態(tài)來檢驗系統(tǒng)模型與其性質(zhì)規(guī)約的滿足關系。如果程序或系統(tǒng)的形式化模型不滿足給定的性質(zhì)規(guī)約，模型檢驗算法會給出不滿足的反例，可以根據(jù)反例對系統(tǒng)或程序進行分析和調(diào)試，如果模型檢驗算法未發(fā)現(xiàn)反例，則系統(tǒng)或程序一定滿足所檢驗的性質(zhì)[7]。

1.2 有限狀態(tài)自動機

有限狀態(tài)自動機(finite state automaton，F(xiàn)SA)[11-12]分為非確定和確定兩種形式，兩者是等價的，其唯一的區(qū)別就是狀態(tài)轉(zhuǎn)移函數(shù)不同，確定有限狀態(tài)機一個輸入對應一個狀態(tài)轉(zhuǎn)移，非確定有限狀態(tài)自動機一個輸入對應多個狀態(tài)轉(zhuǎn)移，然后從多個狀態(tài)轉(zhuǎn)移中非確定地選擇其中一個。有限狀態(tài)自動機識別正則語言[12]，其所接受的所有字符串構(gòu)成了自動機識別的語言L(M)。確定有限狀態(tài)自動機的定義如下：

定義1：確定有限狀態(tài)自動機(deterministic finite automaton，DFA)可以寫成元組的形式(Q，Σ，δ，Q0，F(xiàn))，其中：

(1)Q表示狀態(tài)的非空有限集合，?q∈Q，q稱為DFA的一個狀態(tài)；

(2)Σ表示輸入字符的集合，Σ={a0,a1,…,an}；

(3)δ表示狀態(tài)轉(zhuǎn)移或移動函數(shù)，δ：Q×Σ*→Q，δ(qn，an)=qm；

(4)Q0∈Q表示DFA的初始狀態(tài);

(5)F?Q表示DFA的終止狀態(tài)集合，?q∈F，q稱為DFA的一個終止狀態(tài)。

確定有限狀態(tài)自動機DFA從初始狀態(tài)Q0開始，逐個讀入字符集Σ中的字符，根據(jù)當前狀態(tài)qn、輸入的字符an和狀態(tài)轉(zhuǎn)移函數(shù)δ來決定DFA的下一狀態(tài)qm。當輸入字符結(jié)束，如果DFA的當前狀態(tài)qm∈F，表示DFA接受該字符集Σ，否則表示DFA不接受該字符集。

1.3 下推自動機

下推自動機(push down automaton，PDA)[11-12]除了包含有限狀態(tài)外，還包括一個長度不限的棧，下推自動機的狀態(tài)轉(zhuǎn)移不僅參考有限狀態(tài)部分還要考慮棧的當前狀態(tài)，狀態(tài)轉(zhuǎn)移過程還包括棧的出棧、入棧操作。下推自動機的定義如下：

定義2：下推自動機PDA可以寫成元組的形式(Q，Σ，Γ，δ，Q0，Z0，F(xiàn))，其中：

(1)Q、Σ、Q0、F與DFA中含義一致;

(2)Γ表示有限的堆棧字母表，為能夠推入堆棧的符號的集合;

(3)δ表示轉(zhuǎn)移函數(shù)，δ為Q×(Σ∪{ε})×Γ到Q×Γ*子集的映射，映射關系：δ(q,a,X)={(q1,γ1)，(q2,γ2)，…，(qn,γn)}，控制著自動機的行為。形式上δ的自變量可以表示為一個三元組δ(q,a,X)，其中q∈Q，表示PDA當前狀態(tài);a∈Σ或a=ε，ε為空串表示不是輸入符號;X∈Γ，表示當前堆棧棧頂符號;

δ的輸出是序?qū)?q,γ)的有窮集合，其中q表示新狀態(tài)，γ表示堆棧符號用來替代當前堆棧棧頂符號X，如果γ=ε，則彈出棧頂元素X，如果γ=X，堆棧不發(fā)生改變，如果γ=YZ，那么棧頂符號X被Z代替，然后Y推入棧；

(4)Z0∈Γ，表示PDA棧中的初始符號。

2 形式化建模與驗證方法設計

該文使用模型檢驗對UEFI模塊進行形式化驗證，其中UEFI模塊代碼采用下推自動機PDA進行建模，UEFI模塊中可能存在的安全漏洞屬性采用確定有限狀態(tài)自動機DFA進行建模，最后采用模型檢驗算法驗證UEFI模塊是否滿足給定的安全漏洞屬性模型。UEFI模塊形式化驗證流程如圖1所示。

圖1 形式化驗證流程

2.1 安全漏洞屬性建模

利用有限狀態(tài)自動機對UEFI模塊的安全漏洞屬性進行建模。首先，需要對安全漏洞進行形式化分析，確定安全漏洞的狀態(tài)集合Q、初始狀態(tài)Q0、終止狀態(tài)集合F。其次，將安全漏洞所涉及的一系列可能的程序點采用抽象語法樹(abstract syntax tree，AST)[13]進行描述，作為有限狀態(tài)自動機的輸入信息Σ。最后，根據(jù)狀態(tài)間的轉(zhuǎn)移關系設計狀態(tài)間的轉(zhuǎn)移函數(shù)δ。安全漏洞的形式化描述中每一次狀態(tài)轉(zhuǎn)移的結(jié)果是確定的，所以基于確定有限狀態(tài)自動機DFA的UEFI模塊安全漏洞屬性模型(security vulnerabilities deterministic finite automaton，SVDFA)的定義如下：

定義3：SVDFA可以寫成元組的形式(Q，Σ，δ，Q0，F(xiàn))，其中：

(1)Q表示安全漏洞所涉及的非空有限狀態(tài)集合，?q∈Q，q為在安全漏洞狀態(tài)轉(zhuǎn)移時可能達到的任意狀態(tài);

(2)Σ表示可能引起安全漏洞狀態(tài)轉(zhuǎn)移的程序操作表達式集合，程序操作源碼轉(zhuǎn)為與上下文無關的AST語法描述的表達式;

(3)δ表示安全漏洞狀態(tài)轉(zhuǎn)移函數(shù)集合，δ：Q×Σ*→Q，δ(qn,an)=qm，qn∈Q表示當前狀態(tài)，an∈Σ表示輸入的程序節(jié)點表達式，qm∈Q表示轉(zhuǎn)移后狀態(tài);

(4)Q0∈Q表示安全漏洞的初始狀態(tài);

一是，養(yǎng)殖草雞需要較大的放養(yǎng)場地，慈王村擁有豐富的土地資源，村民荒地較多，雞舍環(huán)境干凈優(yōu)越。得天獨厚的自然條件極其適宜草雞養(yǎng)殖。二是，草雞優(yōu)良的保健價值日益得到市場的青睞。三是，慈王村領導干部對草雞散養(yǎng)技術、環(huán)境調(diào)控與疾病防疫有一定的研究。四是，慈王村地理位置優(yōu)越，茶園、農(nóng)家樂數(shù)量居多，當?shù)厍逭媸称贰氨床蓦u”遠近聞名，草雞市場供不應求，銷售優(yōu)勢明顯。

(5)F?Q表示滿足安全漏洞的最終接受狀態(tài)集合。

SVDFA的狀態(tài)遷移從初始狀態(tài)Q0開始，如果當前程序執(zhí)行點的AST表達式an與當前狀態(tài)qn能滿足狀態(tài)轉(zhuǎn)移函數(shù)δ(qn,an)=qm，SVDFA當前狀態(tài)由qn變?yōu)閝m，如果程序檢驗完畢，SVDFA在狀態(tài)轉(zhuǎn)移過程中有狀態(tài)q∈F，則表示該程序可能出現(xiàn)安全漏洞模型描述的安全問題，否則沒有出現(xiàn)安全漏洞屬性模型描述的安全問題。UEFI模塊中的安全問題可能非常復雜，如果一開始就對一個復雜的安全問題進行形式化建模將非常困難且不精確。通常一個復雜的安全問題由幾個簡單的安全問題組成，采用笛卡爾乘積的方式將一些簡單安全漏洞屬性模型{Mi=(Qi,Σi,δi,Q0i,Fi)}集合組合成一個復雜的安全漏洞屬性模型S=(Q，Σ，δ，Q0，F(xiàn))，這種建模方式使得安全漏洞描述模塊化，并且使得模型擴展、復用成為可能。

2.2 程序控制流模型

數(shù)據(jù)抽象作為一種解決狀態(tài)爆炸問題的有效手段，其基本思想就是在對系統(tǒng)進行模型檢驗時剔除系統(tǒng)中與檢驗無關的信息，僅保留有用信息，最后對抽象系統(tǒng)進行分析與驗證就會變得容易，進而緩解模型檢驗時的狀態(tài)爆炸問題。將UEFI模塊近似抽象為對應的控制流模型后，對于復雜的UEFI模塊，狀態(tài)空間數(shù)量仍然很多，而要檢驗的安全漏洞屬性往往是有限狀態(tài)空間。該文根據(jù)安全漏洞屬性再次壓縮控制流模型，將控制流模型中與安全漏洞屬性無關的控制流進行刪除，進一步壓縮狀態(tài)空間，最終得到只與安全漏洞屬性相關的UEFI模塊抽象模型。將UEFI模塊代碼抽象為與程序節(jié)點相關的控制流模型，只對抽象出的控制流進行建模，降低整個模型的復雜度。本建模方式關注點在于程序執(zhí)行路徑中有哪些可能被執(zhí)行的函數(shù)或方法以及執(zhí)行順序，并不考慮真實執(zhí)行下的具體數(shù)據(jù)流，是一種對原系統(tǒng)的近似抽象。UEFI模塊的程序控制流圖(UEFI control flow graph，UCFG)定義如下：

定義4：UCFG可以寫為元組的形式(N，E，IE，CE)，其中：

(1)N表示所有程序節(jié)點的集合，?n∈N，n表示程序控制流中的一個程序節(jié)點，n具有三種屬性n(NAME，OP，TYPE)，其中NAME表示程序點的名稱，OP表示程序節(jié)點源碼轉(zhuǎn)為抽象語法樹AST描述后的表達式，TYPE表示程序節(jié)點的類型。程序節(jié)點TYPE有三種類型;

·CALL，表示調(diào)用普通過程(方法或函數(shù))的程序節(jié)點;

·RETURN，表示此程序節(jié)點為return操作;

·OTHER，表示除CALL和RETURN以外的其他程序節(jié)點。

(3)IE表示傳輸邊，為程序控制流中普通過程內(nèi)的程序節(jié)點傳輸邊，IE={|n1,n2∈N且n1,n2屬于同一過程內(nèi)};

(4)CE表示調(diào)用邊，為程序控制流中普通過程間的程序節(jié)點調(diào)用邊，CE={|n1,n2∈N且n1,n2不屬于同一過程內(nèi)}。

例如，在對如圖2所示的函數(shù)調(diào)用序列進行控制流建模時會有：傳輸邊IE={(n1,n2)}，表示一條從程序點n1到程序點n2的過程內(nèi)傳輸邊；調(diào)用邊CE={(n1,nx)，(n2,ny)}，表示會有從程序點n1到函數(shù)FunctionA()定義節(jié)點nx和n2到函數(shù)FunctionB()定義節(jié)點ny兩條調(diào)用邊。

圖2 函數(shù)調(diào)用序列

由于靜態(tài)分析只是對語法語義的分析，并不涉及真實數(shù)據(jù)流，對于條件判斷語句如if-else或while等控制結(jié)構(gòu)，并不會做出精準判斷，目前采用的建模策略為默認每條分支都有可能執(zhí)行，如圖3的代碼序列，會產(chǎn)生傳輸邊IE={(n1,n2)，(n1,n3)}。

圖3 控制結(jié)構(gòu)序列

通過上述UEFI模塊程序控制流模型UCFG，就可以描述一個程序中所有的程序節(jié)點轉(zhuǎn)換路徑，源程序被抽象為一個從入口程序點出發(fā)，沿著傳輸邊IE與調(diào)用邊CE的一條有限或無限的有向圖。

UEFI模塊安全漏洞屬性的有限狀態(tài)機模型SVDFA中的Σ集合數(shù)量有限，且在大多數(shù)情況下遠遠少于程序控制流UCFG中的程序點集合N的數(shù)量，所以在抽象的程序控制流中仍有大量與安全漏洞檢測無關的控制流節(jié)點，該文利用安全漏洞屬性模型SVDFA對程序控制流UCFG進行壓縮，刪減無用節(jié)點，節(jié)點類型的判定算法描述如下：

1.initialize: Uesful Node UF←{}，Uesless Node UL ←{}

2.for ?n∈Ndo

3. ifn∈Eor n.OP∈SVDFA. Σ then

4.UF←{n}

5. end if

6.end for

7.for ?n∈Ndo

8.ifn?UF and (?n∈DFS(n，{IE，CE}) ) ? UF then

9.UL←{n}

10. end if

11.end for

其中DFS(n，{IE，CE})函數(shù)表示找出程序節(jié)點n在邊集{IE，CE}中直接或間接調(diào)用的所有節(jié)點。

2.3 程序建模

將UEFI模塊代碼抽象的程序控制流模型UCFG轉(zhuǎn)換為下推自動機PDA時，Q，Q0，F(xiàn)都只包含一個虛擬狀態(tài){s}，即表示在UCFG→PDA時PDA不存在狀態(tài)的轉(zhuǎn)換，只是利用Σ，Γ，δ來記錄程序節(jié)點的執(zhí)行路徑。UEFI模塊代碼的下推自動機模型(UEFI push down automaton，UPDA)定義如下：

定義5：UPDA可以表示為元組形式(Q，Σ，Γ，δ，Q0，Z0，F(xiàn))，其中：

(1)Q={s}，表示狀態(tài)的有限集合;

(2)Σ={IE∪CE}，表示輸入符號的有限集合，實際為控制流模型UCFG中所有類型邊的集合;

(3)Γ={Ν}，表示有限的堆棧字母表，實際為控制流模型UCFG中所有程序節(jié)點的集合N;

(4)δ表示轉(zhuǎn)移函數(shù)集合，δ為Q×(Σ∪{ε})×Γ到Q×Γ*子集的映射，映射關系：δ(s,a,X)={(s,γ1)，(s,γ2)，…，(s,γn)}。轉(zhuǎn)移函數(shù)生成算法如下:

1.for ?e∈Σ，e={|n1,n2∈Σ} do

2. if e.n1.TYPE=RETURN then

3. UPDA.δaddδ(s，e，e.n1)={(s，ε)}

4. end if

5. if e.n1.TYPE=CALL then

6.UPDA.δaddδ(s，e，e.n1)={(s，e.n2e.n1)}

7. end if

8. if e.n1.TYPE=OTHER then

9. UPDA.δaddδ(s，e，e.n1)={(s，e.n2)}

10. end if

11.end for

(5)Q0=s，表示初始狀態(tài);

(6)Z0∈{E}，表示UPDA堆棧中的初始符號，實際為控制流模型UCFG中的程序入口節(jié)點;

(7)F={s}，表示UPDA的接受狀態(tài)或終結(jié)狀態(tài)集合。

2.4 形式化驗證

基于自動機理論[12]的形式化驗證框架如下：假設采用Σ表示程序中所有程序節(jié)點表達式集合，S?Σ*表示所有符合安全漏洞屬性的程序節(jié)點執(zhí)行序列，γ∈Σ*表示程序中一條可行的程序節(jié)點執(zhí)行序列。Γ?Σ*表示程序中所有可行程序節(jié)點執(zhí)行序列的集合。判斷S∩Γ是否為空，如果為空則說明沒有出現(xiàn)安全漏洞，不為空則可能出現(xiàn)安全問題。

通常程序可能的執(zhí)行序列Γ是不可計算集，因此S∩Γ為一個不可判定問題，但可以通過限定S和Γ的形式將問題具體化來判定。首先，在UEFI模塊中通常的時序安全漏洞屬性的程序節(jié)點序列都能使用正則語言描述，假設S為正則語言，則存在SVDFA可以識別S，即S?L(SVDFA)。其次，程序的可行執(zhí)行路徑需要一個棧來記錄返回調(diào)用者地址，需要用上下文無關語言描述，所以假設Γ為一個上下文無關的語言，則存在UPDA可以識別Γ，即Γ?L(UPDA)。判定S∩Γ變?yōu)榕卸↙(SVDFA)∩L(UPDA)是否為空，則定義P=L(SVDFA)∩L(UPDA)，因為L(SVDFA)為正則語言，L(UPDA)為上下文無關語言，則P為上下文無關語言。同理，P可以被一個下推自動機(security vulnerabilities UEFI push down automaton，SVUPDA)接受，且SVUPDA為SVDFA與UPDA的交集。SVUPDA可由SVDFA與UPDA組合而成[14]，定義如下：

定義6：SVUPDA可以表示為元組形式(Q，Σ，Γ，δ，Q0，Z0，F(xiàn))，其中：

(1)Q表示狀態(tài)的有限集合，實際值為SVDFA中安全漏洞的狀態(tài)集合Q;

(2)Σ表示輸入符號的有限集合，實際值為UPDA中所有類型邊的集合Σ;

(3)Γ表示有限的堆棧字母表，實際值為UPDA中所有程序節(jié)點的集合Γ；

(4)δ表示轉(zhuǎn)移函數(shù)集合，δ為Q×(Σ∪{ε})×Γ到Q×Γ*子集的映射，映射關系：δ(q,a,X)={(q1,γ1)，(q2,γ2)，…，(qn,γn)}。轉(zhuǎn)移函數(shù)生成算法描述如下:

1.for ?i∈UPDA.δ，i(s,e,n1)={(q1，X)}，e={|n1,n2∈Σ} do

2. if i.X=i.n2then

3. for ?j∈SVDFA.δ，j(qn，an)=qmdo

4. if i.n1.op = j.anthen

5.SVUPDA.δaddδ(j.qn，i.e，i.n1)={( j.qm，i.n2)})

6. end if

7. end for

8. end if

9. if i.X = i.n2i.n1then

10. for ?q∈SVDFA.Q do

11.SVUPDA.δaddδ(q，i.e，i.n1)={(q，i.n2i.n1)})

12. end for

13. end if

14. if i.X=εthen

15. for ?q∈SVDFA.Q do

16. SVUPDA.δaddδ(q，i.e，i.n1)={(q，ε)})

17. end for

18. end if

19.end for

從上述轉(zhuǎn)移函數(shù)算法中可知，當UPDA中的程序節(jié)點類型TYPE為CALL或RETURN時，SVUPDA的狀態(tài)不發(fā)生變化，只是記錄SVUPDA的堆棧變化，當UPDA中的程序節(jié)點類型TYPE為OTHER時，既記錄SVUPDA的堆棧變化，也記錄了狀態(tài)的轉(zhuǎn)移。

(5)Q0表示初始狀態(tài)，實際值為SVDFA中安全漏洞的初始狀態(tài)Q0;

(6)Z0表示堆棧中的初始符號，實際值為UPDA中棧初始符號Z0；

(7)F表示SVUPDA的接受狀態(tài)或終結(jié)狀態(tài)集合，實際值為SVDFA中的安全漏洞的最終接受狀態(tài)集合F。

通過文獻[15-16]中的模型檢驗算法判斷SVUPDA接受的語言L(P)是否為空就可判斷是否出現(xiàn)安全漏洞，如果為空，則表示未出現(xiàn)安全漏洞模型SVDFA描述的安全漏洞，不為空則表示可能出現(xiàn)所描述的問題，需要確認是否為誤報。之所以出現(xiàn)誤報，是因為靜態(tài)的語法語義分析并不考慮實際數(shù)據(jù)流，Γ除了接受實際可行路徑集合外，也會接受實際數(shù)據(jù)流時不會發(fā)生的路徑。但是，因為Γ?L(UPDA)，可以得到S∩Γ?L(SVDFA) ∩L(UPDA)，這保證了給定安全漏洞屬性模型的完全性，即可能存在誤報但無漏報。

3 實驗結(jié)果與分析

基于自動機的模型檢驗主要能力取決于對UEFI模塊中安全漏洞屬性模型描述的豐富性、準確性，以及是否有狀態(tài)爆炸引起的性能問題。在安全漏洞屬性模型豐富性方面，該文考慮到UEFI模塊中可以通過引入StdLib包調(diào)用C標準庫及GNU C庫，對UEFI標準庫、C標準庫及CNU C庫進行分析，總結(jié)了六種類型的安全漏洞模型，安全漏洞模型的分類與數(shù)量如下：緩沖區(qū)溢出類型13種；資源重復釋放5種；空指針引用7種；格式化字符串9種；競態(tài)條件3種；函數(shù)調(diào)用路徑7種。該文共對12個UEFI模塊代碼混合植入上述六類，44種的安全漏洞，共計563個由國家信息安全漏洞庫CNNVD公布的EDKII中真實安全漏洞，對UEFI模塊進行形式化驗證，驗證結(jié)果如表1所示。

表1 安全漏洞檢測結(jié)果

從表1可以看出，在被檢測的UEFI模塊中，植入563個安全漏洞，檢測報出604個可能存在的安全問題，其中包括檢測出557個植入的安全漏洞，誤報47個，統(tǒng)計漏報率1.06%，誤報率7.78%。經(jīng)過分析發(fā)現(xiàn)，漏報的主要原因是安全漏洞屬性模型的不豐富造成，符合安全漏洞模型的安全漏洞都可以檢測出來，檢測結(jié)果基本符合形式化驗證中闡述的不會有漏報的理論，降低漏報率的主要方法是不斷豐富和精確安全漏洞屬性模型。誤報率達7.78%，經(jīng)分析發(fā)現(xiàn)，大部分誤報都是由于靜態(tài)分析時并沒有考慮真正數(shù)據(jù)流，在模型檢驗時有大量真實情況下不可達路徑的原因，例如資源重復釋放、競態(tài)條件、函數(shù)調(diào)用路徑類漏洞的誤報，主要是因為真實數(shù)據(jù)流情況下會在條件判斷的確定分支里進行資源釋放，在程序抽象時會對條件判斷的所有的分支進行統(tǒng)計，造成誤報。對于性能分析，主要是驗證在對程序控制流進行壓縮和未壓縮時的性能分析，來驗證壓縮算法可以緩解狀態(tài)爆炸，提高檢測性能。該文對代碼規(guī)模約為500～5 000行范圍的UEFI模塊分別植入相同的6類，共65個安全漏洞進行20次檢驗，耗時平均值結(jié)果如圖4所示。

圖4 模型檢驗耗時

隨著代碼規(guī)模的增大，程序的狀態(tài)空間會呈現(xiàn)指數(shù)增長趨勢，在計算機性能不變的前提下，在未壓縮的模型檢驗中，耗時與狀態(tài)空間成正比，耗時趨勢呈指數(shù)增長，預計隨著代碼規(guī)模持續(xù)增大會出現(xiàn)狀態(tài)爆炸，內(nèi)存不足的問題。在壓縮后的模型檢驗中，狀態(tài)空間是跟軟件規(guī)模和安全漏洞屬性狀態(tài)數(shù)量組成的線性函數(shù)，隨著軟件規(guī)模持續(xù)增大，狀態(tài)空間線性增長，達到緩解狀態(tài)爆炸的目的。

4 結(jié)束語

固件主要負責計算機中硬件初始化和預備操作系統(tǒng)啟動環(huán)境等功能，處于計算機中極其重要的位置，有著較高的安全級別，并且隨著UEFI模塊規(guī)模的逐漸龐大，被攻擊面逐漸增加。該文提出一種針對UEFI模塊的形式化建模與驗證的方法，基于有限狀態(tài)自動機和下推自動機分別對UEFI模塊中的安全漏洞屬性和代碼進行形式化建模，采用模型檢驗算法進行形式化驗證，同時利用數(shù)據(jù)抽象的思想壓縮程序控制流的狀態(tài)規(guī)模，緩解狀態(tài)爆炸問題。對44種UEFI模塊中可能出現(xiàn)的安全問題進行建模，12個植入安全問題且不同代碼規(guī)模的UEFI模塊進行形式化驗證，實驗結(jié)果表明，該檢驗方法漏報率為1.06%，誤報率7.78%，并較好地緩解了狀態(tài)爆炸問題。