張朋輝，田曦，樓康威

（國防科學(xué)技術(shù)大學(xué)電子科學(xué)與工程學(xué)院，湖南 長沙 410003）

基于軟硬件協(xié)同形式驗證的固件漏洞分析技術(shù)

張朋輝，田曦，樓康威

（國防科學(xué)技術(shù)大學(xué)電子科學(xué)與工程學(xué)院，湖南 長沙 410003）

為了系統(tǒng)高效地分析固件中潛在的安全隱患，提出了一種基于行為時序邏輯TLA的軟硬件協(xié)同形式驗證方法。通過對固件工作過程中的軟硬件交互機制進行形式建模分析，在動態(tài)調(diào)整攻擊模型的基礎(chǔ)上，發(fā)現(xiàn)了固件更新過程中存在的安全漏洞，并通過實驗證實了該漏洞的存在，從而證明了形式驗證方法的可靠性。

固件安全；TLA；形式驗證；漏洞分析；軟硬件協(xié)同

針對固件安全性的研究目前主要基于軟件漏洞分析方法，大多局限在代碼層面，通過使用軟件安全研究中常用的手工測試、Fuzzing測試技術(shù)［3，4］、二進制比對技術(shù)［5］以及動態(tài)分析技術(shù)［6］等，嘗試從固件的源代碼中發(fā)現(xiàn)漏洞。這些方法一方面工作量較大，需要研究人員具有較強的軟件開發(fā)和測試能力，另一方面可持續(xù)性不足，無法形成一個系統(tǒng)高效的檢測方法。除此以外，由于純粹從代碼方面考慮，這些方法遵循的是傳統(tǒng)代碼漏洞挖掘方法的原則，無法結(jié)合硬件設(shè)備的運行來驗證代碼行為，更多針對的是源代碼中是否存在惡意代碼進行檢測，沒有關(guān)注固件在運行過程中同硬件架構(gòu)的交互細(xì)節(jié)，即軟硬件協(xié)同細(xì)節(jié)，進而也不能對硬件的行為和軟硬件交互進行建模分析，檢測不出實際運行過程中可能產(chǎn)生的一些漏洞。

形式驗證的方法能夠很好地彌補上述傳統(tǒng)方法的不足，通過使用數(shù)學(xué)語言對軟件或者硬件內(nèi)部模塊抽象建模，可以非常直觀地研究其內(nèi)部運行機制。另外，形式語言可以對已有的軟硬件模型綜合分析，隨著建模細(xì)節(jié)的增多，形式語言不僅可以對軟硬件模塊內(nèi)部的運行進行檢驗，還可以對模塊之間的信息流進行分析驗證。然而，當(dāng)前形式驗證的方法大多集中在軟件［7，8］和協(xié)議［9］的安全性設(shè)計及驗證中，少部分面向硬件的研究也僅僅側(cè)重門級邏輯的檢驗和功能設(shè)計的正確性驗證等［10，11］，沒有或很少涉及固件中軟硬件協(xié)同工作的底層細(xì)節(jié)。

為此，本文提出了基于TLA（temporal logical of actions）行為時序邏輯的軟硬件協(xié)同形式驗證分析方法，以固件運行過程中的軟硬件協(xié)同工作機制為主要內(nèi)容進行安全研究。不同于傳統(tǒng)的單一從硬件或軟件出發(fā)進行安全驗證，本文以硬件工作流程為基礎(chǔ)，結(jié)合軟件對硬件的調(diào)用過程綜合分析了計算機開機過程中可能存在的風(fēng)險。首先，通過TLA+語言對固件的架構(gòu)體系和軟硬件執(zhí)行過程進行形式建模分析，給出了固件驅(qū)動硬件的動作以及硬件對固件的反饋判斷信息等形式模型；然后，結(jié)合攻擊模型Attack全面分析軟硬件協(xié)同工作過程中可能存在的安全風(fēng)險，通過分析模型檢測器TLC（TLA+ checker）所提供的錯誤路徑，檢驗了固件對硬件行為的控制是否存在被惡意修改的可能及其給計算機安全帶來的影響；最后，通過實驗證明了這種方法的可行性。

TLA最初是由Lamport設(shè)計，用來描述和推斷操作系統(tǒng)的狀態(tài)［12］。TLA+是基于此邏輯擴展出的一套完整性描述語言。借助這一語言，可以用較簡單抽象的形式模型來描述一些復(fù)雜的軟硬件架構(gòu)，同時結(jié)合模型檢測工具TLC，能夠在諸如軟件安全分析、協(xié)議安全分析、硬件設(shè)計完整性驗證以及軟硬件體系漏洞挖掘等方面極大地提高研究效率，這一特點使其在目前的研究工作中得到了越來越廣泛的使用。TLC是形式語言TLA+的模型檢測工具，用于檢查TLA+規(guī)范中定義的性質(zhì)能否被滿足，還可以用于在TLA+規(guī)范中查找錯誤或者是在定義的系統(tǒng)模型中挖掘安全隱患［13］。實際運行的時候，TLC工具可以將TLA+規(guī)范中所有獨立可達的狀態(tài)統(tǒng)計出來。

2 行為時序邏輯TLA以及其TLC工具

一個TLA+模型通常由許多模塊（module）組成，模塊中包含模型中用到的所有變量、狀態(tài)、行為（behavior）、動作（action）、狀態(tài)謂詞（predicate）、各種操作符以及可選的持續(xù)性制約條件等。描述對象系統(tǒng)所具有的性質(zhì)可以通過抽象的變量或者常量來表示，狀態(tài)就是一個系統(tǒng)中所有變量的一組特定取值，變量取值的變化表示系統(tǒng)從一種狀態(tài)進入了另一種狀態(tài)。行為由系統(tǒng)中一系列連續(xù)發(fā)生的狀態(tài)組成，本文通過定義各種可能的行為來表示一個系統(tǒng)的規(guī)范。TLA+可以對狀態(tài)的轉(zhuǎn)變做出描述，新舊2種狀態(tài)下變量的表示方法不一樣。變量的新狀態(tài)會在表示符號的右上角加一個“′”，如果用x來表示某種系統(tǒng)屬性，那么下一狀態(tài)下其表示方法為x ′。如果一個TLA+公式中，既含有形如x的變量，又含有形如x ′的變量，則表征的是一種新舊狀態(tài)之間的轉(zhuǎn)換關(guān)系，那么這樣的公式就是一個動作，最常見的動作就是狀態(tài)轉(zhuǎn)換關(guān)系（next state relation）。狀態(tài)謂詞是指不帶“′”的時序公式，如初始狀態(tài)謂詞（initial predicate）。TLA+的操作符有很多，理論上基礎(chǔ)數(shù)學(xué)中用于集合、量化、關(guān)系等的操作符都可以使用，比如“?”、“?′”和“＞”等。除此以外，在表征系統(tǒng)狀態(tài)演進時，TLA+還引入了一些新的操作符，最重要的就是“□”和“◇”?！啊酢北硎尽癮lways”，即對任意狀態(tài)P，時序公式“□P”表示狀態(tài)P會一直持續(xù)下去?！啊蟆北硎尽癳ventually”，即對任意狀態(tài)P，時序公式“◇P”表示狀態(tài)P最終總會出現(xiàn)。需要注意的是，如果P表示的是一個動作，有時也會用這種表示方法來表明系統(tǒng)特性，這時需要改變書寫方式，記為□〈P〉vars 或者◇〈P〉vars，下標(biāo)表示在動作P中變量vars可以保持不變。持續(xù)性制約條件描述的是系統(tǒng)中確定會發(fā)生的事，是在任意一個時刻都不會違背的系統(tǒng)特性，分為較弱的制約條件（WF）以及較強的制約條件（SF）。例如

作為持續(xù)性條件時，表示在以后的狀態(tài)變化中，只要動作A的激活條件能夠滿足，則動作A在系統(tǒng)的行為中就必然會出現(xiàn)。如果A不斷地被激活，就會有無限多的A出現(xiàn)在系統(tǒng)中。

TLA+中行為的真假通過時序公式來表示，時序公式F會給行為σ賦一個布爾值，記作Fσ■。當(dāng)且僅當(dāng)上式為真時，認(rèn)為行為σ滿足公式F。通常按式（2）定義一個系統(tǒng)

其中，Init是系統(tǒng)的初始狀態(tài)謂詞，表征了系統(tǒng)最開始的一些性質(zhì)?！酰跱ext］vars 表示系統(tǒng)的狀態(tài)轉(zhuǎn)換關(guān)系，Next表示一個轉(zhuǎn)換動作，下標(biāo)vars表示在2個相鄰的狀態(tài)之間，部分變量的值可以保持不變。Liveness是持續(xù)性限制條件，表述了系統(tǒng)在以后的狀態(tài)轉(zhuǎn)變中確定會出現(xiàn)的情況。這3部分組合在一起，就是對一個系統(tǒng)的完整定義。

在使用TLC檢測器驗證模型之前，可以選擇使用初始謂詞和狀態(tài)轉(zhuǎn)換關(guān)系來描述系統(tǒng)規(guī)范，也可以直接使用表述系統(tǒng)行為的時序公式來描述，如圖1所示。

此外，執(zhí)行模型檢測的一些附加檢測條件也可以進行選擇，可以分別對規(guī)范中的系統(tǒng)性質(zhì)（property）、類型不變量（typeInvariant）以及是否存在死循環(huán)（deadlock）等進行檢測，如圖2所示。

圖1 規(guī)范行為的描述方式

圖2 TLC檢測內(nèi)容

死循環(huán)檢測可以對系統(tǒng)規(guī)范的狀態(tài)轉(zhuǎn)換流程做出檢測，驗證系統(tǒng)是否存在執(zhí)行隱患。類型不變量檢測主要是確保系統(tǒng)中某些屬性不被更改，可以檢測系統(tǒng)抵御惡意篡改風(fēng)險的能力。系統(tǒng)性質(zhì)檢測側(cè)重系統(tǒng)的功能驗證，可以檢查規(guī)范中定義或者描述的功能最終能否正常實現(xiàn)。三者可以同時選擇，對系統(tǒng)規(guī)范做出比較全面的檢測，也可以指定檢測某一項，針對系統(tǒng)規(guī)范的某一方面做出更有針對性的驗證。當(dāng)TLC工具在驗證規(guī)范的過程中發(fā)現(xiàn)有漏洞隱患存在時，就會以錯誤路徑的方式自動化給出一條反例，指出錯誤路徑中所列出的一系列狀態(tài)轉(zhuǎn)換，最終可以導(dǎo)致對系統(tǒng)規(guī)范待驗證性質(zhì)的違背。TLC工具尋找錯誤路徑是自動進行的，而且只提供一個狀態(tài)轉(zhuǎn)換最少的路徑。

3 軟硬件協(xié)同工作過程及其TLA建模

從計算機上電到完全進入操作系統(tǒng)是一個十分復(fù)雜的過程，在這個過程中，計算機首先會初始化固件的運行環(huán)境，包括CMOS芯片、處理器、芯片組、隨機存儲器RAM等。TLA+形式模型具有較強的針對性和可擴充性。利用這一特點，可以將上述部件內(nèi)部的相關(guān)操作抽象為某一個具體的狀態(tài)，而不用將其所有的工作機制都寫入規(guī)范［14］。例如，大多數(shù)計算機在上電之后執(zhí)行的第一條指令都會是JMP命令，用來將指令指針指向Flash芯片從而執(zhí)行固件代碼，本文不會描述這種相關(guān)性不大的底層細(xì)節(jié)，由于研究的重心是計算機固件及其同硬件的交互，因此，針對其他部件的一些工作原理本文進行了有保留的抽象。

3.1 軟硬件協(xié)同工作過程

圖3 軟硬件協(xié)同工作流程

如圖3所示，本文定義了從計算機上電開始到操作系統(tǒng)完全啟動過程中軟硬件協(xié)同工作的幾個關(guān)鍵步驟。計算機剛上電時，固件代碼執(zhí)行的第一個工作通常是初始化CPU及檢查當(dāng)前微碼（Microcode）文件寄存器中的內(nèi)容是否支持當(dāng)前處理器的具體型號。不匹配的處理器在實際工作過程中往往會產(chǎn)生許多問題，如發(fā)熱量過大、系統(tǒng)頻繁出現(xiàn)故障等，微碼文件的擴充通常需要通過固件更新來實現(xiàn)。接下來是芯片組的初始化，為后續(xù)執(zhí)行過程準(zhǔn)備相關(guān)寄存器等硬件資源。之后固件會分析CMOS中保存的信息，對重啟原因進行檢查，判斷上次系統(tǒng)結(jié)束運行時是正常關(guān)機操作，還是其他原因?qū)е庐惓ｊP(guān)機。如果是正常開機，就按照正常開機流程直接執(zhí)行后續(xù)步驟，反之，則有相應(yīng)的分支處理流程，這個階段叫做軟重啟（soft reboot）判斷。軟重啟判斷結(jié)束之后，如果確定執(zhí)行的是軟重啟，則進行相應(yīng)的軟重啟原因排查。導(dǎo)致系統(tǒng)執(zhí)行軟重啟的原因很多，系統(tǒng)更新、固件更新、新硬件的發(fā)現(xiàn)和驅(qū)動安裝以及某些底層軟件的更新都有可能導(dǎo)致操作系統(tǒng)執(zhí)行軟重啟。由于研究的對象是計算機固件，因此本文將操作系統(tǒng)更新以及后續(xù)操作抽象為一個狀態(tài)，將硬件改動和驅(qū)動程序更新同樣也抽象為一個狀態(tài)。如果確定軟重啟的原因是固件更新，系統(tǒng)還會進一步執(zhí)行判斷，檢查執(zhí)行更新操作的條件是否滿足，最主要的是對固件存儲芯片F(xiàn)lash進行可寫標(biāo)志檢查和對固件更新文件執(zhí)行合法性檢查［15］。前者是針對更新操作的合法性，后者是針對更新文件的安全性。執(zhí)行更新需要這2個條件同時滿足，任意一個條件不滿足時都會導(dǎo)致固件更新失敗，直接進入操作系統(tǒng)。

3.2 軟硬件協(xié)同工作過程建模

通過前文對計算機固件更新過程的描述，本文從中抽象出了幾個關(guān)鍵的動作，包括判斷微碼文件合法性的CheckMicrocode，判斷本次啟動是否為軟重啟的IsSoftReboot以及判斷軟重啟原因的IsFirmwareUpdate、IsOSUpdate和IsDriverUpdate等，還有檢查更新條件是否滿足的UpdateCheck，最后是固件更新執(zhí)行結(jié)束后反映系統(tǒng)狀態(tài)的EnterOS等。

在對固件系統(tǒng)特性進行抽象的過程中，用到了幾個變量，這些變量同樣也是系統(tǒng)運行過程中各組件間實現(xiàn)通信的媒介。在描述微碼文件合法性判定時，用Microcode_verification_sign作為標(biāo)志位同CPU型號進行比較。在描述軟重啟判定條件時，用Soft_reboot_sign表示判定標(biāo)志位。同樣地，用Reboot_reason_sign表示軟重啟的原因。在判定固件更新是否執(zhí)行時，用Write_flash_sign變量和Update_verification_sign變量分別表示Flash芯片的可寫標(biāo)志位和固件更新文件的安全性檢驗標(biāo)志位。用Firmware_security_data表示固件更新文件中經(jīng)過改動后的安全相關(guān)內(nèi)容，可以看作是固件版本，System_security_data表征系統(tǒng)中當(dāng)前固件的版本情況。沒有更新時，令這2個變量取值相等，表示固件文件的版本和系統(tǒng)中存在的固件版本相同。用這2個變量的不同作為判斷系統(tǒng)中是否存在待更新固件文件的依據(jù)，進而，可以通過判定這2個變量的值來觀察系統(tǒng)當(dāng)前的狀態(tài)，判斷系統(tǒng)是否成功執(zhí)行了更新。為了更加抽象地表示固件內(nèi)容和固件更新的執(zhí)行情況，本文引入了3個常量OldFirm、NewFirm、AtkFirm。用OldFirm表示更新之前的固件版本、NewFirm表示正常更新過程中更新文件的固件版本、AtkFirm表示經(jīng)過篡改的固件版本。

系統(tǒng)的初始狀態(tài)定義為

由于TLA+語言中沒有明確定義數(shù)據(jù)類型，在給變量賦值的時候只會檢查形式上有無語法錯誤，并不會對賦值的合法性做出檢查，因此，用TypeInvariant將變量類型以系統(tǒng)性質(zhì)的形式固定下來，具體形式如下。

式（4）一方面可以將變量的取值類型固化，防止出現(xiàn)邏輯錯誤，另一方面可以便于變量的添加和引用等操作。這樣的類型不變定義叫做一個記錄（record），之后對變量進行操作時，只需要通過類似Varset.Soft_reboot_sign的形式引用就可以了。

狀態(tài)轉(zhuǎn)換關(guān)系需要包含各個階段的TLA+公式，每一個階段都需要詳細(xì)定義，包括其觸發(fā)激活條件、判斷語句以及對狀態(tài)變量值采取的相關(guān)操作，然后，采用邏輯操作符“∨”來連接每一種可能的操作［16］。

式（5）將固件系統(tǒng)從開機上電到完全進入操作系統(tǒng)的關(guān)鍵步驟用TLA+語言做了抽象，其含義是，在任意時刻，上述幾個動作都有可能發(fā)生。TLA+定義的只是系統(tǒng)中可能發(fā)生的所有動作，在定義狀態(tài)轉(zhuǎn)換關(guān)系Next的時候并不會規(guī)定各個動作發(fā)生的先后順序，能夠表明動作之間執(zhí)行順序的語句只會在各個動作的詳細(xì)定義中，以觸發(fā)激活條件的形式給出。這樣TLC工具在對規(guī)范做完整性驗證的時候，會根據(jù)列出的動作激活條件以及下一步的具體操作，生成一個完整的狀態(tài)執(zhí)行流程。

在描述持續(xù)性條件時，考慮到實際系統(tǒng)運行過程中會有其他不可測情況的出現(xiàn)，如各種分支情況，本文采用弱持續(xù)性條件作為約束

式（6）表明只有動作Next被永久激活，即Next動作的激活條件總能被滿足時，動作Next才肯定會出現(xiàn)，而非強持續(xù)條件所描述的，只要Next動作的激活條件出現(xiàn)，Next就一定會執(zhí)行。通過這種定義，在模型實際執(zhí)行的過程中加入了對容錯的支持。

最后，綜合上面的工作，給出了系統(tǒng)規(guī)范的完整定義式

和其中，式（7）是基于TLA+形式語言給出的一個固件系統(tǒng)完整定義，涵蓋了第3.1節(jié)中描述的系統(tǒng)架構(gòu)和軟硬件工作過程。式（8）則是將系統(tǒng)規(guī)范的特性以性質(zhì)的形式給出，其含義是，無論在哪種情況下，系統(tǒng)的運行始終不會違背類型不變定義，所有的變量都會在給定的初始范圍內(nèi)取值。另外，隨著狀態(tài)的推移，系統(tǒng)最終總會停留在EnterOS上，因為這個動作意味著固件執(zhí)行階段的結(jié)束，計算機最終進入操作系統(tǒng)啟動階段。

4 攻擊模型的建立以及TLC驗證結(jié)論

本文的第3節(jié)對固件本身及其同硬件的交互過程做出了形式化建模，按照第3.1節(jié)中介紹的工作過程進行了詳細(xì)的分步描述，得到了一個固件執(zhí)行系統(tǒng)規(guī)范，給出了初始狀態(tài)謂詞、狀態(tài)轉(zhuǎn)換關(guān)系以及持續(xù)性條件的詳細(xì)定義。在此基礎(chǔ)之上，本文對固件更新過程的安全性進行了研究。

4.1 攻擊模型Attack

系統(tǒng)規(guī)范的漏洞檢查并不等同于對其進行正確性驗證，因為正確性驗證所做的工作是檢查模型能否嚴(yán)格按照規(guī)范中定義的流程執(zhí)行，檢驗的是系統(tǒng)中定義的性質(zhì)最終能否實現(xiàn)。而漏洞檢查則不同，這種情況下，一般會假設(shè)系統(tǒng)規(guī)范在理想環(huán)境下是正確的，關(guān)注的重點是系統(tǒng)在受到攻擊的時候會不會存在安全隱患。因此，要做漏洞檢查分析，還需要將攻擊者也用模型化的方法加入系統(tǒng)規(guī)范中［17］。

在軟硬件結(jié)合的背景下，給出漏洞的定義。漏洞是一種特殊的狀態(tài)元素（配置寄存器）和控制信號的組合，這種組合會導(dǎo)致對信息安全目標(biāo)的違背或者會導(dǎo)致繞開信息安全的保護機制。具體到固件和硬件的協(xié)同工作過程中，漏洞就是固件發(fā)出某種非正常的操作指令，可以控制計算機某些寄存器的配置，進而影響硬件特定行為方式的判定，導(dǎo)致固件中某些重要的數(shù)據(jù)或工作方式存在被惡意修改的可能。

用TLA+語言定義攻擊者模型的時候，由于形式語言的抽象性，可以將多種攻擊能力同時合并到攻擊模型中，然后檢查系統(tǒng)的安全性。顯然在攻擊能力足夠強的時候系統(tǒng)必然會出現(xiàn)一些安全問題，但是這種情況下產(chǎn)生的許多問題都是在非正常假設(shè)條件下所得到的結(jié)果，即攻擊者的能力可以任意配置且沒有任何限制，因此，生成的錯誤路徑并非一定具有實際可行性，所以，合理地選擇攻擊模型的特權(quán)以及能力就顯得尤為重要。

一個比較有效的研究方法是按照從強到弱動態(tài)調(diào)節(jié)攻擊者能力，當(dāng)攻擊者能力過強，甚至已經(jīng)與實際情況相違背時，TLC驗證工具必然會提供一些錯誤路徑，對這些路徑需要加以判斷，如果確定是不可行的，可以動態(tài)地修改規(guī)范中攻擊模型的權(quán)限及能力，然后加載到TLC工具中重新進行驗證，直到發(fā)現(xiàn)實際可行的漏洞，如圖4所示。

圖4 研究方法改進過程

基于這一思想，首先，確定了一個最強的攻擊模型，即該模型擁有直接修改固件內(nèi)容的權(quán)限，但此時TLC工具給出的錯誤路徑經(jīng)分析后并不能被實際使用，因為Flash芯片的修改還涉及到一些判定機制，想要修改其內(nèi)容必須符合之前所述的幾個條件；之后，在攻擊模型中添加了一個判定條件，發(fā)現(xiàn)TLC同樣不會提供錯誤路徑，這是因為在這種條件下攻擊模型沒有足夠的權(quán)限對Flash芯片進行修改，并非規(guī)范中不存在漏洞。通過動態(tài)調(diào)整，最終確定的攻擊者模型公式如下。

式（9）表明，本文所定義的攻擊者，能夠更改Flash芯片的可寫標(biāo)志位，使攻擊者有可能修改固件存儲芯片F(xiàn)lash中的內(nèi)容，滿足了固件執(zhí)行更新判定過程中的第1個條件。同時，該模型能夠滿足更新文件合法性驗證的要求，即滿足了第2個條件。另外，要求攻擊者能夠修改計算機中的固件內(nèi)容，為了區(qū)別計算機中原有的固件版本OldFirm和合法更新文件中的版本NewFirm，標(biāo)記修改后的新固件為AtkFirm。

4.2 TLC檢測結(jié)果

為了查找固件系統(tǒng)規(guī)范中的漏洞，強調(diào)其內(nèi)容不可隨意更改，結(jié)合前述攻擊者模型，本文在規(guī)范中加入了一個針對固件中同安全性內(nèi)容相關(guān)的系統(tǒng)性質(zhì)，強調(diào)更新后的固件版本不能為AtkFirm，即

這樣，TLC工具在執(zhí)行驗證的時候，就會基于此性質(zhì)自動化地尋找錯誤路徑，結(jié)果如圖5所示。

圖5 錯誤路徑

圖5中的錯誤路徑一共包含6個狀態(tài)，詳細(xì)列出了系統(tǒng)規(guī)范中可能存在安全風(fēng)險的狀態(tài)轉(zhuǎn)換方式。結(jié)合系統(tǒng)規(guī)范和攻擊者模型分析該錯誤路徑可知，TLC工具提供了一個潛在的軟硬件協(xié)同工作漏洞，即如果攻擊者具備修改Flash芯片可寫標(biāo)志的能力，同時自身又滿足更新文件安全性的要求，那么這種情況下計算機固件的更新過程存在安全隱患。

5 錯誤路徑實現(xiàn)及分析

根據(jù)TLA模型以及TLC驗證工具得到的結(jié)果，本文選取計算機的固件更新文件作為攻擊載體。之所以選擇固件更新文件，是因為它本身就已經(jīng)滿足前述2個判定條件的要求。第3個條件要求攻擊者能夠加載區(qū)別于系統(tǒng)中現(xiàn)有內(nèi)容的新固件文件，可以通過修改固件更新文件中的內(nèi)容，然后執(zhí)行更新來實現(xiàn)。在實際研究過程中發(fā)現(xiàn)，在固件更新過程中，并不能夠保證更新文件中所有模塊的合法性，其驗證過程更多是側(cè)重廠商號、版本號以及對硬件設(shè)備兼容性上，即使存在對更新文件完整性的驗證，也很難對封裝在文件內(nèi)部的一些模塊進行深入檢查，其中最重要的就是PCI Expansion Rom［18］。

5.1 PCI Expansion ROM文件

PCI Expansion ROM是PCI規(guī)范中定義的一個文件［19］，允許設(shè)備通過該ROM文件的代碼執(zhí)行設(shè)備初始化操作。通常一個Expansion ROM可以包含幾個不同的image文件，以便適配不同的主板架構(gòu)和處理器架構(gòu)。每一個image都是從512 byte邊界處開始，而且必須包含PCI Expansion ROM頭文件。x86/x64架構(gòu)平臺的PCI頭文件格式如表1所示。

表1 PCI Expansion ROM頭文件格式

前2個字節(jié)是PCI Expansion ROM文件的簽名，固定為0xAA55，用于ROM文件的檢索。其中，偏移03h處是設(shè)備初始化函數(shù)的入口，固件在初始化PCI設(shè)備時會跳轉(zhuǎn)到這里將執(zhí)行權(quán)交給PCI Expansion ROM。偏移18h～19h指向PCI的數(shù)據(jù)結(jié)構(gòu)（data structure），PCI的數(shù)據(jù)結(jié)構(gòu)必須位于第一個64 kB段內(nèi)，里面包含了設(shè)備碼（device ID）和廠商碼（vendor ID）以及代碼類型等內(nèi)容。

在檢測到PCI設(shè)備需要相應(yīng)的ROM文件協(xié)助初始化之后，固件用2個步驟搜索其對應(yīng)的PCI Expansion ROM文件。首先，檢測PCI設(shè)備在配置空間里是否有可執(zhí)行的ROM文件，如果有，就將該文件映射到地址空間的一個空閑區(qū)域；然后，通過檢測雙字節(jié)“AA55h”簽名來搜索ROM文件，通過設(shè)備碼和廠商碼進行匹配，如果找到，就通過一個CALL指令跳轉(zhuǎn)到這里執(zhí)行，如果沒找到，則跳過此設(shè)備，返回固件的主線程繼續(xù)執(zhí)行［20］。

5.2 實驗結(jié)果及分析

在分析了固件的啟動流程以及TLA+模型之后，本文在x86平臺下針對常見的Award固件展開了研究。首先，使用官方備份和更新工具提取出Flash芯片中的固件文件；然后，使用CBROM工具提取出了其中的PCI網(wǎng)卡模塊，如圖6所示。

圖6中AR815x.lom文件就是此固件文件中內(nèi)置的網(wǎng)卡PCI Expansion ROM文件，其具體信息如圖7所示。

圖6 提取Award固件中網(wǎng)卡模塊的PCI Expansion ROM文件

圖7 網(wǎng)卡模塊的PCI Expansion ROM文件信息

由PCI Expansion ROM的規(guī)范可知，圖7中0018h和0019h偏移指向PCI的數(shù)據(jù)結(jié)構(gòu)，即偏移地址為0x0040。PCI數(shù)據(jù)結(jié)構(gòu)前4個字節(jié)為標(biāo)識符PCIR，偏移04h～05h即0x0044h～0x0045h為廠商的標(biāo)識碼，即Vendor ID為0x1969；偏移06h～07h為設(shè)備標(biāo)識碼，即Device ID為0x1083。

通過編譯，將一個開源的引導(dǎo)程序按照該網(wǎng)卡的設(shè)備信息封裝成PCI Expansion ROM的格式，使用CBROM工具將新的ROM文件導(dǎo)入到固件的更新文件中，替換原來的網(wǎng)卡ROM文件。然后，通過正常的固件更新操作，將修改后的更新文件注入到系統(tǒng)固件中，成功地劫持了開機引導(dǎo)過程，使計算機上電后在執(zhí)行到PCI設(shè)備初始化的時候，操作系統(tǒng)便不經(jīng)固件，而是由修改之后的PCI Expansion ROM進行引導(dǎo)，如圖8所示。

圖8 網(wǎng)卡PCI Expansion ROM引導(dǎo)進入操作系統(tǒng)

在實際的更新執(zhí)行過程中，固件系統(tǒng)本身并沒有檢測所有封裝模塊的安全性，在跳轉(zhuǎn)到PCI Expansion ROM文件執(zhí)行設(shè)備初始化的時候，也很難對代碼的行為做出合法性檢驗，從而給固件自身甚至是操作系統(tǒng)的運行環(huán)境都帶來了安全威脅。本次實驗通過修改合法的固件更新文件得到了一個符合攻擊模型形式規(guī)范的實際攻擊載體，然后按照正常的更新流程替換了網(wǎng)卡的ROM文件，這樣系統(tǒng)固件在執(zhí)行遍歷PCI設(shè)備操作的時候，發(fā)現(xiàn)網(wǎng)卡設(shè)備對應(yīng)的PCI Expansion ROM文件，于是就按照規(guī)范定義的操作將這部分代碼復(fù)制到內(nèi)存中執(zhí)行。由于此時固件尚未將控制權(quán)交給操作系統(tǒng)，因此，這時候執(zhí)行的代碼都擁有絕對的高權(quán)限［21］。

6 結(jié)束語

固件位于計算機整個體系架構(gòu)的底層，是軟硬件協(xié)同工作的保證，固件文件中潛在的安全隱患會在計算機軟件和硬件工作的過程中無限放大。在對固件安全的研究過程中，本文提出了基于軟硬件協(xié)同形式驗證的漏洞分析方法，建立了完整的軟硬件交互形式模型，使用TLC工具在固件更新過程中發(fā)現(xiàn)了漏洞，并通過實驗驗證了該漏洞的存在，證明了方法的可靠性。

同傳統(tǒng)的安全分析研究方法相比，形式驗證的方法效率更高，能夠很好地繼承和發(fā)展之前的研究成果。這種特點不僅表現(xiàn)在系統(tǒng)模型的深度和廣度上，還體現(xiàn)在攻擊模型的動態(tài)調(diào)整建立中。在今后的工作中，可以逐步擴充形式模型庫，將計算機體系中重要的組件陸續(xù)加入到形式模型庫中，由淺入深，建立更為完備的計算機系統(tǒng)形式模型，在此基礎(chǔ)上對計算機體系的安全性做出更為深入的分析。

［1］ ZIMMER V， ROTHMAN M， MARISETTY S. Beyond BIOS：developing with the unified extensible firmware interface［M］. Intel Press， 2010.

［2］ BROSSARD J， DEMETRESCU F. Hardware backdooring is practical［J］. BlackHat， Las Vegas， USA， 2009，58（1）.

［3］ RONTTI T， JUUSO A M， TAKANEN A. Preventing DoS attacks in NGN networks with proactive specification-based fuzzing［J］. IEEE Communications Magazine， 2012， 50（9）：164-170.

［4］ RUI MA， DAGUANG WANG， CHANGZHEN HU， et al. Test data generation for stateful network protocol fuzzing using a rule-based state machine［J］. Tsinghua Science and Technology， 2016， 21.

［5］ 周仕鈞. 基于二進制補丁比對技術(shù)的漏洞特征分析與研究［D］.昆明： 云南大學(xué)， 2013. ZHOU S J. Holes characteristics analysis and research based on binary patch［D］. Kunming： Yunnan University， 2013.

［6］ KIM S， KIM R Y C， PARK Y B. Software vulnerability detection methodology combined with static and dynamic analysis［J］. Wireless Personal Communications， 2015：1-17.

［7］ 鄭宇軍， 張蓓， 薛錦云. 軟件形式化開發(fā)關(guān)鍵部件選取的水波優(yōu)化方法［J］. 軟件學(xué)報， 2016（4）： 933-942. ZHENG Y J， ZHANG B， XUE J Y. Water ware optimization method of Software for multination development key components selection［J］. Journal of Software， 2016（4）： 933-942.

［8］ CALINESCU R， GHEZZI C， JOHNSON K， et al. Formal verification with confidence intervals to establish quality of service properties of software systems［J］. IEEE Transactions on Reliability， 2016，65（1）：107-125.

［9］ KUMAR S， CHANDRA G， YADAV D. Formal verification of security protocol with B method［C］// IEEE International Conference on Computer and Communication Technology. c2014：161-167.

［10］ LACH J， BINGHAM S， ELKS C， et al. Accessible formal verification for safety-critical hardware design［C］//Reliability and Maintainability Symposium， IEEE Computer Society. c2006： 29-32.

［11］ CHOI H， YIM M K， LEE J Y， et al. Formal verification of an industrial system-on-a-chip［C］// IEEE International Conference on Computer Design. c2000：453-458.

［12］ LAMPORT L. Specifying systems， the TLA+ language and tools for hardware and software engineers［J］. Software Quality Professional， 2002（4）：43.

［13］ CHAUDHURI K， DOLIGEZ D， LAMPORT L， et al. Verifying safety properties with the TLA+ proof system［M］//Automated Reasoning. Berlin Heidelberg： Springer， 2010：142-148.

［14］ LU T， MERZ S， WEIDENBACH C. Towards verification of the pastry protocol using TLA?+［C］//Formal Techniques for Distributed Systems Proceedings. c2011：244-258.

［15］ KALLENBERG C， BUTTERWORTH J， KOVAH X， et al. Defeating signed BIOS enforcement［J］. EkoParty， Buenos Aires， 2013.

［16］ ZHANG H， MERZ S， GU M. Specifying and verifying PLC systems with TLA+： a case study［J］. Computers & Mathematics with Applications， 2010， 60（3）：695-705.

［17］ NARAYANA P， CHEN R， ZHAO Y， et al. Automatic vulnerability checking of IEEE 802.16 WiMAX Protocols through TLA+［C］// IEEE Workshop on Secure Network Protocols.c2006：44-49.

［18］ HEASMAN J. Implementing and detecting a PCI rootkit［J］. Retrieved February， 2006， 20： 3.

［19］ BUDRUK R， ANDERSON D， SOLARI E. PCI express system architecture［J］. Addison Wesley， 2003.

［20］ YIN Y. Implementation of PCI expansion ROM mechanism［J］. Computer Engineering & Applications， 2005.

［21］ WOJTCZUK R， RUTKOWSKA J. Attacking SMM memory via Intel CPU cache poisoning［J］. Invisible Things Lab， 2009.

張朋輝（1989-），男，河南安陽人，國防科學(xué)技術(shù)大學(xué)碩士生，主要研究方向為專用集成電路可信性設(shè)計、硬件安全性分析。

田曦（1971-），男，湖南長沙人，博士，國防科學(xué)技術(shù)大學(xué)副教授、碩士生導(dǎo)師，主要研究方向為信息安全、可信性設(shè)計。

樓康威（1992-），男，浙江金華人，國防科學(xué)技術(shù)大學(xué)碩士生，主要研究方向為專用集成電路可信性設(shè)計、電子信息系統(tǒng)信號安全分析。

Firmware vulnerability analysis based on formal verification of software and hardware

ZHANG Peng-hui， TIAN-Xi， LOU Kang-wei
（School of Electronic Science and Engineering， National University of Defense Technology， Changsha 410003， China）

In order to analyze the potential vulnerabilities in the firmware systematically and effectively， a formal verification method based on TLA， in a collaborated form of software and hardware was proposed. With this method，the interaction mechanism of software and hardware in the computer boot process was modeled and analyzed. By adjusting the attack model， a secure vulnerability in the update process of the firmware was found， and its existence by an experiment， which proved the reliability of formal verification was demonstrated.

firmware security， TLA， formal verification， vulnerability analysis， software and hardware collaboration

1 引言

固件（firmware）是計算機上電后最先執(zhí)行的代碼，主要負(fù)責(zé)系統(tǒng)硬件平臺的初始化及加載操作系統(tǒng)，并最終將控制權(quán)傳遞給它。早期的固件版本叫作基本輸入輸出系統(tǒng)（BIOS， basic input output system），由于其開發(fā)效率低，功能擴展性差以及更新機制不完善等缺點，已經(jīng)逐漸被支持圖形界面和鼠標(biāo)操作的統(tǒng)一可擴展固件接口（UEFI， unified extensible firmware interface）所取代［1］。UEFI在充分集成BIOS功能的基礎(chǔ)上添加了許多新特性，如完全使用C語言開發(fā)、更新機制簡單快速以及方便跨平臺移植等。固件常駐在主板上的Flash芯片中，即使在重裝操作系統(tǒng)后依然不受影響。由于固件對計算機的安全至關(guān)重要，固件廠商以及芯片公司均提供了專門的機制來保護其內(nèi)容免受干擾，但是當(dāng)遇到需要修復(fù)固件漏洞或者添加一些新功能的情況時，又必須有一種可靠的方案來對其進行更新，這種機制一定程度上給固件內(nèi)容的安全帶來了風(fēng)險。一旦固件的代碼受到感染，系統(tǒng)啟動過程中的其他組件也會受到安全威脅，因此，Brossard等［2］指出，只要取得了固件代碼的控制權(quán)，任意控制計算機的行為就成為了可能。

The National High Technology Research and Development Program （No.2015AA2557）

TP309

A

10.11959/j.issn.2096-109x.2016.00071

2016-05-22；

2016-06-27。通信作者：張朋輝，zph.111@163.com

國家高技術(shù)研究發(fā)展計劃基金資助項目（No.2015AA2557）