基于模型檢測的硬件木馬檢測技術研究

張啟智，趙毅強，高雅，馬浩誠

基于模型檢測的硬件木馬檢測技術研究

張啟智，趙毅強，高雅，馬浩誠

（天津大學微電子學院，天津 300110）

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

硬件木馬；模型檢測；模型構建；屬性聲明

1 引言

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

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

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

本文對基于模型檢測的硬件木馬檢測技術的應用流程進行了細致的歸納與梳理，對較為常用的模型檢測工具進行了調研，對現有的電路形式化模型構建方法與面向木馬檢測的安全屬性聲明策略進行了詳細的總結。

2 模型檢測技術概述

2.1 基本原理與應用流程

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

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

圖1 模型檢測的應用流程

Figure 1 Application process of model checking

2.2 常用檢測工具

2.2.1 NuSMV

NuSMV（new symbolic model verifyer）[6]是由Carnegie Mellon大學基于SMV（symbolic model verifyer）[7]開發的，以有序二叉判定圖為基礎對有限狀態系統是否滿足基于CTL邏輯描述的屬性約束進行驗證的模型檢測器。經過長時間的使用和更新，NuSMV已經是一個較為成熟的可以同時適用于軟硬件驗證的模型檢測器[8-10]。

NuSMV是一個開放式（這是其最重要的特征）的系統，它的內部由解析器、實例化模塊、編碼模塊、模型檢測模塊等組成。每個模塊實現一組功能，并通過精準定義的接口與其他模塊進行交互，這種設計方式方便用戶根據自己的需要進行調整和修改。

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

2.2.2 UPPAAL

UPPAAL是由瑞典的Uppsala大學和丹麥的Aalborg大學聯合開發用于實時系統驗證的工具[14]，它在通信協議和多媒體領域得到了成功的應用。UPPAAL模型檢測器包括3部分：編輯器、模擬器和驗證器。編輯器是建立時間自動機模型的部分；模擬器是對編輯器中建立的模型進行仿真模擬的部分；驗證器是編寫安全屬性并對其進行驗證的模塊，在這一模塊中，用戶可以利用查詢語言對想要驗證的安全屬性進行編寫。UPPAAL的基本結構如圖3 所示。

圖2 NuSMV代碼結構

Figure 2 The code structure of NuSMV

圖3 UPPAAL的基本結構

Figure 3 The fundamental structure of UPPAAL

在UPPAAL中，一個系統被建模為由多個時間自動機并行組成的網絡。系統的每個狀態在UPPAAL中被定義為位置、時鐘變量以及有界變量的集合。每個時間自動機通過激活邊界或者觸發與其他自動機的同步信號來進入下一個狀態。

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

3 不同種類硬件木馬的模型檢測技術

在利用模型檢測技術進行硬件木馬檢測的過程中，需要對不同種類的硬件木馬根據其功能或結構特點有針對性地展開驗證。硬件木馬根據其功能可分為4類：降低性能型、改變功能型、拒絕服務型、信息泄露型[19]。下面將詳細介紹針對各種類型硬件木馬的模型檢測方法。

3.1 降低性能型硬件木馬的模型檢測技術

降低性能型硬件木馬是指通過改變電路的制造參數（如使電路的主頻下降、低溫下系統癱瘓、電磁輻射變強和電量消耗加速等）來降低電路性能的木馬。對于這種類型的硬件木馬，驗證者在進行模型檢測時，通常考慮對木馬可能攻擊的某些電路參數設定閾值，基于不能超過預設閾值這一特性聲明電路應當滿足的安全屬性。

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

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

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

3.2 改變功能型硬件木馬的模型檢測技術

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

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

用自然語言描述為存儲器接口的地址不得與輸入的16位地址不同。如果出現輸入存儲器接口的地址信息與預設地址信息不同的情況，模型檢測器就會報告驗證失敗并生成反例。

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

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

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

3.3 拒絕服務型硬件木馬的模型檢測技術

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

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

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

3.4 信息泄露型硬件木馬的模型檢測技術

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

He等[29]針對總線結構中植入在從機的讀取總線信息的硬件木馬，提出了由主機存儲給特定從機的信息不應該被泄露給總線上其他從機的安全屬性，首先通過狀態存在性的約束確定了電路的有限狀態機模型中確實存在信息泄露，進而通過狀態可達性的約束確定了硬件木馬被植入的位置，成功檢測出了信息泄露型硬件木馬。

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

4 結束語

近年來，基于模型檢測的硬件木馬檢測技術逐漸成為硬件安全領域研究的熱點。對于面向硬件木馬檢測的模型檢測技術來說，狀態爆炸問題始終是限制其發展的最主要的瓶頸[31]。對于一個具有個邏輯門的電路來說，其所具有的電路狀態數目為2。而如今超大規模集成電路已經被廣泛生產和應用，想要對具有數百萬的邏輯門的電路系統進行完備的模型建立與驗證十分具有挑戰性。

在學術界，緩解狀態爆炸的主要方法有4種：組合推理、抽象技術、對稱、歸納。由于電路設計具有模塊化的特點，面向硬件安全的模型檢測研究者通常采用組合推理的方式來緩解電路建模的狀態爆炸問題，即對電路進行分模塊建?；蛘邔τ谔囟娐纺K而非全部電路進行建模與驗證[29-32]。而分模塊建模的方法必須要考慮的問題是分模塊建模的情況下仍然需要保證模型能夠完備地描述全部電路狀態，針對特定模塊進行建模則需要對硬件木馬的攻擊模式有相當全面的了解和認識。這些問題在一定程度上限制了基于模型檢測的硬件木馬檢測技術的實際應用。

基于上述研究現狀，對電路模型的約簡可作為未來的一個研究方向。例如，硬件電路中擁有許多重復的單元，如存儲單元等，在建模過程中可以通過特定的技術手段對這些重復單元對應的狀態機進行化簡，進而達到減少驗證開銷的目的。

[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]高洪博. 指令誘發型硬件木馬檢測技術研究[D]. 鄭州: 信息工程大學, 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

趙毅強，yq_zhao@tju.edu.cn

國家自然科學基金（61832018）

The National Natural Science Foundation of China(61832018)

張啟智, 趙毅強, 高雅, 等. 基于模型檢測的硬件木馬檢測技術研究[J]. 網絡與信息安全學報, 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? ），男，山東菏澤人，天津大學博士生，主要研究方向為集成電路設計與硬件形式化驗證。

趙毅強（1964? ），男，河北辛集人，博士，天津大學教授、博士生導師，主要研究方向為集成電路安全、混合信號集成電路設計、光電檢測與成像系統設計、傳感器系統設計。

高雅（1998? ），女，遼寧東港人，天津大學碩士生，主要研究方向為數字電路安全。

馬浩誠（1996? ），男，河北滄州人，天津大學博士生，主要研究方向為集成電路設計與硬件安全。