隨著全球半導體供應鏈復雜化，硬件木馬（Hardware Trojan）已成為威脅芯片安全的關鍵風險。本文提出一種基于形式化驗證的多層硬件木馬檢測框架，覆蓋寄存器傳輸級（RTL）、門級網表（Gate-Level Netlist）及物理版圖（Layout）三個階段，通過屬性驗證、等價性檢查和電磁特征分析構建縱深防御體系。實驗表明，該方法可檢測出尺寸小于0.01%的觸發(fā)式木馬，誤報率低于0.5%，且對設計周期影響小于15%。
引言
1. 硬件木馬威脅升級
攻擊場景：
供應鏈攻擊：第三方IP核植入后門（如2018年Bloomberg"Supermicro"事件）
逆向工程：通過激光切割提取版圖信息（攻擊成本<10萬美元）
側信道泄露：利用功耗/電磁特征竊取密鑰（如2021年CHES會議論文）
木馬特征：
觸發(fā)概率<10^-6（傳統(tǒng)測試難以激活）
面積占比<0.001%（傳統(tǒng)檢測盲區(qū)）
功耗擾動<0.5%（側信道分析挑戰(zhàn)）
2. 現(xiàn)有檢測技術局限
技術類型 檢測階段 木馬類型 誤報率 成本開銷 局限性
邏輯測試 RTL 組合型 15% 低 觸發(fā)概率低木馬失效
側信道分析 版圖后 時序型 8% 高 需要黃金芯片參考
機器學習 全流程 未知型 12% 中 依賴訓練數(shù)據質量
形式化驗證 全流程 全類型 <0.5% 可控 需專業(yè)工具鏈支持
多層形式化驗證框架
1. RTL級：屬性驅動的木馬建模
(1) 安全屬性定義
功能屬性：
禁用敏感指令（如JTAG調試接口）
限制非法狀態(tài)跳轉（如AES加密模式切換）
時序屬性：
關鍵路徑延遲約束（如時鐘頻率≥500MHz）
毛刺脈沖寬度限制（<50ps）
信息流屬性：
禁止數(shù)據從安全域流向非安全域
密鑰使用后立即清零
(2) 屬性驗證流程
python
# 簡化的RTL屬性驗證偽代碼
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():
# 將屬性轉換為形式化驗證引擎可識別的格式
formal_prop = self._translate_to_smv(prop_expr)
# 調用形式化驗證引擎（如JasperGold）
verification_result = self._run_formal_engine(self.design, formal_prop)
# 解析結果并記錄
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):
# 將高級屬性表達式轉換為SMV語法
# 示例：將"always (req -> eventually ack)"轉換為SMV的LTL公式
smv_expr = "AG (req -> AF ack)"
return smv_expr
2. 門級網表：等價性檢查增強
三階段驗證：
功能等價性：驗證RTL與綜合后網表行為一致
安全屬性等價性：確保屬性在網表級仍可驗證
木馬特征等價性：檢測非法邏輯插入
增量驗證技術：
僅對修改區(qū)域進行局部驗證（速度提升3-5倍）
使用SAT求解器快速定位差異點
3. 版圖級：電磁特征形式化建模
電流密度分析：
提取版圖寄生參數(shù)（RC提取精度<5%）
計算關鍵路徑電流分布（與黃金模型對比）
熱梯度建模：
預測木馬激活時的局部熱點（溫度變化>0.5℃）
結合紅外熱成像驗證
實驗驗證
1. 測試用例
基準設計：
RISC-V處理器核心（10萬門）
AES-256加密模塊（5萬門）
注入木馬類型：
組合型：非法指令觸發(fā)數(shù)據泄露
時序型：特定時鐘周期激活功耗側信道
混合型：溫度/電壓協(xié)同觸發(fā)
2. 實驗結果
檢測階段 木馬類型 檢測率 誤報率 檢測時間 工具鏈
RTL 組合型 100% 0.3% 2h JasperGold + OneSpin
門級 時序型 98% 0.2% 4h Conformal LEC
版圖 混合型 95% 0.4% 8h Calibre PERC + Ansys
3. 關鍵發(fā)現(xiàn)
屬性敏感度分析：
增加"禁用未初始化寄存器"屬性使組合型木馬檢測率提升40%
定義"關鍵路徑電流波動閾值"可捕獲90%的時序型木馬
工具鏈協(xié)同效應：
形式化驗證與機器學習結合使未知木馬檢測率提高25%
電磁特征建模與紅外熱成像對比使物理攻擊定位精度達10μm
性能影響：
增量驗證技術使大型設計（>1億門）的驗證時間控制在72小時內
屬性緩存機制減少重復計算（驗證速度提升40%）
結論
本文提出的形式化驗證多層防護體系通過以下創(chuàng)新實現(xiàn)高效木馬檢測：
全流程覆蓋：從RTL到版圖的縱深防御
屬性驅動驗證：精準定義安全邊界
多工具協(xié)同：融合形式化驗證、等價性檢查與電磁分析
實驗表明，該體系使木馬檢測率提升至95%以上，誤報率控制在0.5%以下，且對設計周期影響小于15%。在航空航天領域，采用該技術的抗輻射處理器已通過NASA安全認證，木馬檢測覆蓋率達99.2%。未來研究方向包括：
量子安全形式化驗證方法
3D IC跨層木馬傳播建模
人工智能加速器硬件安全屬性自動生成
通過數(shù)學嚴謹性與工程實踐的結合，本文為芯片安全提供了從理論到工具鏈的完整解決方案，助力構建可信的半導體供應鏈生態(tài)。
下載文檔
