針對硬件木馬的形式化驗(yàn)證模型構(gòu)造方法

沈利香，慕德俊，曹 國，謝光前，束方勇

(1.西北工業(yè)大學(xué) 自動化學(xué)院，陜西 西安 710072；2.常州工學(xué)院 計(jì)算機(jī)信息工程學(xué)院，江蘇 常州 213032；3.西北工業(yè)大學(xué) 網(wǎng)絡(luò)空間安全學(xué)院，陜西 西安 710072；4.西北工業(yè)大學(xué) 管理學(xué)院，陜西 西安 710072；5.常州工學(xué)院 經(jīng)濟(jì)與管理學(xué)院，江蘇 常州 213032)

伴隨著集成電路供應(yīng)鏈的全球化，硬件安全正越來越成為硬件設(shè)計(jì)中的一個巨大挑戰(zhàn)。硬件安全漏洞會威脅電路的安全屬性，包括保密性，完整性和有效性等。硬件木馬是硬件安全中的一個主要問題。文獻(xiàn)[1]指出硬件木馬威脅了整個集成電路市場。當(dāng)植入木馬的芯片被用到各種系統(tǒng)時，硬件木馬會導(dǎo)致嚴(yán)重的安全問題和經(jīng)濟(jì)損失，甚至是人身傷害。例如，2010年Stuxnet蠕蟲使可編程邏輯控制器偏離了預(yù)定義行為，嚴(yán)重?fù)p害了伊朗核電站的離心機(jī)。

形式化驗(yàn)證是一種基于算法的驗(yàn)證方法，與仿真測試相比驗(yàn)證更加完備，但也更加耗時。形式化驗(yàn)證技術(shù)主要包含了定理證明和模型檢測。在定理證明方面，JIN等使用定理證明技術(shù)驗(yàn)證Verilog代碼安全。在文獻(xiàn)[2-3]中，提出了一種測試框架。該框架結(jié)合了定理證明和信息流追蹤技術(shù)[4-5]。文獻(xiàn)[6]首先針對門級電路構(gòu)造電路語義模型，然后定義驗(yàn)證定理，以人機(jī)交互方式利用定理證明器驗(yàn)證定理的合理性，從而確定門級電路的安全性。在模型檢測方面，該技術(shù)窮舉式地遍歷驗(yàn)證模型的狀態(tài)空間，以驗(yàn)證測試電路的各種屬性。與定理證明相比，模型檢測不需要證明，驗(yàn)證速度更快，這使得它比定理證明更為實(shí)用。此外，模型檢測能夠產(chǎn)生反例，反例能夠揭示出驗(yàn)證屬性是如何產(chǎn)生結(jié)果“假”的原因與過程。至今，模型檢測已經(jīng)成功地用于解決很多實(shí)際問題，例如硬件驗(yàn)證、通信協(xié)議分析、安全分析[7]等。在硬件驗(yàn)證方面，現(xiàn)有的相關(guān)文獻(xiàn)主要針對門級網(wǎng)表建模，針對寄存器傳輸級(Register Transfer Level，RTL)建模的研究較少。但是，由于門級網(wǎng)表的復(fù)雜性，依據(jù)門級網(wǎng)表構(gòu)成的形式化驗(yàn)證模型復(fù)雜度高，使得形式化驗(yàn)證的效率不高。相對門級網(wǎng)表，寄存器傳輸級的硬件設(shè)計(jì)要精簡很多。文獻(xiàn)[8]提出了一種針對寄存器傳輸級代碼的硬件驗(yàn)證方法。首先，寄存器傳輸級的Verilog代碼轉(zhuǎn)換為C語言代碼，這種轉(zhuǎn)換需要保持C語言代碼與Verilog代碼之間的等價(jià)性。然后對C語言代碼進(jìn)行模型檢測。由于C語言本身不具有時序特性，這種轉(zhuǎn)換對保持Verilog設(shè)計(jì)的等價(jià)性會有影響。工具Verilog2SMV[9]對開源綜合器Yosys[10]進(jìn)行了擴(kuò)展，可以將Verilog代碼轉(zhuǎn)換為符號模型驗(yàn)證模型，利用符號模型檢測器NuXMV驗(yàn)證生成的模型是否滿足設(shè)計(jì)屬性。由Verilog2SMV構(gòu)造的模型，其可讀性和可重用性都較差，測試人員不易根據(jù)自己的需要進(jìn)行靈活的更改。

為了直接檢測待驗(yàn)證設(shè)計(jì)中的硬件木馬，提高驗(yàn)證模型的可讀性、可重用性和驗(yàn)證效率，提出了一種自動構(gòu)造形式化驗(yàn)證模型的方法。首先生成待驗(yàn)證設(shè)計(jì)中每個變量的<路徑條件，表達(dá)式>對以確定約束關(guān)系，其中路徑條件表示Verilog語句執(zhí)行對應(yīng)的條件，表達(dá)式表示路徑條件對應(yīng)的變量賦值的表達(dá)式。然后，<路徑條件，表達(dá)式>對用來確定有限狀態(tài)機(jī)Kripke結(jié)構(gòu)中的狀態(tài)轉(zhuǎn)移關(guān)系，構(gòu)造寄存器傳輸級的形式化驗(yàn)證模型。最后，定義安全驗(yàn)證屬性，使用符號模型檢測器NuSMV[11]遍歷狀態(tài)空間驗(yàn)證構(gòu)造的形式化驗(yàn)證模型。當(dāng)驗(yàn)證結(jié)果為假時，硬件木馬或者其觸發(fā)器會通過反例暴露出來。實(shí)驗(yàn)使用了標(biāo)準(zhǔn)測試集Trust-HUB[12-13]檢測硬件木馬。

1 寄存器傳輸級設(shè)計(jì)的形式化驗(yàn)證模型構(gòu)造

模型檢測用于有限狀態(tài)機(jī)建模，有限狀態(tài)系統(tǒng)用Kripke結(jié)構(gòu)定義：M=(S，S0，R，L)[14]，其中S表示有限狀態(tài)機(jī)的狀態(tài)集合，S0表示一個初始狀態(tài)集合，R表示狀態(tài)轉(zhuǎn)移關(guān)系，L表示包含原子屬性集合的標(biāo)簽函數(shù)。符號模型檢測[14]用符號表達(dá)狀態(tài)轉(zhuǎn)移關(guān)系，采用有序二元決策圖(Ordered Binary Decision Diagram，OBDD)對整個驗(yàn)證模型的狀態(tài)空間進(jìn)行遍歷驗(yàn)證，大大提高了驗(yàn)證效率，是一種有效的模型檢測優(yōu)化技術(shù)。

圖1提出的自動化構(gòu)造方法，圍繞Kripke結(jié)構(gòu)中的狀態(tài)轉(zhuǎn)移關(guān)系R進(jìn)行形式化驗(yàn)證模型構(gòu)造。該方法不需要黃金模板，形式化驗(yàn)證時也不需要設(shè)定測試向量，符號模型檢測會根據(jù)模型的狀態(tài)空間自動進(jìn)行遍歷搜索。因?yàn)榉抡鏈y試的速度比形式化驗(yàn)證快，待驗(yàn)證的硬件設(shè)計(jì)應(yīng)該首先通過基本的功能測試，以減少整體的驗(yàn)證時間。構(gòu)造形式化驗(yàn)證模型的目的是從反例中檢測到難以被仿真測試發(fā)現(xiàn)的硬件木馬。方法的整體思路如圖1所示。首先，為了獲取到硬件設(shè)計(jì)中的約束關(guān)系，采用深度優(yōu)先遍歷Verilog設(shè)計(jì)的控制流圖，生成每個節(jié)點(diǎn)的路徑條件。算法1描述了此過程。

算法1GeneratePcExp

輸入(控制流圖CFG)。

輸出(variablePcExpList)。

node←CFG.root；

While(深度遍歷控制流圖CFG沒有結(jié)束 ) {

node←后繼未訪問節(jié)點(diǎn)node；

controlNode←node.getControlNode；

switch(node.Type) {

case ALWAYS：節(jié)點(diǎn)的路徑條件列表node.pclist←always敏感列表?xiàng)l件； break；

case IF：node.pclist←控制節(jié)點(diǎn)的路徑條件列表controlNode.pclist&node的語句條件；break；

case ELSE：lastpc←"!("+controlNode.pclist中的最后一項(xiàng)+ ")"；

刪除controlNode.pclist中的最后一項(xiàng)；添加最后一項(xiàng)lastpc到controlNode.pclist； break

case CASE：node.pcllist←controlNode.pclist； break；

case CASE_ITME：

if (node是“default”)node.pclist←controlNode.pclist& default的路徑條件；

elsenode.pclist←controlNode.pclist&node的語句條件； break；

case ASSIGN_CONTIUNE：

case ASSIGN_NONBLOCK：

case ASSIGN_BLOCK：node.pclist←controlNode.pclist；pc←node.pclist；

exp←node的賦值表達(dá)式；variablePcExpList←； break；

default：node.pclist←controlNode.pclist； break；

} }。

對于一個Verilog的賦值語句，每個路徑條件都有對應(yīng)的一個表達(dá)式，即<路徑條件，表達(dá)式>對。遍歷結(jié)束后，每個賦值表達(dá)式的左邊變量會擁有一個或者多個<路徑條件，表達(dá)式>對。路徑條件實(shí)際為約束條件，表達(dá)式則為約束條件下的狀態(tài)轉(zhuǎn)移。具有約束關(guān)系的<路徑條件，表達(dá)式>對構(gòu)成了一種狀態(tài)轉(zhuǎn)移關(guān)系。約束關(guān)系的集合，構(gòu)成了Kripke結(jié)構(gòu)中整個模型的狀態(tài)轉(zhuǎn)移關(guān)系。狀態(tài)轉(zhuǎn)移關(guān)系是驗(yàn)證模型中最為核心的內(nèi)容，因此，可以依據(jù)<路徑條件，表達(dá)式>集合構(gòu)造形式化驗(yàn)證模型。

算法2verilogToSmv

輸入(variablePcExpList)。

輸出(形式化驗(yàn)證模型文件smv_file)。

VAR_variables←reg and wire 類型變量；

DEFINE_identifiers←parameter類型；

sub-modules←例化模塊module_instantiations；

for (每一個在列表variablePcExpList中的變量variable)

{ if (是連續(xù)賦值語句中的variable)

{ if (賦值語句中有“?：” 操作符 )nusmv_string←nusmv_string+construct_case_body()；

elsenusmv_string←variable+"：="+ expVerilog2Smv(exp) +"；"； }

if (是組合邏輯中的variable)

{ if (是阻塞賦值 )nusmv_string←nusmv_string+"variable：=case"；

else if (exp中的變量right_variables在同一個always中被賦值)

nusmv_string←nusmv_string+“next(variable)：=case”；

else nusmv_string←nusmv_string+“variable ：=case”； }

else { if (是非阻塞賦值 )nusmv_string←nusmv_string+“next(variable) ：=case”；

else if (exp中的right_variables在同一個always中被賦值)

nusmv_string←nusmv_string+"variable：=case"；

elsenusmv_string←nusmv_string+"next(variable) ：=case"； }

nusmv_string←nusmv_string+construct_case_body()； }

smv_file←nusmv_string。

算法2表明了基于此集合的形式化驗(yàn)證模型構(gòu)造方法。然后，可以依據(jù)待驗(yàn)證設(shè)計(jì)的規(guī)范定義安全驗(yàn)證屬性p。最后，利用符號模型檢測器NuSMV驗(yàn)證形式化驗(yàn)證模型是否滿足屬性p。如果驗(yàn)證結(jié)果為假，則產(chǎn)生一個反例，從反例中可以揭露出硬件設(shè)計(jì)中的硬件木馬或者其觸發(fā)器。

1.1 NuSMV的輸入語言和形式化驗(yàn)證模型

NuSMV的輸入語言提供了常量表達(dá)式、基本表達(dá)式、簡單表述式和next表達(dá)式。這些表達(dá)式用于形式化驗(yàn)證模型的聲明(declarations)定義和約束(constraints)定義。自動構(gòu)造方法將可綜合的寄存器傳輸級Verilog代碼轉(zhuǎn)換為聲明定義和約束定義，從而將Verilog代碼轉(zhuǎn)換為形式化驗(yàn)證模型。與Verilog2SMV設(shè)計(jì)作為Yosys的插件不同，圖1的構(gòu)造方法直接從Verilog代碼生成形式化驗(yàn)證模型，并且生成的模型具有良好的可讀性和可重用性。

圖1 針對硬件木馬檢測的形式化驗(yàn)證模型構(gòu)造

形式化驗(yàn)證模型的構(gòu)造主要依據(jù)以下原則進(jìn)行，算法2實(shí)現(xiàn)了這些原則。

(1) Input，output，inout，reg和wire等聲明為形式化驗(yàn)證模型中的變量。例如，“reg[2：0]state”定義為“state：unsigned word[3]”；

(2) Parameter類型聲明為“DEFINE”。例如，“parameter ID=3′b000”定義為“DEFINE ID ：=0ub3_000”；

(3) 模塊語句定義為“MODULE”，例化語句定義為形式化驗(yàn)證模型中的子模塊引用。例如，模塊u_xmit對應(yīng)的例化語句“u_xmitiXMIT(.sys_clk(sys_clk)，.sys_rst_l(sys_rst_l)，…)”定義為“iXMIT：u_xmit(sys_clk，sys_rst_l，…)”；

1.2 從寄存器傳輸級Verilog代碼提取<路徑條件，表達(dá)式>對

針對可綜合Verilog語法，從控制流圖構(gòu)造<路徑條件，表達(dá)式>集合。圖2是對應(yīng)于表1的控制流圖，文獻(xiàn)[15]描述了控制流圖的詳情。

圖2 表1中寄存器傳輸級Verilog代碼對應(yīng)的控制流圖

控制流圖中，節(jié)點(diǎn)名稱的格式是“NodeType_LineNo”，即節(jié)點(diǎn)類型_行數(shù)。例如，名稱為“ASSIGN_BLOCK_77”的節(jié)點(diǎn)表示一個阻塞賦值語句；該語句的位置在Verilog模塊文件中的第77行，如表1所示。

表1 寄存器傳輸級Verilog 代碼

如圖2所示，表1中第77行語句的路徑條件是“cond_1&cond_2”，第80行是 “cond_1&！cond_2”。cond_1是“(posedgesys_clkor negedgesys_rst_l)”，而cond_2是“(～sys_rst_l)”。算法1生成了控制流圖中所有賦值節(jié)點(diǎn)的<路徑條件，表達(dá)式>對，算法1輸出變量variablePcExpList包含了<路徑條件，表達(dá)式>集合。首先，采用深度優(yōu)先遍歷從控制流圖中選取未被訪問的節(jié)點(diǎn)node(算法1第3行)。然后(算法1第4行)依據(jù)節(jié)點(diǎn)node的前驅(qū)關(guān)系確定其控制節(jié)點(diǎn)controlNode。ControlNode代表的是非賦值語句，包括 ALWAYS，IF，ELSE，CASE，CASE_ITEM等語句。例如，表1第76行的if語句是第77行阻塞賦值語句和第79行else語句的控制節(jié)點(diǎn)。算法1的第6至12行處理了控制節(jié)點(diǎn)的路徑條件。由控制流圖可以確定賦值語句的路徑條件也是其控制節(jié)點(diǎn)controlNode的路徑條件(第13～17行)。

1.3 基于<路徑條件，表達(dá)式>集合確定狀態(tài)轉(zhuǎn)移關(guān)系，構(gòu)造形式化驗(yàn)證模型

算法1的輸出variablePcExpList包含了Verilog代碼中每個左邊被賦值變量的<路徑條件，表達(dá)式>對，形式化驗(yàn)證模型中的約束關(guān)系是依據(jù)<路徑條件，表達(dá)式>對實(shí)現(xiàn)的，模型的約束關(guān)系集合體現(xiàn)了整個模型的狀態(tài)轉(zhuǎn)移關(guān)系。驗(yàn)證模型中有兩類定義約束(ASSIGN)的形式：簡單表達(dá)式和next表達(dá)式。算法2(第5～7行)將Verilog代碼中的連續(xù)賦值語句轉(zhuǎn)換為簡單表達(dá)式或者next表達(dá)式。Always語句段中的左邊變量可能有多個<路徑條件，表達(dá)式>對，因?yàn)樵械腣erilog代碼中存在條件分支，例如if語句，case語句等。因此將多個<路徑條件，表達(dá)式>對轉(zhuǎn)換為形式化驗(yàn)證模型中的case語句，確定狀態(tài)轉(zhuǎn)移關(guān)系(算法2第8～14行)。另外，算法2中的函數(shù) construct_case_body實(shí)現(xiàn)構(gòu)造case語句，參數(shù)中pc表示路徑條件，exp表示表達(dá)式；函數(shù)expVerilog2Smv實(shí)現(xiàn)Verilog表達(dá)式轉(zhuǎn)換成NuSMV的輸入語言表達(dá)式。最終構(gòu)造的形式化驗(yàn)證模型，其復(fù)雜程度與原來的Verilog代碼相同。Verilog變量名稱、常量名稱、模塊例化和變量之間的約束關(guān)系等都被完整清晰地保留在形式化驗(yàn)證模型中，提高了模型的易讀性和可重用性，方便測試人員依據(jù)驗(yàn)證結(jié)果發(fā)現(xiàn)和理解原有硬件設(shè)計(jì)中的安全問題。

2 檢測硬件木馬

檢測硬件木馬的方法包含了3個步驟。

步驟1 從Verilog代碼構(gòu)造寄存器傳輸級的形式化驗(yàn)證模型。驗(yàn)證模型中“MODULE”定義的是模塊及其參數(shù)；“DEFINE”定義了常量，相當(dāng)于Verilog中的“parameter”；“VAR”定義了Verilog中的reg和wire等類型變量。“ASSIGN”定義了形式化驗(yàn)證模型的約束關(guān)系“路徑條件：變量表達(dá)式”，由Verilog代碼中的<路徑條件，表達(dá)式>對轉(zhuǎn)換得到。

步驟2 定義待驗(yàn)證設(shè)計(jì)的安全驗(yàn)證屬性。屬性的定義可以采用手工定義方式，或者算法自動挖掘方式。

步驟3 利用符號模型檢測器NuSMV驗(yàn)證步驟1構(gòu)造的形式化驗(yàn)證模型是否滿足步驟2定義的安全驗(yàn)證屬性。當(dāng)反例產(chǎn)生時進(jìn)行分析，確定導(dǎo)致驗(yàn)證屬性失敗的變量和相關(guān)變量取值，發(fā)現(xiàn)硬件木馬或其觸發(fā)器。

3 驗(yàn)證實(shí)驗(yàn)

實(shí)驗(yàn)運(yùn)行環(huán)境為Intel Core-i7-6500U CPU，主頻2.5 GHz和8 GB的DDR3內(nèi)存。實(shí)驗(yàn)對象為Trust-HUB 中寄存器傳輸級Verilog代碼形式的測試基準(zhǔn)。

3.1 從寄存器傳輸級Verilog代碼構(gòu)造形式化驗(yàn)證模型

表2中左邊一列是自動構(gòu)造的寄存器傳輸級形式化驗(yàn)證模型。右邊一列是其對應(yīng)的Trust-HUB RS232中u_xmit模塊的Verilog代碼。

表2 寄存器傳輸級的形式化驗(yàn)證模型構(gòu)造

3.2 定義安全驗(yàn)證屬性

表3列舉了實(shí)驗(yàn)中檢測到硬件木馬的安全驗(yàn)證屬性。

表3 檢測到硬件木馬的安全驗(yàn)證屬性

3.3 檢測硬件木馬

以T700為例，NuSMV 2.6的驗(yàn)證結(jié)果顯示為“假”，并且產(chǎn)生了一個反例。圖3表明了反例中各個變量之間值的變化關(guān)系。反例包含了710個狀態(tài)，在第709個狀態(tài)時，iXMIT.xmit_doneInH等于1，iXMIT.xmit_doneH在第710個狀態(tài)為0，從而使得安全驗(yàn)證屬性為假。進(jìn)一步地，依據(jù)形式化驗(yàn)證模型，xmit_doneH受DataSend_ena影響，DataSend_ena受state_DataSend影響，state_DataSend受輸入變量xmit_dataH影響。反例顯示，xmit_dataH出現(xiàn)了序列170(0xaa)，85(0x55)，0(0x00)，255(0xff)，這個序列即是硬件木馬的觸發(fā)器。

圖3 反例中的狀態(tài)變化關(guān)系

圖4 Trust-HUB RS232 T700仿真結(jié)果

表4列出了Trust-HUB 測試基準(zhǔn)中寄存器傳輸級設(shè)計(jì)的驗(yàn)證結(jié)果，其中PIC16F84由于電路較大，進(jìn)行了狀態(tài)空間約減。內(nèi)部數(shù)據(jù)觸發(fā)硬件木馬均被檢測到，包括組合電路木馬和時序電路木馬。

表4 Trust-HUB 測試基準(zhǔn)的驗(yàn)證結(jié)果

4 總 結(jié)

為了驗(yàn)證寄存器傳輸級設(shè)計(jì)中的硬件木馬，實(shí)現(xiàn)了一種自動構(gòu)造形式化驗(yàn)證模型的方法。整個方法的核心圍繞著Kripke結(jié)構(gòu)中的狀態(tài)轉(zhuǎn)移關(guān)系進(jìn)行構(gòu)造。這種轉(zhuǎn)移關(guān)系，是通過遍歷Verilog寄存器傳輸級設(shè)計(jì)的控制流圖，確定具有約束關(guān)系的<路徑條件，表達(dá)式>對集合實(shí)現(xiàn)的。實(shí)驗(yàn)表明，由驗(yàn)證產(chǎn)生的反例可以有效檢測到Verilog代碼中的內(nèi)部數(shù)據(jù)觸發(fā)類型硬件木馬或者其觸發(fā)器。

需要注意的是，設(shè)計(jì)錯誤也可能導(dǎo)致安全問題，引起安全屬性的驗(yàn)證結(jié)果為假，產(chǎn)生反例。但是設(shè)計(jì)錯誤通常在代碼結(jié)構(gòu)上不會明顯地表現(xiàn)出“觸發(fā)器+硬件木馬”這種比較典型的硬件木馬結(jié)構(gòu)。大多數(shù)設(shè)計(jì)錯誤的問題可以通過仿真測試發(fā)現(xiàn)，因此自動構(gòu)造方法針對通過基本功能測試的硬件設(shè)計(jì)代碼進(jìn)行安全驗(yàn)證，以盡可能避免設(shè)計(jì)錯誤的干擾。該方法構(gòu)造的形式化驗(yàn)證模型，可以較好地發(fā)現(xiàn)數(shù)據(jù)觸發(fā)類型的硬件木馬。未來的研究將會更多地集中在提高不同類型硬件木馬的驗(yàn)證效率以及自動化生成安全驗(yàn)證屬性上。