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

張朋輝，田曦，樓康威

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

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

張朋輝，田曦，樓康威

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

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

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

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

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

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

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

2 行為時(shí)序邏輯TLA以及其TLC工具

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.1 攻擊模型Attack

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

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

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

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

圖4 研究方法改進(jìn)過(guò)程

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

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

4.2 TLC檢測(cè)結(jié)果

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

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

圖5 錯(cuò)誤路徑

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

5 錯(cuò)誤路徑實(shí)現(xiàn)及分析

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

5.1 PCI Expansion ROM文件

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

表1 PCI Expansion ROM頭文件格式

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

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

5.2 實(shí)驗(yàn)結(jié)果及分析

在分析了固件的啟動(dòng)流程以及TLA+模型之后，本文在x86平臺(tái)下針對(duì)常見(jiàn)的Award固件展開(kāi)了研究。首先，使用官方備份和更新工具提取出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個(gè)字節(jié)為標(biāo)識(shí)符PCIR，偏移04h～05h即0x0044h～0x0045h為廠商的標(biāo)識(shí)碼，即Vendor ID為0x1969；偏移06h～07h為設(shè)備標(biāo)識(shí)碼，即Device ID為0x1083。

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

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

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

6 結(jié)束語(yǔ)

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

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

［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］ 周仕鈞. 基于二進(jìn)制補(bǔ)丁比對(duì)技術(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］ 鄭宇軍， 張蓓， 薛錦云. 軟件形式化開(kāi)發(fā)關(guān)鍵部件選取的水波優(yōu)化方法［J］. 軟件學(xué)報(bào)， 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-），男，河南安陽(yáng)人，國(guó)防科學(xué)技術(shù)大學(xué)碩士生，主要研究方向?yàn)閷Ｓ眉呻娐房尚判栽O(shè)計(jì)、硬件安全性分析。

田曦（1971-），男，湖南長(zhǎng)沙人，博士，國(guó)防科學(xué)技術(shù)大學(xué)副教授、碩士生導(dǎo)師，主要研究方向?yàn)樾畔踩⒖尚判栽O(shè)計(jì)。

樓康威（1992-），男，浙江金華人，國(guó)防科學(xué)技術(shù)大學(xué)碩士生，主要研究方向?yàn)閷Ｓ眉呻娐房尚判栽O(shè)計(jì)、電子信息系統(tǒng)信號(hào)安全分析。

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

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

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