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

基于可滿足性無關項的硬件木馬設計與檢測

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

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

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

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

1 引言

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

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

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

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

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

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

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

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

2 相關工作

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

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

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

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

3 威脅模型

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

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

4 基于無關項的硬件木馬安全威脅

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

4.1 利用可滿足性無關項的木馬設計

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

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

Figure 1 Example of satisfiability don't cares

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

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

圖2 利用可滿足性無關項的木馬設計

Figure 2 Hardware Trojan leveraging satisfiability don't care

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

4.2 攻擊模型

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

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

5 實驗結果與分析

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

5.1 RSA密碼核木馬設計和測試流程

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

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

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

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

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

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

Figure 3 Hardware Trojan design, testing and attack flow

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

圖4 包含無關項木馬的RSA設計

Figure 4 RSA design with SDC Trojan

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

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

表1 RSA密碼核對木馬設計的影響

5.2 故障注入攻擊

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

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

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

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

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

6 無關項木馬防御手段

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

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

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

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

7 結束語

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

[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

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

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

武玲娟，朱嘉誠，唐時博，等. 基于可滿足性無關項的硬件木馬設計與檢測[J]. 網(wǎng)絡與信息安全學報，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è)大學研究員，主要研究方向為硬件安全與形式化安全驗證。

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

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

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

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