[發明專利]基于有界模型的微型木馬檢測方法

有效

• 申請號: 201810437259.0
• 申請日: 2018-05-09
• 公開（公告）號: CN108595986B
• 公開（公告）日: 2021-10-08
• 發明（設計）人: 江建慧;張穎;于露
• 申請（專利權）人: 同濟大學
• 主分類號: G06F21/76
• 分類號: G06F21/76;G01R31/28
• 代理公司: 上海科盛知識產權代理有限公司 31225
• 代理人: 翁惠瑜

1.一種基于有界模型的微型木馬檢測方法，其特征在于，包括以下步驟：

1)將一批具有相同功能的芯片分為訓練組和測試組；

2)對所述訓練組進行物理檢測，提取可疑電路對；

3)使用有界模型檢驗法對所述可疑電路對進行功能檢測，根據檢測結果判斷是否存在微型木馬，并建立基于反例的測試序列庫；

4)以所述測試序列庫對測試組進行微型木馬檢測；

所述使用有界模型檢驗法對所述可疑電路對進行功能檢測具體為：

301)判斷是否存在可疑電路對，若是，則執行步驟302)，若否，則結束；

302)取出一可疑電路對，用SMV語言描述所述可疑電路對，形成兩個電路模型，以相同信號作為所述兩個電路模型的輸入；

303)設置所述兩個電路模型的LTL屬性；

304)采用有界模型檢驗法進行LTL屬性驗證，判斷是否存在反例，若是，則采集所述反例加入反例集合中，若否，則判定可疑電路對不存在微型木馬，返回步驟301)。

2.根據權利要求1所述的基于有界模型的微型木馬檢測方法，其特征在于，所述物理檢測具體為：

切割芯片模制涂層，顯示出電路表面結構，重復掃描芯片的表面，獲得芯片布局。

3.根據權利要求2所述的基于有界模型的微型木馬檢測方法，其特征在于，所述提取可疑電路對具體為：

對比所述訓練組中每一芯片對的芯片布局，若存在某一芯片對的兩個芯片布局不同，則從所述芯片布局中提取每個含有差異的電路以及其周圍電路，形成可疑電路對。

4.根據權利要求1所述的基于有界模型的微型木馬檢測方法，其特征在于，步驟304)具體為：

341)初始化有界模型檢驗法的邊界值k；

342)判斷通過有界模型檢驗法是否找到一個反例，若是，則采集所述反例加入反例集合中，若否，則執行步驟343)；

343)判斷當前邊界值k是否大于或等于界限閾值N，若是，則返回步驟301)，若否，則令k＝k+i，i為設定步長，返回步驟342)。

5.根據權利要求4所述的基于有界模型的微型木馬檢測方法，其特征在于，所述邊界值k的初始值為芯片的時序電路的時序深度。

6.根據權利要求1所述的基于有界模型的微型木馬檢測方法，其特征在于，所述建立基于反例的測試序列庫具體為：

獲得反例對原始電路功能的影響，確定微型木馬的實際功能，建立一個包含微型木馬功能和芯片輸入的數據庫，作為測試序列庫。