張啟智，趙毅強(qiáng)，高雅，馬浩誠(chéng)

基于模型檢測(cè)的硬件木馬檢測(cè)技術(shù)研究

張啟智，趙毅強(qiáng)，高雅，馬浩誠(chéng)

（天津大學(xué)微電子學(xué)院，天津 300110）

硬件木馬對(duì)原始電路的惡意篡改，已成為集成電路面臨的核心安全威脅。為了保障集成電路的安全可信，研究人員提出了諸多硬件木馬檢測(cè)方法。其中，模型檢測(cè)作為一種形式化驗(yàn)證方法，在設(shè)計(jì)階段可有效檢測(cè)出硬件木馬。首先，闡述了模型檢測(cè)的工作原理和應(yīng)用流程；其次，介紹了基于模型檢測(cè)的硬件木馬檢測(cè)技術(shù)的研究進(jìn)展；最后，指出了當(dāng)前該技術(shù)所面臨的瓶頸，并討論了潛在的研究方向。

硬件木馬；模型檢測(cè)；模型構(gòu)建；屬性聲明

1 引言

近年來(lái)，人工智能、5G等新興技術(shù)飛速發(fā)展，“萬(wàn)物互聯(lián)”的時(shí)代逐漸成為現(xiàn)實(shí)。集成電路作為現(xiàn)代信息技術(shù)的硬件基礎(chǔ)，其功能多樣性與應(yīng)用廣泛性迅速提升，已經(jīng)成為支撐經(jīng)濟(jì)社會(huì)發(fā)展的戰(zhàn)略性、基礎(chǔ)性和先導(dǎo)性產(chǎn)業(yè)。由于集成電路產(chǎn)品的先進(jìn)性和復(fù)雜性，同時(shí)為了更合理地配置資源，簡(jiǎn)化電路設(shè)計(jì)流程，縮短上市時(shí)間，電路設(shè)計(jì)者通常會(huì)大量復(fù)用將第三方IP核（intellectual property core）。然而，由于第三方機(jī)構(gòu)的不可控性，第三方IP核可能存在植入硬件木馬的風(fēng)險(xiǎn)，嚴(yán)重威脅集成電路的安全可信。

硬件木馬是指對(duì)原始集成電路的惡意篡改，如冗余模塊或惡意邏輯[1]。一般情況下，硬件木馬會(huì)保持靜默狀態(tài)，只有在滿足特定情況時(shí)才會(huì)被激活，執(zhí)行攻擊者預(yù)先設(shè)定的惡意行為，這對(duì)集成電路的安全造成了嚴(yán)重的威脅。被廣泛應(yīng)用于生產(chǎn)實(shí)踐中的硬件木馬檢測(cè)技術(shù)大多只適用于硅后階段，如邏輯測(cè)試、側(cè)信道分析等。基于邏輯測(cè)試的硬件木馬檢測(cè)技術(shù)通過(guò)在芯片的輸入端口施加特定的測(cè)試激勵(lì)，檢測(cè)輸出端口的信號(hào)是否與預(yù)期的輸出一致，進(jìn)而判斷電路中是否存在硬件木馬。但是，一些觸發(fā)結(jié)構(gòu)較為復(fù)雜的時(shí)序性硬件木馬難以被測(cè)試激勵(lì)觸發(fā)，有些硬件木馬即使被觸發(fā)也不會(huì)改變電路的輸出邏輯，使邏輯檢測(cè)技術(shù)在實(shí)際硬件木馬檢測(cè)中的使用大大受限[2]。基于側(cè)信道信息的硬件木馬檢測(cè)技術(shù)關(guān)注硬件木馬的植入給電路運(yùn)行參數(shù)帶來(lái)的影響[3]。早在2007年，Agrawal等[1]建立了芯片的功耗指紋模型，提出了利用電路的功耗信息來(lái)實(shí)現(xiàn)硬件木馬的檢測(cè)。之后，電磁、時(shí)延等多種側(cè)信道信息被應(yīng)用到木馬檢測(cè)中。但基于側(cè)信道信息的硬件木馬檢測(cè)技術(shù)容易受到檢測(cè)環(huán)境與工藝偏差的影響，導(dǎo)致難以完全識(shí)別出硬件木馬。綜上所述，硅后的硬件木馬檢測(cè)技術(shù)受到諸多限制的影響，木馬檢測(cè)的準(zhǔn)確率不高；同時(shí)，由于芯片已經(jīng)制造完成，即使檢測(cè)出硬件木馬，也難以對(duì)其進(jìn)行針對(duì)性的防御與修正。

模型檢測(cè)[4]是一種可以同時(shí)面向軟件和硬件的自動(dòng)化驗(yàn)證技術(shù)，其原理是通過(guò)對(duì)系統(tǒng)狀態(tài)空間進(jìn)行窮盡搜索來(lái)判斷系統(tǒng)是否滿足某些性質(zhì)。模型檢測(cè)作為形式化方法的一種，可以在硅前階段對(duì)芯片設(shè)計(jì)是否滿足規(guī)定的安全屬性進(jìn)行驗(yàn)證，在芯片投入生產(chǎn)之前對(duì)其中是否被植入了硬件木馬進(jìn)行檢測(cè)。同時(shí)，模型檢測(cè)可以在系統(tǒng)不滿足性質(zhì)規(guī)約時(shí)給出反例，有助于實(shí)現(xiàn)硬件木馬的定位并進(jìn)行針對(duì)性的修改。因此，近年來(lái)基于模型檢測(cè)的硬件木馬檢測(cè)技術(shù)逐漸成為相關(guān)領(lǐng)域研究的重點(diǎn)。

本文對(duì)基于模型檢測(cè)的硬件木馬檢測(cè)技術(shù)的應(yīng)用流程進(jìn)行了細(xì)致的歸納與梳理，對(duì)較為常用的模型檢測(cè)工具進(jìn)行了調(diào)研，對(duì)現(xiàn)有的電路形式化模型構(gòu)建方法與面向木馬檢測(cè)的安全屬性聲明策略進(jìn)行了詳細(xì)的總結(jié)。

2 模型檢測(cè)技術(shù)概述

2.1 基本原理與應(yīng)用流程

模型檢測(cè)是一種將給定的模型中所有可達(dá)狀態(tài)與行為進(jìn)行遍歷搜索，進(jìn)而驗(yàn)證其是否滿足某些性質(zhì)的方法。模型檢測(cè)具有兩個(gè)突出的優(yōu)點(diǎn)：一是模型檢測(cè)的自動(dòng)化程度非常高，整個(gè)驗(yàn)證的過(guò)程全部為自動(dòng)進(jìn)行，它并不要求驗(yàn)證人員對(duì)數(shù)學(xué)知識(shí)有非常專業(yè)的掌握；二是如果模型檢測(cè)得到的結(jié)果反饋表示所驗(yàn)證的模型或系統(tǒng)不能完全滿足屬性的約束或者不符合某些性質(zhì)，那么模型檢測(cè)器將生成一個(gè)反例，告訴驗(yàn)證人員具體哪些邏輯或哪些行為不滿足要求的屬性。這種機(jī)制對(duì)于驗(yàn)證人員了解系統(tǒng)安全性的漏洞，以及集成電路中是否存在硬件木馬有相當(dāng)大的幫助；同時(shí)，給驗(yàn)證人員排除惡意電路指明了方向。

利用模型檢測(cè)技術(shù)來(lái)進(jìn)行電路中硬件木馬的檢測(cè)一般分為以下3步：電路模型的構(gòu)建、安全屬性的聲明以及驗(yàn)證[5]。模型檢測(cè)的應(yīng)用流程如圖1所示。首先是電路模型的構(gòu)建，也就是將電路設(shè)計(jì)轉(zhuǎn)換為模型檢測(cè)器可以讀取的形式。在多數(shù)情況下，模型構(gòu)建是電路描述語(yǔ)言向形式化語(yǔ)言的轉(zhuǎn)譯。然而，在有些情況下，受限于驗(yàn)證時(shí)間和計(jì)算機(jī)內(nèi)存，需要對(duì)模型進(jìn)行化簡(jiǎn)或省略與驗(yàn)證目標(biāo)無(wú)關(guān)的電路。其次是安全屬性的聲明，驗(yàn)證者需要首先聲明希望電路滿足的性質(zhì)，這種性質(zhì)一般以某種邏輯的形式進(jìn)行表達(dá)。最后是驗(yàn)證，驗(yàn)證的過(guò)程一般是由解析器自動(dòng)化實(shí)現(xiàn)的，但在實(shí)際的驗(yàn)證過(guò)程中需要一定程度的人為參與，如對(duì)未通過(guò)驗(yàn)證的結(jié)果進(jìn)行分析，進(jìn)而提出對(duì)應(yīng)的安全性設(shè)計(jì)需求。

圖1 模型檢測(cè)的應(yīng)用流程

Figure 1 Application process of model checking

2.2 常用檢測(cè)工具

2.2.1 NuSMV

NuSMV（new symbolic model verifyer）[6]是由Carnegie Mellon大學(xué)基于SMV（symbolic model verifyer）[7]開發(fā)的，以有序二叉判定圖為基礎(chǔ)對(duì)有限狀態(tài)系統(tǒng)是否滿足基于CTL邏輯描述的屬性約束進(jìn)行驗(yàn)證的模型檢測(cè)器。經(jīng)過(guò)長(zhǎng)時(shí)間的使用和更新，NuSMV已經(jīng)是一個(gè)較為成熟的可以同時(shí)適用于軟硬件驗(yàn)證的模型檢測(cè)器[8-10]。

NuSMV是一個(gè)開放式（這是其最重要的特征）的系統(tǒng)，它的內(nèi)部由解析器、實(shí)例化模塊、編碼模塊、模型檢測(cè)模塊等組成。每個(gè)模塊實(shí)現(xiàn)一組功能，并通過(guò)精準(zhǔn)定義的接口與其他模塊進(jìn)行交互，這種設(shè)計(jì)方式方便用戶根據(jù)自己的需要進(jìn)行調(diào)整和修改。

NuSMV兼容的程序代碼在結(jié)構(gòu)組成上與硬件描述語(yǔ)言類似，由模塊組成。每個(gè)程序必須有一個(gè)主模塊，主模塊中定義系統(tǒng)的主要功能以及各個(gè)模塊之間的關(guān)系，同時(shí)可以對(duì)其余模塊進(jìn)行多次實(shí)例化。這種編程方式與硬件設(shè)計(jì)的代碼描述方式高度契合，因此，在面向硬件安全的模型檢測(cè)研究中，NuSMV的使用非常廣泛[11-13]。NuSMV代碼結(jié)構(gòu)如圖2所示。

2.2.2 UPPAAL

UPPAAL是由瑞典的Uppsala大學(xué)和丹麥的Aalborg大學(xué)聯(lián)合開發(fā)用于實(shí)時(shí)系統(tǒng)驗(yàn)證的工具[14]，它在通信協(xié)議和多媒體領(lǐng)域得到了成功的應(yīng)用。UPPAAL模型檢測(cè)器包括3部分：編輯器、模擬器和驗(yàn)證器。編輯器是建立時(shí)間自動(dòng)機(jī)模型的部分；模擬器是對(duì)編輯器中建立的模型進(jìn)行仿真模擬的部分；驗(yàn)證器是編寫安全屬性并對(duì)其進(jìn)行驗(yàn)證的模塊，在這一模塊中，用戶可以利用查詢語(yǔ)言對(duì)想要驗(yàn)證的安全屬性進(jìn)行編寫。UPPAAL的基本結(jié)構(gòu)如圖3 所示。

圖2 NuSMV代碼結(jié)構(gòu)

Figure 2 The code structure of NuSMV

圖3 UPPAAL的基本結(jié)構(gòu)

Figure 3 The fundamental structure of UPPAAL

在UPPAAL中，一個(gè)系統(tǒng)被建模為由多個(gè)時(shí)間自動(dòng)機(jī)并行組成的網(wǎng)絡(luò)。系統(tǒng)的每個(gè)狀態(tài)在UPPAAL中被定義為位置、時(shí)鐘變量以及有界變量的集合。每個(gè)時(shí)間自動(dòng)機(jī)通過(guò)激活邊界或者觸發(fā)與其他自動(dòng)機(jī)的同步信號(hào)來(lái)進(jìn)入下一個(gè)狀態(tài)。

雖然相比于一般的模型檢測(cè)器，UPPAAL的性能與效率均較為優(yōu)異[15]，但受限于電路模型建立的復(fù)雜程度以及工具本身難以滿足電路中常見數(shù)據(jù)類型的聲明要求，UPPAAL在硬件安全驗(yàn)證領(lǐng)域的應(yīng)用并不如NuSMV廣泛[16-18]。

3 不同種類硬件木馬的模型檢測(cè)技術(shù)

在利用模型檢測(cè)技術(shù)進(jìn)行硬件木馬檢測(cè)的過(guò)程中，需要對(duì)不同種類的硬件木馬根據(jù)其功能或結(jié)構(gòu)特點(diǎn)有針對(duì)性地展開驗(yàn)證。硬件木馬根據(jù)其功能可分為4類：降低性能型、改變功能型、拒絕服務(wù)型、信息泄露型[19]。下面將詳細(xì)介紹針對(duì)各種類型硬件木馬的模型檢測(cè)方法。

3.1 降低性能型硬件木馬的模型檢測(cè)技術(shù)

降低性能型硬件木馬是指通過(guò)改變電路的制造參數(shù)（如使電路的主頻下降、低溫下系統(tǒng)癱瘓、電磁輻射變強(qiáng)和電量消耗加速等）來(lái)降低電路性能的木馬。對(duì)于這種類型的硬件木馬，驗(yàn)證者在進(jìn)行模型檢測(cè)時(shí)，通常考慮對(duì)木馬可能攻擊的某些電路參數(shù)設(shè)定閾值，基于不能超過(guò)預(yù)設(shè)閾值這一特性聲明電路應(yīng)當(dāng)滿足的安全屬性。

Hasan等[20]對(duì)包含兩個(gè)主機(jī)和一個(gè)從機(jī)的高級(jí)處理器總線結(jié)構(gòu)（AMBA）進(jìn)行建模，其中從機(jī)中被植入創(chuàng)造死鎖場(chǎng)景，使從機(jī)優(yōu)先于主機(jī)占用總線以降低處理器性能的硬件木馬。對(duì)于此類木馬，基于計(jì)算樹邏輯（CTL，computation tree logic）描述了如下安全屬性：對(duì)于全部狀態(tài)路徑，主機(jī)的總線使用優(yōu)先級(jí)要高于從機(jī)。在得到反例后，基于反例描述的死鎖情況運(yùn)用博弈論的理論對(duì)木馬植入和檢測(cè)的復(fù)雜程度進(jìn)行分析，并給出了針對(duì)性的木馬檢測(cè)結(jié)構(gòu)設(shè)計(jì)意見。

文獻(xiàn)[21-22]基于電路運(yùn)行過(guò)程中產(chǎn)生的側(cè)信道信息進(jìn)行了電路模型的構(gòu)建，明確了電路中存在的各種邏輯門在真值表的各個(gè)狀態(tài)下產(chǎn)生的功耗信息以及邏輯門自身的時(shí)延信息，通過(guò)統(tǒng)計(jì)電路中所有可能的狀態(tài)得到電路功耗與時(shí)延信息的上下限，基于側(cè)信道信息的閾值構(gòu)建電路應(yīng)當(dāng)滿足的安全屬性。研究者在基準(zhǔn)電路中插入冗余的邏輯門作為硬件木馬，按照上述方式聲明安全屬性，在模型檢測(cè)器中進(jìn)行驗(yàn)證，成功檢測(cè)出了植入的硬件木馬，如式(1)、式(2)所示。

上述安全屬性用自然語(yǔ)言描述為：電路中所有邏輯門的功耗之和應(yīng)大于或等于電路總功耗的最小值且小于或等于電路總功耗的最大值；電路中某條通路上所有邏輯門的時(shí)延之和應(yīng)大于或等于通路時(shí)延的最小值，且小于或等于通路時(shí)延的最大值。

3.2 改變功能型硬件木馬的模型檢測(cè)技術(shù)

改變功能型硬件木馬是通過(guò)增加、刪減或者修改電路邏輯，在特定時(shí)刻篡改原始電路的功能，使電路產(chǎn)生錯(cuò)誤輸出甚至使電路癱瘓的木馬。針對(duì)此類硬件木馬的模型檢測(cè)技術(shù)往往需要將安全屬性定義為待驗(yàn)證電路功能與正確功能完全一致或者對(duì)于特定的攻擊場(chǎng)景將安全屬性定義為只能執(zhí)行特定指令。

Rathmair等[23]采用模型檢測(cè)的技術(shù)對(duì)植入在內(nèi)存控制器中的硬件木馬進(jìn)行檢測(cè)。該研究針對(duì)的硬件木馬在地址信號(hào)高于某個(gè)預(yù)設(shè)閾值時(shí)，交換地址信息的某兩位數(shù)值，使外部無(wú)法訪問(wèn)到正確的內(nèi)存中的信息。針對(duì)這種改變功能型的木馬，研究者首先將電路轉(zhuǎn)譯為形式化模型，進(jìn)而提出了針對(duì)性的安全屬性：

用自然語(yǔ)言描述為存儲(chǔ)器接口的地址不得與輸入的16位地址不同。如果出現(xiàn)輸入存儲(chǔ)器接口的地址信息與預(yù)設(shè)地址信息不同的情況，模型檢測(cè)器就會(huì)報(bào)告驗(yàn)證失敗并生成反例。

Zhang等[24]針對(duì)難以通過(guò)電路運(yùn)行參數(shù)差別進(jìn)行微小木馬展開模型檢測(cè)。該微型木馬可以篡改電路的真值表，影響電路的正常輸出。研究者將原始電路和可疑電路組成可疑電路對(duì)，并統(tǒng)一對(duì)原始電路和可疑電路進(jìn)行模型構(gòu)建，采用CTL邏輯對(duì)可疑電路對(duì)進(jìn)行安全屬性的約束：

用自然語(yǔ)言表述為對(duì)于任意相同的輸入變量，可疑電路對(duì)的輸出總是相同的。這是一種白名單的驗(yàn)證策略，也就是說(shuō)只允許出現(xiàn)與母本電路真值表相同的情況。如果屬性驗(yàn)證沒有通過(guò)，即可得知可疑電路與母本電路并不完全一致，進(jìn)而檢測(cè)出硬件木馬的存在。

Zhao等[25]同樣采用白名單的驗(yàn)證策略對(duì)改變功能型硬件木馬進(jìn)行檢測(cè)，基于電路的邏輯運(yùn)算結(jié)果建立安全屬性；Krieg等[26]通過(guò)對(duì)惡意行為進(jìn)行描述的方式來(lái)建立安全屬性，然而這種屬性建立方式存在一個(gè)問(wèn)題，即如果屬性通過(guò)驗(yàn)證則可以說(shuō)明電路中存在惡意邏輯，但如果屬性未能通過(guò)驗(yàn)證卻并不能保證電路中不存在其他惡意邏輯。

3.3 拒絕服務(wù)型硬件木馬的模型檢測(cè)技術(shù)

拒絕服務(wù)型硬件木馬在特定條件下可以使系統(tǒng)暫時(shí)性拒絕響應(yīng)、狀態(tài)跳轉(zhuǎn)紊亂甚至系統(tǒng)永久性癱瘓等，常常被植入在總線、微處理器等硬件場(chǎng)景中。對(duì)于此類硬件木馬，可以采用以下兩種驗(yàn)證策略：①用形式化語(yǔ)義描述電路的正常功能，查看模型檢測(cè)器是否報(bào)告反例；②對(duì)于可能的木馬攻擊方式，針對(duì)性地設(shè)計(jì)安全屬性進(jìn)行驗(yàn)證，這種驗(yàn)證策略需要對(duì)木馬的攻擊方式以及可能的攻擊位置有充分的認(rèn)識(shí)。

高洪博[27]在2013年提出了一種基于模型檢測(cè)的指令誘發(fā)型硬件木馬的檢測(cè)技術(shù)，在以微處理器為核心的交通燈控制系統(tǒng)中植入了設(shè)計(jì)的木馬[28]，其功能由特定的指令序列觸發(fā)，觸發(fā)后導(dǎo)致系統(tǒng)工作紊亂，無(wú)法正常工作。研究者基于CTL對(duì)系統(tǒng)應(yīng)當(dāng)產(chǎn)生的正常功能進(jìn)行描述，驗(yàn)證發(fā)現(xiàn)存在不符合屬性約束的反例，同時(shí)對(duì)固件代碼進(jìn)行逆向，可以得到產(chǎn)生反例的代碼序列，檢測(cè)并定位到硬件木馬，交通燈控制系統(tǒng)正常顯示序列的CTL語(yǔ)言描述如式(6)所示。

He等[29]考慮了具有主機(jī)A與主機(jī)B的總線結(jié)構(gòu)，拒絕服務(wù)型硬件木馬被植入在主機(jī)B中。正常工作模式下，兩個(gè)主機(jī)擁有相同的優(yōu)先級(jí)，不會(huì)出現(xiàn)某個(gè)主機(jī)長(zhǎng)時(shí)間占用總線的情況。而主機(jī)B中植入的硬件木馬能夠修改并調(diào)高主機(jī)B的優(yōu)先等級(jí)，此時(shí)如果主機(jī)B不斷請(qǐng)求總線的使用權(quán)限，主機(jī)A將無(wú)法訪問(wèn)總線參與通信，影響SoC的正常功能，發(fā)生拒絕服務(wù)攻擊。研究者首先提取了電路的有限狀態(tài)機(jī)模型，對(duì)電路進(jìn)行了完備的形式化描述。隨后提出了針對(duì)該類木馬攻擊的電路安全屬性（總線的使用權(quán)限不能被某個(gè)主機(jī)長(zhǎng)期占用，尤其當(dāng)其他主機(jī)也在請(qǐng)求總線的使用權(quán)限時(shí)）。研究者采用了遞進(jìn)式的驗(yàn)證方法，首先驗(yàn)證是否存在主機(jī)B長(zhǎng)期占用總線的情況，進(jìn)而驗(yàn)證在這種情況下主機(jī)A是否嘗試取得總線的使用權(quán)限。在UPPAAL解析器中對(duì)上述安全屬性進(jìn)行驗(yàn)證，成功檢測(cè)出了拒絕服務(wù)型硬件木馬。

3.4 信息泄露型硬件木馬的模型檢測(cè)技術(shù)

信息泄露型硬件木馬是母本電路中的冗余電路，借助電路的輸出端口、掃描測(cè)試端口、射頻發(fā)射模塊以及電路耗散的側(cè)信道信息等泄露電路內(nèi)部的私密信息。對(duì)于這一類硬件木馬，驗(yàn)證人員通常通過(guò)“敏感信息不能被已知模塊以外的模塊獲取”這一安全屬性進(jìn)行驗(yàn)證。

He等[29]針對(duì)總線結(jié)構(gòu)中植入在從機(jī)的讀取總線信息的硬件木馬，提出了由主機(jī)存儲(chǔ)給特定從機(jī)的信息不應(yīng)該被泄露給總線上其他從機(jī)的安全屬性，首先通過(guò)狀態(tài)存在性的約束確定了電路的有限狀態(tài)機(jī)模型中確實(shí)存在信息泄露，進(jìn)而通過(guò)狀態(tài)可達(dá)性的約束確定了硬件木馬被植入的位置，成功檢測(cè)出了信息泄露型硬件木馬。

Rajendran等[30]在檢測(cè)信息泄露型硬件木馬時(shí)，首先考慮安全屬性，即存在一種輸入的情況能夠使密鑰被輸出。盡管這一安全屬性存在諸多缺陷，如需要檢測(cè)所有狀態(tài)情況、無(wú)法檢測(cè)分段輸出的密鑰等，它仍然是檢測(cè)信息泄露型木馬的基礎(chǔ)屬性。

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

近年來(lái)，基于模型檢測(cè)的硬件木馬檢測(cè)技術(shù)逐漸成為硬件安全領(lǐng)域研究的熱點(diǎn)。對(duì)于面向硬件木馬檢測(cè)的模型檢測(cè)技術(shù)來(lái)說(shuō)，狀態(tài)爆炸問(wèn)題始終是限制其發(fā)展的最主要的瓶頸[31]。對(duì)于一個(gè)具有個(gè)邏輯門的電路來(lái)說(shuō)，其所具有的電路狀態(tài)數(shù)目為2。而如今超大規(guī)模集成電路已經(jīng)被廣泛生產(chǎn)和應(yīng)用，想要對(duì)具有數(shù)百萬(wàn)的邏輯門的電路系統(tǒng)進(jìn)行完備的模型建立與驗(yàn)證十分具有挑戰(zhàn)性。

在學(xué)術(shù)界，緩解狀態(tài)爆炸的主要方法有4種：組合推理、抽象技術(shù)、對(duì)稱、歸納。由于電路設(shè)計(jì)具有模塊化的特點(diǎn)，面向硬件安全的模型檢測(cè)研究者通常采用組合推理的方式來(lái)緩解電路建模的狀態(tài)爆炸問(wèn)題，即對(duì)電路進(jìn)行分模塊建?；蛘邔?duì)于特定電路模塊而非全部電路進(jìn)行建模與驗(yàn)證[29-32]。而分模塊建模的方法必須要考慮的問(wèn)題是分模塊建模的情況下仍然需要保證模型能夠完備地描述全部電路狀態(tài)，針對(duì)特定模塊進(jìn)行建模則需要對(duì)硬件木馬的攻擊模式有相當(dāng)全面的了解和認(rèn)識(shí)。這些問(wèn)題在一定程度上限制了基于模型檢測(cè)的硬件木馬檢測(cè)技術(shù)的實(shí)際應(yīng)用。

基于上述研究現(xiàn)狀，對(duì)電路模型的約簡(jiǎn)可作為未來(lái)的一個(gè)研究方向。例如，硬件電路中擁有許多重復(fù)的單元，如存儲(chǔ)單元等，在建模過(guò)程中可以通過(guò)特定的技術(shù)手段對(duì)這些重復(fù)單元對(duì)應(yīng)的狀態(tài)機(jī)進(jìn)行化簡(jiǎn)，進(jìn)而達(dá)到減少驗(yàn)證開銷的目的。

[1]AGRAWAL D, BAKTIR S, KARAKOYUNLU D, et al. Trojan detection using IC fingerprinting[C]//IEEE Symposium on Security and Privacy (SP '07), 2007: 296-310.

[2]FLOTTES M, DUPUIS S, BA P, et al. On the limitations of logic testing for detecting hardware Trojans Horsesv[C]//10th International Conference on Design & Technology of Integrated Systems in Nanoscale Era (DTIS), Naples. 2015: 1-5.

[3]HELY D, MARTIN J, DARIO G, et al. Experiences in side channel and testing based hardware Trojan detection[C]//IEEE 31st VLSI Test Symposium (VTS). 2013: 1-4.

[4]CLARKE E M, GRUMBERGO, PELED D, et al. Model checking[M]. Cambridge: MIT press, 1999.

[5]BARTOLETTI M, DEGANO P, FERRARI G L, et al. Model checking usage policies[C]//Trustworthy Global Computing. 2009: 19-35.

[6]ALESSANDRO C, EDMUND C, FAUSTO G, et al. NUSMV: a new symbolic model checker[J]. STTT 2, 2000: 410-425

[7]MCMILLAN K L. Symbolic model checking: an approach to the state explosion problem[M]. Kluwer Academic, 1993.

[8]SZWED P. Efficiency of formal verification of ArchiMate business processes with NuSMV model checker[C]//Federated Conference on Computer Science and Information Systems (FedCSIS), Lodz. 2015: 427-1436.

[9]XU N, MA Z, JIANG J, et al. Model checking instance based on NuSMV[C]//IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation (SmartWorld/SCALCOM/UIC/ATC/ CBDCom/IOP/SCI). 2018: 2052-2056.

[10]SEBASTIANI R, ROVERI Marco, PISTORE M, et al. NuSMV2: an open source tool for symbolic model checking[C]//International Conference on Computer Aided Verification. 2002.

[11]HASAN SR, KAMHOUA CA, KWIAT KA, et al. Translating circuit behavior manifestations of hardware Trojans using model checkers into run-time Trojan detection monitors[C]//IEEE Asian Hardware-Oriented Security and Trust (AsianHOST). 2016: 1-6.

[12]DESAI K, STEVENS K. S, O'LEARY J, et al. Symbolic verification of timed asynchronous hardware protocols[C]//IEEE Computer Society Annual Symposium on VLSI (ISVLSI). 2013: 47-152.

[13]PAKONEN A, BUZHINSKY I. Verification of fault tolerant safety I&C systems using model checking[C]//International Conference on Industrial Technology. 2019.

[14]BEHRMANN G,DAVID A, LARSEN K G.A Tutorial on UPPAAL[C]//Proc of Int school on Formal Methods for the Design of Computer Communication & Software Systems. 2004: 200-236.

[15]AAAMIR N,FAROOQUE A, AMJAD A,et al. Comparison of model checking tools using timed automata - PRISM and UPPAAL[C]//IEEE International Conference on Computer and Communication Engineering Technology (CCET). 2018: 248-253.

[16]YAN X, LI Y, LI X. Real-time simulation of automotive systems based on UPPAAL[C]//Proceedings of 2017 IEEE 8th International Conference on Software Engineering and Service Science. 2017: 193-196.

[17]CHAUDHTY Y. A. K, HAMMED M. Formal verification of cloud based distributed System using UPPAAL[C]//International Conference on Innovation and Intelligence for Informatics, Computing, and Technologies (3ICT). 2019: 1-4.

[18]YAN X, WANG L, CHE X, et al. Source code testing for automotive software based on UPPAAL model[C]//IEEE International Conference on Software Engineering & Service Science, 2014: 95-98.

[19]LI H, LIU Q, ZHANG J, et al. A Survey of hardware Trojan detection, diagnosis and prevention[C]//IEEE International Conference on Computer-aided Design & Computer Graphics. 2016.

[20]HASAN S. R, KAMHOUA C. A, KWIAT K. A, et al. A novel framework to introduce hardware Trojan monitors using model checking based counterexamples: inspired by game theory[C]//2018 IEEE 61st International Midwest Symposium on Circuits and Systems (MWSCAS). 2018: 853-856.

[21]LODHI F K, ABBASI I H, KAMBOH A M, et al. Formal verification of gate-level multiple side channel parameters to detect hardware Trojans[C]//Communications in Computer and Information Science. 2016.

[22]HAFEEZ A I, FAIQ K, OSMAN H, et al. McSeVIC: a model checking based framework for security vulnerability analysis of integrated circuits[J]. IEEE Access, 2018, 6 :1.

[23]RATHMAIR M, SCHUPFER F, KRIEG C. Applied formal methods for hardware Trojan detection[C]//IEEE International Symposium on Circuits & Systems. 2014: 169-172.

[24]ZHANG Y, YU L, LI H, et al. Small Trojan testing using bounded model checking[C]//IEEE International Test Conference. 2018.

[25]ZHAO J F. Case study: discovering hardware Trojans based on model checking[C]//The 8th International Conference. 2018: 64-68.

[26]KRIEG C, RATHMAIR M, SCHUPFER F. A process for the detection of design-level hardware Trojans using verification methods[C]//High Performance Computing & Communications, IEEE Intl Symp on Cyberspace Safety & Security, IEEE Intl Conf on Embedded Software & Syst. 2015.

[27]高洪博. 指令誘發(fā)型硬件木馬檢測(cè)技術(shù)研究[D]. 鄭州: 信息工程大學(xué), 2013. GAO H B. Research on detection techniques of instruction-triggered hardware Trojan horse[D]. Zhengzhou: Information Engineering University, 2013.

[28]GAO H, LI Q, ZHU Y, et al. Code-controlled hardware Trojan horse[C]//International Conference on Information Computing & Applications. 2012: 171-178.

[29]HE J J, GUO X, MEADE T, et al. SoC interconnection protection through formal verification[J]. Integration, 2019, 64: 143-151.

[30]RAJENDRAN J, DHANDAYUTHAPANY A M, VEDULA V, et al. Formal security verification of third party intellectual property cores for information leakage[C]//IEEE International Conference on VLSI Design & International Conference on Embedded Systems. 2016: 547-552.

[31]CLARKE E M, KLIEBER W, MILO N, et al. Model checking and the state explosion problem[J]. Lecture Notes in Computer Science, 2011: 1-30.

[32]CRUZ J, FARAHMANDI F, AHMED A, et al. Hardware Trojan detection using ATPG and model checking[C]//International Conference on Vlsi Design & International Conference on Embedded Systems. 2018: 91-96.

Survey on model checking based hardware Trojan detection technology

ZHANG Qizhi, ZHAO Yiqiang, GAOYa, MA Haocheng

School of MicroElectronics, Tianjin University, Tianjin 300110, China

Hardware Trojanis malicious tampering to the original circuit, which has become the most important security threat of integrated circuit.In order to ensure the safety and reliability of ICs, many hardware Trojan detection methods are proposed.As one of the formal verification methods, model checking can effectively detect the hardware Trojan in the design phase. Firstly, the working principle andprocess of model checking were described. Secondly, the research progress of hardware Trojan detection technology based on model checking was introduced. Finally, the bottlenecks faced by the current technology were pointed out and the potential research direction was discussed.

hardware Trojan, model checking, model establishing, property declaration

TN407

A

10.11959/j.issn.2096?109x.2021029

2020?11?16；

2021?01?21

趙毅強(qiáng)，yq_zhao@tju.edu.cn

國(guó)家自然科學(xué)基金（61832018）

The National Natural Science Foundation of China(61832018)

張啟智, 趙毅強(qiáng), 高雅, 等. 基于模型檢測(cè)的硬件木馬檢測(cè)技術(shù)研究[J]. 網(wǎng)絡(luò)與信息安全學(xué)報(bào), 2021, 7(2): 57-63.

ZHANG Q Z, ZHAO Y Q, GAO Y, et al. Survey on model checking based hardware Trojan detection technology[J]. Chinese Journal of Network and Information Security, 2021, 7(2): 57-63.

張啟智（1998? ），男，山東菏澤人，天津大學(xué)博士生，主要研究方向?yàn)榧呻娐吩O(shè)計(jì)與硬件形式化驗(yàn)證。

趙毅強(qiáng)（1964? ），男，河北辛集人，博士，天津大學(xué)教授、博士生導(dǎo)師，主要研究方向?yàn)榧呻娐钒踩?、混合信?hào)集成電路設(shè)計(jì)、光電檢測(cè)與成像系統(tǒng)設(shè)計(jì)、傳感器系統(tǒng)設(shè)計(jì)。

高雅（1998? ），女，遼寧東港人，天津大學(xué)碩士生，主要研究方向?yàn)閿?shù)字電路安全。

馬浩誠(chéng)（1996? ），男，河北滄州人，天津大學(xué)博士生，主要研究方向?yàn)榧呻娐吩O(shè)計(jì)與硬件安全。