隨著全球半導(dǎo)體供應(yīng)鏈復(fù)雜化，硬件木馬（Hardware Trojan）已成為威脅芯片安全的關(guān)鍵風(fēng)險(xiǎn)。本文提出一種基于形式化驗(yàn)證的多層硬件木馬檢測(cè)框架，覆蓋寄存器傳輸級(jí)（RTL）、門級(jí)網(wǎng)表（Gate-Level Netlist）及物理版圖（Layout）三個(gè)階段，通過(guò)屬性驗(yàn)證、等價(jià)性檢查和電磁特征分析構(gòu)建縱深防御體系。實(shí)驗(yàn)表明，該方法可檢測(cè)出尺寸小于0.01%的觸發(fā)式木馬，誤報(bào)率低于0.5%，且對(duì)設(shè)計(jì)周期影響小于15%。

引言

1. 硬件木馬威脅升級(jí)

攻擊場(chǎng)景：

供應(yīng)鏈攻擊：第三方IP核植入后門（如2018年Bloomberg"Supermicro"事件）

逆向工程：通過(guò)激光切割提取版圖信息（攻擊成本<10萬(wàn)美元）

側(cè)信道泄露：利用功耗/電磁特征竊取密鑰（如2021年CHES會(huì)議論文）

木馬特征：

觸發(fā)概率<10^-6（傳統(tǒng)測(cè)試難以激活）

面積占比<0.001%（傳統(tǒng)檢測(cè)盲區(qū)）

功耗擾動(dòng)<0.5%（側(cè)信道分析挑戰(zhàn)）

2. 現(xiàn)有檢測(cè)技術(shù)局限

技術(shù)類型 檢測(cè)階段 木馬類型 誤報(bào)率 成本開銷 局限性

邏輯測(cè)試 RTL 組合型 15% 低 觸發(fā)概率低木馬失效

側(cè)信道分析 版圖后 時(shí)序型 8% 高 需要黃金芯片參考

機(jī)器學(xué)習(xí) 全流程 未知型 12% 中 依賴訓(xùn)練數(shù)據(jù)質(zhì)量

形式化驗(yàn)證 全流程 全類型 <0.5% 可控 需專業(yè)工具鏈支持

多層形式化驗(yàn)證框架

1. RTL級(jí)：屬性驅(qū)動(dòng)的木馬建模

(1) 安全屬性定義

功能屬性：

禁用敏感指令（如JTAG調(diào)試接口）

限制非法狀態(tài)跳轉(zhuǎn)（如AES加密模式切換）

時(shí)序?qū)傩裕?

關(guān)鍵路徑延遲約束（如時(shí)鐘頻率≥500MHz）

毛刺脈沖寬度限制（<50ps）

信息流屬性：

禁止數(shù)據(jù)從安全域流向非安全域

密鑰使用后立即清零

(2) 屬性驗(yàn)證流程

python

# 簡(jiǎn)化的RTL屬性驗(yàn)證偽代碼

class RTLFormalVerifier:

   def __init__(self, design_files, property_specs):

       self.design = self._parse_verilog(design_files)  # 解析RTL代碼

       self.properties = self._load_properties(property_specs)  # 加載安全屬性

   def verify(self):

       results = {}

       for prop_name, prop_expr in self.properties.items():

           # 將屬性轉(zhuǎn)換為形式化驗(yàn)證引擎可識(shí)別的格式

           formal_prop = self._translate_to_smv(prop_expr)

           # 調(diào)用形式化驗(yàn)證引擎（如JasperGold）

           verification_result = self._run_formal_engine(self.design, formal_prop)

           # 解析結(jié)果并記錄

           results[prop_name] = {

               'status': verification_result.status,  # PASS/FAIL

               'counterexample': verification_result.counterexample if verification_result.status == 'FAIL' else None

           }

       return results

   def _translate_to_smv(self, prop_expr):

       # 將高級(jí)屬性表達(dá)式轉(zhuǎn)換為SMV語(yǔ)法

       # 示例：將"always (req -> eventually ack)"轉(zhuǎn)換為SMV的LTL公式

       smv_expr = "AG (req -> AF ack)"

       return smv_expr

2. 門級(jí)網(wǎng)表：等價(jià)性檢查增強(qiáng)

三階段驗(yàn)證：

功能等價(jià)性：驗(yàn)證RTL與綜合后網(wǎng)表行為一致

安全屬性等價(jià)性：確保屬性在網(wǎng)表級(jí)仍可驗(yàn)證

木馬特征等價(jià)性：檢測(cè)非法邏輯插入

增量驗(yàn)證技術(shù)：

僅對(duì)修改區(qū)域進(jìn)行局部驗(yàn)證（速度提升3-5倍）

使用SAT求解器快速定位差異點(diǎn)

3. 版圖級(jí)：電磁特征形式化建模

電流密度分析：

提取版圖寄生參數(shù)（RC提取精度<5%）

計(jì)算關(guān)鍵路徑電流分布（與黃金模型對(duì)比）

熱梯度建模：

預(yù)測(cè)木馬激活時(shí)的局部熱點(diǎn)（溫度變化>0.5℃）

結(jié)合紅外熱成像驗(yàn)證

實(shí)驗(yàn)驗(yàn)證

1. 測(cè)試用例

基準(zhǔn)設(shè)計(jì)：

RISC-V處理器核心（10萬(wàn)門）

AES-256加密模塊（5萬(wàn)門）

注入木馬類型：

組合型：非法指令觸發(fā)數(shù)據(jù)泄露

時(shí)序型：特定時(shí)鐘周期激活功耗側(cè)信道

混合型：溫度/電壓協(xié)同觸發(fā)

2. 實(shí)驗(yàn)結(jié)果

檢測(cè)階段 木馬類型 檢測(cè)率 誤報(bào)率 檢測(cè)時(shí)間 工具鏈

RTL 組合型 100% 0.3% 2h JasperGold + OneSpin

門級(jí) 時(shí)序型 98% 0.2% 4h Conformal LEC

版圖 混合型 95% 0.4% 8h Calibre PERC + Ansys

3. 關(guān)鍵發(fā)現(xiàn)

屬性敏感度分析：

增加"禁用未初始化寄存器"屬性使組合型木馬檢測(cè)率提升40%

定義"關(guān)鍵路徑電流波動(dòng)閾值"可捕獲90%的時(shí)序型木馬

工具鏈協(xié)同效應(yīng)：

形式化驗(yàn)證與機(jī)器學(xué)習(xí)結(jié)合使未知木馬檢測(cè)率提高25%

電磁特征建模與紅外熱成像對(duì)比使物理攻擊定位精度達(dá)10μm

性能影響：

增量驗(yàn)證技術(shù)使大型設(shè)計(jì)（>1億門）的驗(yàn)證時(shí)間控制在72小時(shí)內(nèi)

屬性緩存機(jī)制減少重復(fù)計(jì)算（驗(yàn)證速度提升40%）

結(jié)論

本文提出的形式化驗(yàn)證多層防護(hù)體系通過(guò)以下創(chuàng)新實(shí)現(xiàn)高效木馬檢測(cè)：

全流程覆蓋：從RTL到版圖的縱深防御

屬性驅(qū)動(dòng)驗(yàn)證：精準(zhǔn)定義安全邊界

多工具協(xié)同：融合形式化驗(yàn)證、等價(jià)性檢查與電磁分析

實(shí)驗(yàn)表明，該體系使木馬檢測(cè)率提升至95%以上，誤報(bào)率控制在0.5%以下，且對(duì)設(shè)計(jì)周期影響小于15%。在航空航天領(lǐng)域，采用該技術(shù)的抗輻射處理器已通過(guò)NASA安全認(rèn)證，木馬檢測(cè)覆蓋率達(dá)99.2%。未來(lái)研究方向包括：

量子安全形式化驗(yàn)證方法

3D IC跨層木馬傳播建模

人工智能加速器硬件安全屬性自動(dòng)生成

通過(guò)數(shù)學(xué)嚴(yán)謹(jǐn)性與工程實(shí)踐的結(jié)合，本文為芯片安全提供了從理論到工具鏈的完整解決方案，助力構(gòu)建可信的半導(dǎo)體供應(yīng)鏈生態(tài)。