摘要：針對集成電路在RTL代碼級設計階段由于使用第三方IP軟核引入的安全性問題，現有的功能測試方法較難實現全覆蓋檢測無法保障電路安全性。本文在已有基于攜帶證明代碼思想的基礎上改進提出一種安全性驗證方法。該方法結合形式化驗證平臺coq，運用形式化邏輯描述電路代碼和安全性假設，構造證明過程并采用系統的證明檢查器驗證證明過程。通過在DES電路代碼的實驗，說明了該驗證方法能有效檢測出電路中后門路徑類型的硬件木馬。相比較于測試類方法覆蓋率不能達到100%而無法確定電路是非安全性，本文提出的方法可以確定電路是安全或非安全，能夠保證電路代碼級的安全可信性。

　　關鍵詞：第三方IP核;硬件木馬;攜帶證明的代碼;形式化驗證

　　隨著SoC設計技術的發展，為縮短開發周期，可復用的IP核在SoC設計中被廣泛應用。大量第三方IP軟核的使用，使得硬件木馬攻擊者有可乘之機，導致電路有泄露信息、功能癱瘓、喪失自主控制能力等威脅[1-3]，因此需要強有力的檢測手段確保第三方IP軟核的可信性。

　　目前，針對IP軟核的檢測方法，主要有基于測試[4-6]和形式化驗證方法[7-8]。基于測試的方法只有測試到電路設計有不符合需求之處時才能說明電路是不可靠的，是一種證偽的思想，由于測試向量并不能遍歷所以可能輸入向量，而當沒有測試到不符合項時不能確定電路是絕對安全可靠的，因此這種證偽的方法具有一定局限性。形式化驗證方法有3種類型：模型驗證、等價驗證和屬性驗證。模型驗證當電路規模較大時存在空間爆炸問題，不適合用于大規模電路[9-10]。

　　等價驗證是指電路設計每個層次的功能針對原有功能目標都需要去進行驗證，如驗證RTL級和綜合后電路之間的相等性[11]。屬性驗證用于第三方IP核的信號安全性驗證，通常結合IP核特定屬性、測試覆蓋率或門級網表，來驗證IP核是否含木馬電路[12]。本文在屬性驗證時引入了攜帶證明代碼思想同時作出了改進，并在形式化驗證平臺上進行安全性驗證。

　　1驗證方法

　　1.1攜帶證明代碼原理

　　基于攜帶證明代碼的思想進行安全性驗證，主要分成兩階段：第一階段是IP提供者與IP使用者關于IP核屬性達成一致觀點，提供者不僅提供IP核代碼，同時提供IP核滿足安全屬性的證明過程[13-14]。這些屬性和證明過程需要與IP核獨立開描述，采用形式化表示提供給IP使用者。第二階段是IP使用者在使用IP核時，必須先驗證IP核代碼是否發生篡改，只有通過形式化證明驗證的IP核才被認為是安全可靠的。由于電路的數據安全屬性一旦被形式化證明了，就不可能會插入硬件木馬使電路屬性不改變而且證明驗證能夠通過。

　　因此，本文提出的方法能夠給IP軟核使用者提供一種簡單有效的機制進行安全性驗證，避免IP設計階段引入的安全威脅。根據攜帶證明代碼的原理進行IP軟核的安全性驗證時，需要采用形式化描述方法表示屬性和證明過程，即形式化驗證技術。形式化驗證技術是指在特定的形式系統(通常是數理邏輯系統)中對程序及其執行環境構造形式模型，并在形式模型上對代碼的各種特性進行邏輯推理和證明[15]。相比于其他的驗證技術，形式化驗證技術優勢在于它是一種保證結果完備性的技術，也就是說如果能夠證明電路代碼滿足特定的屬性，那么相應的集成電路就一定滿足這個性質，是一個證真的過程。

　　1.2形式化驗證流程

　　攜帶證明代碼思想進行IP軟核安全性驗證時需要IP軟核提供者和使用者共同合作，其中主要是IP軟核提供者要提供安全性屬性的證明過程，由于SoC設計過程中常常會使用多個廠家提供的IP核，我們不可能要求每個IP提供者都提供屬性證明過程，而且這些證明過程都使用同樣的形式化描述語言。由于安全屬性的定義是通過邏輯功能定義的，整個證明過程構造可以通過邏輯推理來得到。

　　在驗證證明過程時，若有子定理與電路設定不符，表示IP軟核中有木馬電路;否則定理證明過程通過，IP核滿足安全屬性，因此我們在已有基于攜帶證明代碼思想的基礎上改進提出一種安全性驗證方法，所有驗證工作都由IP使用者執行。

　　分為兩階段，第一階段是確定安全屬性和證明過程，即根據需求確定IP核應滿足的屬性并構造屬性證明的過程;第二階段是檢查證明過程的正確性，即根據證明過程對屬性進行推導，若證明檢查過程成立則IP核滿足屬性，若證明不通過表示IP核不滿足安全屬性，存在木馬電路。由于大規模電路的推導過程復雜，人工推導容易出錯，所以第二階段借助已有形式化驗證工具完成。我們采用計算機輔助定理證明工具coq(CoqDevelopmentTeam)作為開發平臺[16]。選用coq平臺的語言Gallina作為形式化描述語言表示電路、屬性和證明過程，證明的邏輯基礎選用歸納構造演算作為驗證框架的元邏輯。

　　coq系統主要由證明開發系統和證明檢查器構成。證明開發系統中我們可以用Gallina語言設置相對應的安全屬性規范，而且可以使用證明策略構造證明過程。證明檢查器主要用來驗證被形式化表示的安全性規范即定理，能否通過證明過程文件來完成證明。

　　在證明過程中，coq采用反向推導的方法構造證明，即當將某個策略應用到目標程序上時，系統會根據策略產生相對應的子目標，每一個子目標都使用數字進行標識，通過對各個子目標的證明來完成整個程序的證明過程。在將Coq內安全策略應用到一個給定目標時，系統會對應用該策略需要符合的前提條件進行比對，如果比對結果是不符合，那么則該策略就會應用失敗。兩者協調可以非常有效地證明從電路代碼中抽取的定理的正確性。

　　2實例驗證

　　為了證明本文中提出的檢測方法能夠驗證電路中的木馬，我們采用DES電路的Verilog代碼作為驗證對象。DES作為國際通用的加密算法，對信號的保密性區分要求較高，將DES算法的Verilog代碼描述作為待驗證安全屬性的IP核具有很高的代表性。接下來，我們將說明如何運用coq形式化邏輯表示DES電路和電路屬性[17]，在coq開發系統中描述待證明的屬性并構造證明過程，最后運用證明檢查器分析證明過程得出結論。

　　2.1邏輯描述的相關定義

　　根據前述驗證方法的描述可知，本文提出的驗證方法是在coq驗證平臺上完成，由于該驗證平臺無法對Verilog代碼進行識別，需要將DES算法等價轉化為coq開發平臺能夠識別的Gallina語言描述，同時待驗證屬性和證明過程都需要用Gallina語言描述。將Verilog代碼轉化為coq系統描述需要研究的定義的內容包括：描述電路的形式化模型和代碼轉化規則。描述電路的形式化模型主要定義了：信號的定義、信號的運算規則、電路表達式類型的描述。

　　2.2安全性設定

　　驗證DES算法電路的安全屬性時，主要是驗證電路中沒有信息泄露路徑，即需要保密的信息如明文和密鑰，經過加密電路后，在輸出的密文中不含有保密信息。因此假定：對信號添加密級屬性，信號的密級有secure、non_secure兩種，同時對信號添加密級。Inductivesecurity:=secure|non_secure.Definitionbus:=nat->(bus_label*security).需要保密的信息，即明文和密鑰是秘密的信號。在電路運算時電路信號的密級屬性會發生變化，變化可能秘密信號變成非密信號、密級不發生改變或者非密信號變成秘密信號，對應了降密，維持或者升密3種運算。在加密電路中，我們認為移位變換是一種降密運算，其他電路運算都是維持密級不變的運算。

　　2.3驗證

　　在coq系統中證明電路的安全性，需要將上述安全性假設轉化為待證明的定理，即在DES電路中輸入desIn，key密級為secure，輸出信號desout密級為non_secure，轉化為coq系統描述如下：Axiomsecret_key:forall(c:nat)，bus_senkeyc=secure.Axiomsecret_desIn:forall(c:nat)，bus_send⁃esInc=secure.Theoremno_leaking_des:forall(c:nat)，bus_send⁃esoutc=non_secure.由于密鑰生成器為保持密級不變的電路模塊，所以有K_sub的密級為secure，轉化為coq系統描述如下：Axiomsecret_K_sub:forall(c:nat)，bus_senK_subc=secure.確定輸入假設和待證明定理后，需要構造證明過程，coq系統采用的推理邏輯是反向的歸納構造演算的邏輯。

　　所以需要從待證明定理開始展開，即desout開始展開，從電路的輸出端開始往前推算，直到找到與輸入信號相關時可直接進行比對，證明過程完成。在構造證明過程中，可以運用coq系統提供的證明策略描述每一步證明過程，如展開desout用unfolddesout，簡化表達式用simpl。形式化驗證需要采用coq系統的證明檢查器進行驗證，驗證內容包括轉化后的電路的邏輯描述的準確性，待證明定理準確性和證明過程演算。其中證明過程演算中一旦發生與假設定理矛盾就會證明失敗，則說明電路代碼中有木馬電路。

　　3結論

　　SoC設計時第三方IP軟核的使用，導致在RTL代碼級設計階段極易被植入硬件木馬，為及早從設計源頭發現電路中被插入的硬件木馬，本文提出了基于攜帶證明代碼思想改進的形式化驗證方法。通過在DES電路上驗證說明，該方法是對電路進行代碼級分析，能有效檢測出改變電路中信號路徑類型的硬件木馬。

　　相比較于測試類證偽的方法，本文提出方法是一種完備的證真的方法，可靠性更高。形式化驗證方法在驗證軟硬件可靠性方面的應用已較為成熟，在驗證電路代碼級安全性方面的研究是一個較新的研究方向，具體的技術細節如電路轉化模型、代碼的自動化轉化等都需要深入研究，這些技術的成熟必將提高形式化驗證的可適用范圍和易用性。

　　參考文獻：

　　[1]SalmaniH，TehranipoorM.Analyzingcircuitvul⁃nerabilitytohardwareTrojaninsertionatthebehav⁃iorallevel[J].IEEEInternationalSymposiumonDefectandFaultToleranceinVLSIandNanotech⁃nologySystems，2013，79(2):190-195.

　　[2]李杰，肖立伊，赤誠，等.基于SoC系統的IP核評測平臺開發[J].微電子學與計算機，2017，34(6):45-48.

　　[3]周昱，于宗光.硬件木馬威脅與識別技術綜述[J].信息網絡安全，2016(1):11-17.

　　[4]ReeceT，RobinsonWH.Detectionofhardwaretrojansinthird-partyintellectualpropertyusinguntrustedmodules[J].IEEETransactionsonComputer-aidedDesignofIntegratedCircuitsandSystems，2016，35(3):357-366.

　　[5]WaksmanA，SuozzoM，SethumadhavanS.FAN⁃CI:identificationofstealthymaliciouslogicusingbooleanfunctionalanalysis[C]//ProceedingsofAC⁃MSigsacConferenceonComputer&Communica⁃tionsSecurity，2013:697-708.

　　[6]閆淑梅，鄒明亮.IP軟核測試策略及驗證方法研究[J].電子設計工程，2013，21(4):98-100.

　　[7]RajendranJ，DhandayuthapanyA，VedulaV，etal.Formalsecurityverificationofthirdpartyintellectualpropertycoresforinformationleakage[C]//Proceedingsof29thInternationalConferenceonVLSIDesign&15thInternationalConferenceonEmbeddedSystems.2016:547-552.

　　相關刊物推薦：《信息網絡安全》論文發表官方網站 是公安部主管，公安部第三研究所主辦的綜合性專業月刊，是公安部公共信息網絡安全監察局及其下屬各網絡安全監察部門對外宣傳的窗口。