[發(fā)明專利]用于檢測硬件木馬的安全斷言自動生成方法

有效

• 申請?zhí)枺?/td>: 201810151701.3
• 申請日: 2018-02-14
• 公開（公告）號: CN108647533B
• 公開（公告）日: 2021-10-08
• 發(fā)明（設計）人: 蔡懿慈;王晨光;周強
• 申請（專利權(quán)）人: 清華大學
• 主分類號: G06F21/71
• 分類號: G06F21/71
• 代理公司: 北京聿宏知識產(chǎn)權(quán)代理有限公司 11372
• 代理人: 吳大建;張杰

本發(fā)明提供一種用于檢測硬件木馬的安全斷言自動生成方法，包括：對待測芯片的寄存器傳輸級網(wǎng)表文件進行仿真，得到仿真運行結(jié)果和仿真運行文件；根據(jù)構(gòu)建的安全性知識庫對仿真運行結(jié)果進行分析，得到疑似硬件木馬電路的信號；針對每個疑似硬件木馬電路的信號執(zhí)行以下步驟：根據(jù)仿真運行文件，推導與疑似硬件木馬電路的信號對應的寄存器傳輸級不變式；根據(jù)構(gòu)建的安全斷言模板知識庫、推導出的寄存器傳輸級不變式以及疑似硬件木馬電路的信號，生成對應于疑似硬件木馬電路的信號的安全斷言。本發(fā)明利用寄存器傳輸級不變式實現(xiàn)安全斷言的自動生成，減輕設計人員的工作量，省時且不易出錯，有效提高了形式驗證檢測硬件木馬的效率。

技術領域

本發(fā)明涉及集成電路的安全性驗證技術領域，尤其涉及一種用于檢測硬件木馬的安全斷言自動生成方法。

背景技術

硬件木馬是指被故意植入電子系統(tǒng)中的特殊模塊以及電路，或者設計者無意留下的缺陷模塊以及電路。這種模塊或電路平日中潛伏在原始電路之中，在特殊條件觸發(fā)下，該模塊或電路能夠被攻擊者利用以實現(xiàn)對原始電路進行有目的性的修改，進而實現(xiàn)破壞性功能，致使原始電路發(fā)生本不該發(fā)生的情況，例如，泄漏信息給攻擊者、使電路功能發(fā)生改變、甚至直接損壞電路。

近年來，由于集成電路工藝技術發(fā)展迅速，使得芯片設計流程變得日益復雜以及制造過程全球化，從而導致集成電路從設計過程到制造過程都很容易被硬件木馬攻擊。為了提高芯片的安全性，需要在設計階段對硬件木馬的存在性進行檢測。

目前的硬件木馬檢測方法，主要包括：功能測試、測試信道分析和形式驗證等。其中，形式驗證由于能夠從算法上窮盡檢查所有隨時間可能變化的輸入值，可以窮盡地搜索芯片設計的狀態(tài)空間，并且不依賴黃金參考模型，因此日益受到重視。

然而，形式驗證所需的斷言目前仍需要人工編寫，這制約了形式驗證在硬件木馬檢測領域的應用。即使對于有經(jīng)驗的設計人員，人工編寫安全斷言也是非常耗時且容易出錯的，這主要是由于：1、缺少形式化的安全設計規(guī)范說明；2、設計人員須熟悉各種形式化語言；3、編寫過程十分依賴主觀判斷，難以產(chǎn)生百分之百覆蓋率的斷言。

因此，為了提高形式驗證檢測硬件木馬的效率，需要提供一種安全斷言自動生成方法。

發(fā)明內(nèi)容

本發(fā)明所要解決的技術問題是：現(xiàn)有技術中形式驗證所需的斷言需要人工編寫，非常耗時且容易出錯，從而導致形式驗證檢測硬件木馬的效率低。

為了解決上述技術問題，本發(fā)明提供了一種用于檢測硬件木馬的安全斷言自動生成方法。

根據(jù)本發(fā)明的實施例，提供了一種用于檢測硬件木馬的安全斷言自動生成方法，包括：

對待測芯片的寄存器傳輸級網(wǎng)表文件進行仿真，得到仿真運行結(jié)果和仿真運行文件；

根據(jù)構(gòu)建的安全性知識庫對所述仿真運行結(jié)果進行分析，得到疑似硬件木馬電路的信號；

針對每個疑似硬件木馬電路的信號執(zhí)行以下步驟：

根據(jù)所述仿真運行文件，推導與所述疑似硬件木馬電路的信號對應的寄存器傳輸級不變式；

根據(jù)構(gòu)建的安全斷言模板知識庫、推導出的寄存器傳輸級不變式以及所述疑似硬件木馬電路的信號，生成對應于所述疑似硬件木馬電路的信號的安全斷言；

其中，所述安全性知識庫中保存有所述待測芯片中硬件木馬電路的信號特征；每個類型的信號特征對應一個寄存器傳輸級不變式計算式；所述安全斷言模板知識庫中保存有與各個寄存器傳輸級不變式計算式對應的安全斷言模板。

優(yōu)選地，該方法還包括離線或在線構(gòu)建安全性知識庫，其包括：

分析插入至所述待測芯片中的硬件木馬電路中觸發(fā)邏輯單元和功能邏輯單元的信號的信號特征，并基于分析結(jié)果構(gòu)建安全性知識庫。