基于可滿足性無關(guān)項的硬件木馬設(shè)計與檢測

武玲娟，朱嘉誠，唐時博，譚靜，胡偉

基于可滿足性無關(guān)項的硬件木馬設(shè)計與檢測

武玲娟1,2，朱嘉誠1，唐時博1，譚靜1，胡偉1

（1.西北工業(yè)大學(xué)網(wǎng)絡(luò)空間安全學(xué)院，陜西 西安 710072；2. 華中農(nóng)業(yè)大學(xué)信息學(xué)院，湖北 武漢 430070）

硬件木馬是集成電路中隱含的惡意設(shè)計修改，被激活后可用于發(fā)起高效的底層攻擊。由此，展示了一種新的利用可滿足性無關(guān)項的輕量級高隱蔽性硬件木馬安全威脅。該木馬設(shè)計方法將輕量級木馬設(shè)計隱藏于電路正常工作條件下無法覆蓋到的可滿足性無關(guān)項中，使插入木馬后的電路設(shè)計與原始設(shè)計完全功能等價。攻擊者只需利用簡單的故障注入攻擊手段即可激活木馬?；?024位RSA密碼核的實驗結(jié)果顯示，所給出的木馬設(shè)計能夠逃避邏輯綜合優(yōu)化，通過故障注入攻擊能夠有效恢復(fù)RSA密碼核的私鑰。在此基礎(chǔ)上，提出了一種能夠有效檢測該高隱蔽性木馬設(shè)計的防御手段。

硬件安全；硬件木馬；可滿足性無關(guān)項；故障注入；木馬檢測

1 引言

隨著集成電路產(chǎn)業(yè)鏈的全球化，集成電路設(shè)計中通常會大量使用來自不可信第三方的知識產(chǎn)權(quán)（IP，intellectual property）核。這些IP中可能隱含設(shè)計規(guī)范之外的未公開惡意代碼和后門。此外，由于成本限制，集成電路設(shè)計完成之后往往交由芯片制造商進(jìn)行加工，此過程中不可信制造商也可能插入未聲明惡意設(shè)計修改。上述由不可信第三方引入的惡意設(shè)計修改，稱為硬件木馬[1]，硬件木馬通常只有在特定的條件下才會激活，現(xiàn)有的集成電路測試方法難以實現(xiàn)木馬檢測。攻擊者可通過特定輸入、側(cè)信道、故障注入等方式激活木馬，從而造成敏感信息泄露、設(shè)計性能降低甚至系統(tǒng)失效，造成極大的安全威脅[2]。

Karri 等[3]根據(jù)插入階段、激活機(jī)制、負(fù)載特性等對硬件木馬進(jìn)行了系統(tǒng)分類。根據(jù)這一分類系統(tǒng)，Trust-HUB.org平臺上發(fā)布了一系列硬件木馬設(shè)計。這些木馬設(shè)計使用計時器或特定輸入向量作為木馬的激活條件[4]，產(chǎn)生一個單一信號用于觸發(fā)木馬，使這些木馬很容易被翻轉(zhuǎn)概率分析方法檢測到[5-6]。為了抵御基于翻轉(zhuǎn)概率分析的木馬檢測方法，研究者提出使用多個分離的信號作為木馬觸發(fā)信號的設(shè)計方法[7-8]，由于采用基于木馬在特定條件下觸發(fā)的方式，基于標(biāo)簽傳播的翻轉(zhuǎn)概率分析方法和基于無關(guān)項分析的方法仍能夠?qū)⒛抉R識別為惡意或冗余邏輯[9-10]。可見，現(xiàn)有硬件木馬設(shè)計方法通常需引入低活度的觸發(fā)信號、改變設(shè)計功能或存在顯著的負(fù)載指紋，上述特征使檢測此類木馬較為簡單。

為了提高硬件木馬的隱蔽性，防止木馬在設(shè)計階段被檢測到，近年來，研究者提出了基于無關(guān)項的木馬設(shè)計方法，利用集成電路設(shè)計空間中的外部無關(guān)項，包括未聲明的功能、有限狀態(tài)機(jī)中未占用的編碼、X狀態(tài)[11-14]進(jìn)行木馬設(shè)計。插入木馬的電路是原始電路設(shè)計空間的超集，在正常工作情況下，電路并不會進(jìn)入木馬所在的設(shè)計空間，因此，包含外部無關(guān)項木馬的電路完全符合設(shè)計規(guī)范要求，基于設(shè)計規(guī)范驗證的方法難以實現(xiàn)木馬檢測。但是，該方法并不適用于設(shè)計空間被完全聲明的集成電路。

文獻(xiàn)[15]提出了一種利用可滿足性無關(guān)項的硬件木馬設(shè)計方法，利用集成電路內(nèi)部扇出重匯聚引入的可滿足性無關(guān)項，作為木馬的觸發(fā)信號，控制木馬泄露AES算法的密鑰。相對于基于外部無關(guān)項的木馬設(shè)計方法[11-14]，上述工作適用于功能被完全聲明的電路設(shè)計。同時，由于木馬設(shè)計隱藏在電路正常工作條件下無法滿足的可滿足性無關(guān)項中，插入木馬之后的電路設(shè)計與原始設(shè)計完全功能等價，功能等價性驗證并不能檢測到木馬，該木馬設(shè)計引入了256個二輸入選擇器，負(fù)載指紋較為顯著。

本文展示了一種新的利用可滿足性無關(guān)項的輕量級高隱蔽性硬件木馬安全威脅，利用可滿足性無關(guān)項，設(shè)計了針對公鑰密碼系統(tǒng)的輕量級硬件木馬，揭示了公鑰密碼系統(tǒng)所面臨的一種新的硬件木馬安全威脅，并通過實驗驗證其隱蔽性和可利用性。在此基礎(chǔ)上，提出了一種能夠有效檢測該高隱蔽性木馬設(shè)計的防御手段。本文主要工作及貢獻(xiàn)如下：

1) 展示了一種新的利用可滿足性無關(guān)項的輕量級高隱蔽性硬件木馬安全威脅；

2) 通過實驗結(jié)果驗證了該硬件木馬設(shè)計的高隱蔽性和可利用性；

3) 提出了一種能夠有效應(yīng)對該高隱蔽性木馬安全威脅的防御手段。

2 相關(guān)工作

本節(jié)介紹與本文工作密切相關(guān)的無關(guān)性木馬設(shè)計。無關(guān)性木馬利用集成電路設(shè)計空間的外部或內(nèi)部無關(guān)項進(jìn)行木馬設(shè)計，相比傳統(tǒng)基于計數(shù)器或特定輸入向量觸發(fā)的木馬設(shè)計方法，具有更高的隱蔽性。

Fern等[11-12]利用集成電路設(shè)計中未聲明功能引入的外部無關(guān)項進(jìn)行木馬設(shè)計，選取電路中具有未聲明行為的信號，對其功能進(jìn)行修改以添加惡意邏輯，由于插入木馬之后的設(shè)計空間是原始設(shè)計的超集，使用者根據(jù)原始設(shè)計規(guī)范進(jìn)行功能及形式化等價性驗證并不能發(fā)現(xiàn)所插入的木馬。Nahiyan等[13]提出利用有限狀態(tài)機(jī)中未聲明狀態(tài)進(jìn)行木馬設(shè)計的方法，基于集成電路設(shè)計或綜合優(yōu)化中引入的無關(guān)狀態(tài)，插入惡意木馬邏輯，在正常工作下，有限狀態(tài)機(jī)不會切換到包含木馬邏輯的狀態(tài)，而攻擊者可通過故障攻擊使有限狀態(tài)機(jī)進(jìn)入惡意狀態(tài)以激活木馬。Krieg等[14]提出利用X無關(guān)項作為觸發(fā)信號的木馬設(shè)計方法，利用X無關(guān)項信號在仿真中為邏輯0，而在實現(xiàn)電路中為邏輯1的特點，使設(shè)計階段形式化等價性驗證并不能檢測到木馬。以上方法[11-14]可以提高木馬的隱蔽性，但是，當(dāng)電路功能被完全聲明時，基于外部無關(guān)項的木馬設(shè)計方法并不適用。

近年來，Hu等[15]提出利用集成電路內(nèi)部無關(guān)項的木馬設(shè)計方法，木馬隱藏在電路正常工作條件下無法滿足的可滿足性或可觀測性無關(guān)項中，攻擊者通過故障注入攻擊可以激活木馬?；趦?nèi)部無關(guān)項的木馬設(shè)計方法在多用戶FPGA平臺上進(jìn)一步完成了驗證，攻擊者通過部署能量損耗電路引入故障攻擊可以遠(yuǎn)程激活木馬，竊取其他用戶的密鑰信息[16]。研究者提出利用混淆電路中未聲明功能的木馬設(shè)計方法[17]，邏輯混淆是為了防止集成電路IP被盜竊、仿造，在原始電路中加入的設(shè)計，當(dāng)混淆密鑰被正確加載時電路實現(xiàn)設(shè)計規(guī)范中聲明的正確功能，但是為了保護(hù)混淆密鑰，當(dāng)密鑰不正確時，電路功能并不會被明確聲明，因此，攻擊者可以利用混淆密鑰不正確時引入的未聲明狀態(tài)空間插入木馬。

上述方法中研究者分別利用集成電路設(shè)計外部或內(nèi)部無關(guān)項進(jìn)行硬件木馬設(shè)計。本文展示了一種新的硬件木馬安全威脅，木馬隱藏于電路正常工作條件下無法覆蓋到的可滿足性無關(guān)項中，設(shè)計了針對RSA公鑰密碼系統(tǒng)的輕量級硬件木馬，通過故障注入攻擊，能夠有效激活木馬恢復(fù)公鑰密碼系統(tǒng)的私鑰。在此基礎(chǔ)上，本文提出了一種可有效檢測該新型硬件木馬的防御措施。

3 威脅模型

利用可滿足性無關(guān)項設(shè)計的硬件木馬可在集成電路設(shè)計的不同階段由不可信第三方電路設(shè)計者、EDA工具或芯片制造廠家插入原始設(shè)計中。本文假設(shè)硬件木馬由不可信第三方電路設(shè)計者插入原始設(shè)計中，插入木馬后的設(shè)計以寄存器傳輸級代碼、門級網(wǎng)表、物理芯片或FPGA實現(xiàn)的形式提供給用戶。

本文假設(shè)用戶可以獲得原始設(shè)計的規(guī)范，可依據(jù)設(shè)計規(guī)范對插入木馬后的電路進(jìn)行全面的功能驗證，用戶同樣可以基于現(xiàn)有的木馬檢測方法對其進(jìn)行分析。本文假設(shè)攻擊者能夠獲得插入木馬后的電路設(shè)計的細(xì)節(jié)信息，同時，假設(shè)攻擊者可以控制電路模塊的外部輸入信號、觀測公開的狀態(tài)輸出信號（如芯片忙信號BSY），但無法觀測私鑰和解密結(jié)果等內(nèi)部敏感信息。

4 基于無關(guān)項的硬件木馬安全威脅

本節(jié)介紹公鑰密碼系統(tǒng)所面臨的一種基于集成電路內(nèi)部無關(guān)項的硬件木馬安全威脅。該木馬隱藏在電路正常工作條件下無法滿足的可滿足性無關(guān)項中，插入木馬后的電路設(shè)計和原始設(shè)計完全功能等價。可通過提高時鐘頻率發(fā)起故障注入攻擊來激活木馬。

4.1 利用可滿足性無關(guān)項的木馬設(shè)計

可滿足性無關(guān)項是集成電路設(shè)計內(nèi)部由于扇出重匯聚引入的無關(guān)狀態(tài)[18]，在電路正常工作條件下，可滿足性無關(guān)項無法被滿足。如圖1所示的電路，其布爾函數(shù)表達(dá)式為

其中，內(nèi)部信號(n1, n4)組成可滿足性無關(guān)項，邏輯狀態(tài)(1, 1)是(n1, n4)在正常工作條件下無法滿足的狀態(tài)，n1和n4連接到邏輯門g6。進(jìn)一步可以把可滿足性無關(guān)項擴(kuò)展到全局的概念，即沒有連接到同一個邏輯門的可滿足性無關(guān)項，如圖1中的內(nèi)部信號(n5, n4)。(1, 1)是(n5, n4)在正常工作條件下無法滿足的狀態(tài)。通過布爾可滿足性分析可以搜索到集成電路設(shè)計中的可滿足性無關(guān)項。

Figure 1 Example of satisfiability don't cares

文獻(xiàn)[15]提出了利用可滿足性無關(guān)項的木馬設(shè)計方法。如圖2所示，可滿足性無關(guān)項5、4作為木馬的觸發(fā)信號，分別通過寄存器后作為兩個選擇器的選擇信號，輸出信號邏輯表達(dá)式為

在正常工作條件下，5 =4 = 1的邏輯狀態(tài)無法滿足，式(2)等價于

圖2 利用可滿足性無關(guān)項的木馬設(shè)計

Figure 2 Hardware Trojan leveraging satisfiability don't care

與不完全功能聲明引入的集成電路設(shè)計外部無關(guān)項相比，可滿足性無關(guān)項由電路內(nèi)部扇出重匯聚引入，當(dāng)電路功能被完全聲明時，可滿足性無關(guān)項仍然存在。因此，利用可滿足性無關(guān)項的木馬設(shè)計方法適用于功能被完全聲明的集成電路設(shè)計。

4.2 攻擊模型

本文的攻擊模型利用可滿足性無關(guān)項信號的路徑時延差引入故障攻擊。正常工作條件下，可滿足性無關(guān)項無法滿足，木馬不會被激活。由于兩個木馬觸發(fā)信號路徑存在差異，當(dāng)提高輸入時鐘頻率時，一個木馬觸發(fā)信號到寄存器的時序得不到滿足，而另一個木馬觸發(fā)信號的時序仍然滿足時，兩個觸發(fā)信號的邏輯關(guān)系將間歇性滿足木馬觸發(fā)的條件，如同時為邏輯1，此時木馬被激活。

首先，插入木馬之后的電路在正常時鐘頻率下，完成電路的初始化。然后，逐步提高時鐘頻率發(fā)起故障注入攻擊。當(dāng)木馬觸發(fā)信號中僅一個信號的時序失效時，木馬觸發(fā)條件將間歇性滿足從而激活木馬，此時，攻擊者可以通過觀測電路的公開狀態(tài)輸出信號，獲取敏感信息。之后，繼續(xù)提高時鐘頻率，兩個木馬觸發(fā)信號時序均得不到滿足，此時電路輸出處于隨機(jī)錯誤狀態(tài)，不能根據(jù)輸出信號獲取有用信息。

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

本節(jié)以RSA密碼核為例介紹本文基于可滿足性無關(guān)項的硬件木馬設(shè)計與攻擊方法。

5.1 RSA密碼核木馬設(shè)計和測試流程

利用集成電路設(shè)計內(nèi)部可滿足性無關(guān)項的木馬設(shè)計、測試與攻擊流程如圖3所示。

1) 使用Synopsys Design Compiler對原始設(shè)計進(jìn)行綜合與映射，生成門級網(wǎng)表；然后，使用布爾可滿足性分析工具在網(wǎng)表中搜索可滿足性無關(guān)項。

2) 使用4.1節(jié)中介紹的木馬設(shè)計方法在原始設(shè)計中插入木馬；插入木馬后的設(shè)計使用Vivado進(jìn)行綜合，檢測木馬是否能夠逃避邏輯綜合優(yōu)化。

3) 在正常工作條件下，對插入木馬的設(shè)計和原始設(shè)計進(jìn)行隨機(jī)仿真功能測試和功能一致性檢查。

4) 基于攻擊模型對通過測試的插入木馬的設(shè)計發(fā)起故障注入攻擊。

圖3 硬件木馬設(shè)計、測試與攻擊流程

Figure 3 Hardware Trojan design, testing and attack flow

根據(jù)以上木馬設(shè)計及測試流程，本文選取了日本東北大學(xué)Aoki實驗室發(fā)布的開源1 024位RSA密碼核作為設(shè)計基準(zhǔn)，插入木馬的RSA密碼核結(jié)構(gòu)如圖4所示，主要包括狀態(tài)控制單元、模乘計算單元及存儲單元。RSA密碼核中包含一個密鑰移位寄存器，在狀態(tài)控制單元產(chǎn)生的使能信號控制下，移位輸出密鑰的最高位比特，RSA算法根據(jù)最高位比特控制加/解密運算。本文選取模乘運算單元中的一對可滿足性無相關(guān)項信號作為木馬的觸發(fā)信號，這兩個信號在正常工作條件下不能同時為邏輯1。觸發(fā)信號分別經(jīng)過寄存器后，作為多選器的選擇信號。當(dāng)兩個觸發(fā)信號同時為邏輯1時，木馬被激活，密鑰移位寄存器的最高位泄露至BSY信號。

圖4 包含無關(guān)項木馬的RSA設(shè)計

Figure 4 RSA design with SDC Trojan

插入木馬后的RSA密碼核使用Vivado進(jìn)行邏輯綜合與實現(xiàn)，綜合結(jié)果表明，本文介紹的木馬設(shè)計能夠逃避邏輯綜合優(yōu)化，綜合后仍存在電路中。在相同的約束條件下，插入木馬后的RSA密碼核及原始設(shè)計綜合結(jié)果如表1所示，插入木馬后LUT資源減小0.16%，F(xiàn)F資源增加0.15%，功耗降低了0.57%。進(jìn)一步地，通過線性移位寄存器產(chǎn)生隨機(jī)輸入，進(jìn)行隨機(jī)仿真功能測試。測試結(jié)果表明，正常工作條件下，木馬沒有被激活，插入木馬后的RSA密碼核與原始設(shè)計輸出完全一致，功能等價。

RSA密碼核加/解密過程執(zhí)行模冪運算，當(dāng)密鑰為0時，執(zhí)行一次蒙哥馬利模平方運算，當(dāng)密鑰為1時，執(zhí)行一次蒙哥馬利模乘和一次蒙哥馬利模平方運算，其中，1比特密鑰1的運算時間為1比特密鑰0運算時間的兩倍。

表1 RSA密碼核對木馬設(shè)計的影響

5.2 故障注入攻擊

本文選取Xilinx XCZU9EG FPGA芯片進(jìn)行木馬實現(xiàn)和布局布線后時序仿真。根據(jù)布局布線后時序分析報告，得到插入木馬的RSA密碼核的最高時鐘工作頻率為129.31 MHz。

根據(jù)本文的攻擊模型，首先，在100 MHz時鐘頻率下，對插入木馬后的RSA密碼核和原始設(shè)計分別進(jìn)行布局布線后時序仿真，以保證密碼核正常初始化和密鑰正常加載。100 MHz下，RSA密碼核處于正常工作狀態(tài)，木馬沒有被激活，插入木馬后的RSA密碼核和原始設(shè)計輸出完全一致，仿真波形如圖5(a)所示。然后，逐步提高插入木馬后的RSA密碼核的輸入時鐘頻率，發(fā)起故障注入攻擊。實驗發(fā)現(xiàn)，當(dāng)時鐘頻率為151.51MHz時，Dvld信號產(chǎn)生了邏輯高電平，BSY信號出現(xiàn)了不確定X態(tài)，信號值在X和邏輯1之間切換，此時木馬被激活，32位密鑰下仿真波形如圖5(b)所示。

根據(jù)本文介紹的木馬設(shè)計方案，當(dāng)木馬被激活且當(dāng)前密鑰位為邏輯1時，BSY信號為邏輯1；而當(dāng)前密鑰位為邏輯0時，BSY信號出現(xiàn)X態(tài)。因此，可通過觀測BSY信號是否有X態(tài)確定密鑰為1還是0。進(jìn)一步地，確定1比特密鑰0的加密時長，通過加密時長比較確定密鑰為1和0的比特個數(shù)，進(jìn)而恢復(fù)出密鑰。根據(jù)以上分析得到圖5(b)中32位密鑰為0x00903AD9，與測試向量中設(shè)定的密鑰一致，即通過故障注入攻擊，觀測狀態(tài)輸出信號BSY能夠有效恢復(fù)出密鑰。

151.51 MHz輸入時鐘頻率下，本文進(jìn)一步完成了256位、512位、1024位密鑰的布局布線后時序仿真，其中1024位密鑰下仿真波形如圖5(c)所示，木馬激活下，BSY信號波形在X和邏輯1之間切換，基于上述分析方法，同樣可以恢復(fù)出1024位密鑰。

繼續(xù)提高輸入時鐘頻率，在166.67 MHz輸入時鐘頻率下，足夠長的仿真時間內(nèi)BSY信號一直為邏輯1。此時，RSA密碼算法核有過多路徑發(fā)生時序錯誤，完全失效，密鑰移位寄存器也沒有進(jìn)行移位操作。166.67 MHz 時鐘頻率下32位密鑰的仿真波形如圖5(d)所示，此時，不能根據(jù)BSY信號獲取密鑰信息。進(jìn)一步地，分別對多個不同的32位、256位、1024位密鑰，在151.51 MHz輸入時鐘頻率下對插入木馬的RSA密碼核進(jìn)行布局布線后時序仿真，實驗結(jié)果表明，本文給出的攻擊方法與密鑰長度無關(guān)，木馬被激活后基于上述分析方法可以分別恢復(fù)出32位、256位和 1 024位密鑰。

6 無關(guān)項木馬防御手段

本文展示了一種基于集成電路內(nèi)部可滿足性無關(guān)項的硬件木馬安全威脅。由于木馬隱藏在電路正常工作條件下無法滿足的可滿足性無關(guān)項之中，插入木馬后的電路設(shè)計與原始設(shè)計完全功能等價。本文介紹的硬件木馬采用了兩個木馬觸發(fā)信號和兩級木馬負(fù)載結(jié)構(gòu)，由于在正常工作條件下每個觸發(fā)信號都會翻轉(zhuǎn)，基于邏輯功能測試和翻轉(zhuǎn)概率分析的傳統(tǒng)木馬檢測方法難以實現(xiàn)這種新型硬件木馬檢測。此外，這種新型木馬設(shè)計僅包含兩個寄存器和兩個選擇器，木馬邏輯簡單負(fù)載指紋小，由于缺乏黃金芯片比對，基于側(cè)信道分析[19-20]的方法也難以實現(xiàn)木馬檢測。因此，針對這種新型硬件木馬安全威脅需要提出新的防御手段。

圖5 100MHz、151.51MHz、166.67MHz時鐘下布局布線后時序仿真結(jié)果

Figure 5 Post-implementation timing simulation results under 100MHz, 151.51MHz, 166,67MHz

近年來，研究者提出屬性驅(qū)動的硬件安全驗證方法[21-23]，通過在門級或者寄存器傳輸級基于信息流分析方法建立硬件安全模型，實現(xiàn)對集成電路硬件安全屬性的驗證。本文介紹的硬件木馬設(shè)計中存在密鑰敏感信息到公開狀態(tài)輸出BSY信號的信息流傳播路徑，基于上述硬件安全驗證方法建立插入木馬后RSA密碼核的硬件安全模型，對電路的保密性進(jìn)行驗證，能夠檢測到從密鑰到BSY信號的違反保密性安全屬性的不安全路徑。因此，這種新型的硬件安全驗證方法能夠有效檢測基于無關(guān)項的硬件木馬安全威脅。此外，基于頻率掃描的木馬檢測方法，通過采集不同時鐘頻率下電路時延信息進(jìn)行木馬檢測，由于與本文給出的通過提高時鐘頻率發(fā)起故障注入攻擊的方法類似，在特定的頻率下有可能會激活木馬從而實現(xiàn)木馬檢測。

7 結(jié)束語

本文的研究工作展示了一種新的利用可滿足性無關(guān)項的硬件木馬安全威脅及其防御手段。本文介紹了針對公鑰密碼系統(tǒng)RSA的硬件木馬設(shè)計與實現(xiàn)，實驗結(jié)果表明這種新型硬件木馬能夠逃避邏輯綜合優(yōu)化；在正常工作條件下，木馬不會被激活，插入木馬后的RSA密碼核與原始設(shè)計完全功能等價；通過故障注入攻擊能夠恢復(fù)出1024位RSA密碼核的私鑰。同時，本文提出一種針對該高隱蔽性硬件木馬的防御措施，通過基于信息流分析的硬件安全驗證方法，能夠有效檢測到這種新型硬件木馬引發(fā)的不安全路徑。本文的研究工作有助于硬件設(shè)計者關(guān)注隱藏在集成電路內(nèi)部無關(guān)項中的硬件木馬安全威脅，在設(shè)計階段采取有效的防御手段解決潛在的安全隱患。

[1]TEHRANIPOOR M, KOUSHANFAR F. A survey of hardware Trojan taxonomy and detection[J]. IEEE Design & Test of Computers, 2010, 27(1): 10-25.

[2]LI H, LIU Q, ZHANG J. A survey of hardware Trojan threat and defense[J]. Integration, 2016, 55: 426-437.

[3]KARRI R, RAJENDRAN J, ROSENFELD K, et al. Trustworthy hardware: identifying and classifying hardware Trojans[J]. Computer, 2010, 43(10): 39-46.

[4]BAUMGARTEN A, STEFFEN M, CLAUSMAN M, et al. A case study in hardware Trojan design and implementation[J]. International Journal of Information Security, 2011, 10(1): 1-14.

[5]WAKSMAN A, SUOZZO M, SETHUMANDHAVAN S. FANCI: identification of stealthy malicious logic using Boolean functional analysis[C]//Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security. 2013: 697-708.

[6]HICKS M, FINNICUM M, KING S T, et al. Overcoming an untrusted computing base: detecting and removing malicious hardware automatically[C]//2010 IEEE Symposium on Security and Privacy. 2010: 159-172.

[7]STURTON C, HICKS M, WAGNER D, et al. Defeating UCI: building stealthy and malicious hardware[C]//2011 IEEE Symposium on Security and Privacy. 2011: 64-77.

[8]ZHANG J, YUAN F, XU Q. Detrust: defeating hardware trust verification with stealthy implicitly-triggered hardware Trojans[C]//Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security. 2014: 153-166.

[9]ZHANG J, YUAN F, WEI L, et al. VeriTrust: verification for hardware trust[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2015, 34(7): 1148-1161.

[10]HAIDER S K, JIN C, AHMAD M, et al. Advancing the state-of-the-art in hardware Trojans detection[R]. Cryptology ePrint Archive, Report.

[11]FERN N, KULKARNI S, CHENG K T T. Hardware Trojans hidden in RTL don’t cares-automated insertion and prevention methodologies[C]//2015 IEEE International Test Conference (ITC). 2015: 1-8.

[12]FERN N, CHENG K T. Detecting hardware Trojans in unspeci?ed functionality using mutation testing[C]//2015 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). 2015: 560-566.

[13]NAHIYAN A, XIAO K, YANG K, et al. AVFSM: a framework for identifying and mitigating vulnerabilities in FSMs[C]//Proceedings of the 53rd Annual Design Automation Conference. 2016: 1-6.

[14]KRIEG C, WOLF C, JANTSCH A, et al. Toggle MUX: how X-optimism can lead to malicious hardware[C]//2017 54th ACM/EDAC/IEEE Design Automation Conference (DAC). 2017: 1-6.

[15]HU W, ZHANG L, ARDESHIRICHAM A, et al. Why you should care about don't cares: exploiting internal don't care conditions for hardware Trojans[C]//2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). 2017: 707-713.

[16]MAHMOUD D G, HU W, STOJILOVIC M. X-attack: remote activation of satisfiability don't-care hardware Trojans on shared FPGAs[C]//2020 30th International Conference on Field Programmable Logic and Applications (FPL). 2020: 185-192.

[17]HU W, MA Y, WAND X, et al. Leveraging unspecified functionality in obfuscated hardware for Trojan and fault attacks[C]//2019 Asian Hardware Oriented Security and Trust Symposium (AsianHOST). 2019: 1-6.

[18]DUBBAR C, QU G. Satisfiability don't care condition based circuit fingerprinting techniques[C]//The 20th Asia and South Pacific Design Automation Conference. 2015: 815-820.

[19]MAO B, HU W, ALTHOFF A, et al. Quantitative analysis of timing channel security in cryptographic hardware design[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2017, 37(9): 1719-1732.

[20]NARASIMHAN S, DU D, CHAKRABORTY R S, et al. Hardware Trojan detection by multiple-parameter side-channel analysis[J]. IEEE Transactions on Computers, 2012, 62(11): 2183-2195.

[21]HU W, ARDESHIRICHAM A, GOBULUKOGLU M S, et al. Property speci?c information ?ow analysis for hardware security veri?cation[C]//Proceedings of the International Conference on Computer-Aided Design. 2018: 1-8.

[22]HU W, MAO B, OBERG J, et al. Detecting hardware Trojans with gate-level information-flow tracking[J]. Computer, 2016, 49(8): 44-52.

[23]ARDESHIRICHAM A, TAKASHIMA Y, GAO S, et al. Verisketch: Synthesizing secure hardware designs with timing-sensitive information flow properties[C]//Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS). 2019: 1623-1638.

Design and detection of hardware Trojan based on satisfiability don't cares

WU Lingjuan1,2, ZHU Jiacheng1, TANG Shibo1, TAN Jing1, HU Wei1

1. School of CyberSecurity, Northwestern Polytechnical University, Xi’an 710072, China 2. College of Informatics, Huazhong Agricultural University, Wuhan 430070, China

Hardware Trojans are intended malicious design modifications to integrated circuits,which can be used to launch powerful low-level attacks after being activated. Ａ new security threat of lightweight stealthy hardware Trojans leveraging discrete satisfiability don't care signals was demonstrated. These don't care could not be satisfied under normal operation and thus the circuit design with Trojan is functionally equivalent to the Trojan-free baseline.The attacker could activate the Trojan through simple yet effective fault injection.Experimental results on a 1024-bit RSA cryptographic core show that the proposed hardware Trojan can escape fromlogic synthesis optimization, and that the RSA private key can be retrieved by simply over-clocking the design.A defense technique that can effectively detect such stealthy Trojan design was provided.

hardware security, hardware Trojan, satisfiability don't care, fault injection, Trojan detection

TP309

A

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

2020?11?14；

2020?12?24

胡偉，weihu@nwpu.edu.cn

國家自然科學(xué)基金（62074131）；湖北省自然科學(xué)基金（2020CFB190）

The National Natural Science Foundation of China (62074131), The Natural Science Foundation of Hubei Province (2020CFB190)

武玲娟，朱嘉誠，唐時博，等. 基于可滿足性無關(guān)項的硬件木馬設(shè)計與檢測[J]. 網(wǎng)絡(luò)與信息安全學(xué)報，2021, 7(2): 35-42.

WU L J, ZHU J C, TANG S B, et al. Design and detection of hardware Trojans based on satisfiability don't cares[J]. Chinese Journal of Network and Information Security, 2021, 7(2): 35-42.

武玲娟（1984? ），女，河北邢臺人，博士，西北工業(yè)大學(xué)研究員，主要研究方向為硬件安全與形式化安全驗證。

朱嘉誠（1996? ），男，江蘇常州人，西北工業(yè)大學(xué)碩士生，主要研究方向為硬件安全。

唐時博（1994? ），男，陜西西安人，西北工業(yè)大學(xué)博士生，主要研究方向為硬件安全。

譚靜（1997? ），女，安徽合肥人，西北工業(yè)大學(xué)碩士生，主要研究方向為硬件安全。

胡偉（1982?），男，湖北孝感人，博士，西北工業(yè)大學(xué)副教授，主要研究方向為硬件安全、形式化安全驗證與密碼學(xué)。