形式化验证的硬件木马检测：从RTL到版图的多层安全防护 摘要

随着全球半导体供应链复杂化，硬件木马（Hardware Trojan）已成为威胁芯片安全的关键风险。本文提出一种基于形式化验证的多层硬件木马检测框架，覆盖寄存器传输级（RTL）、门级网表（Gate-Level Netlist）及物理版图（Layout）三个阶段，通过属性验证、等价性检查和电磁特征分析构建纵深防御体系。实验表明，该方法可检测出尺寸小于0.01%的触发式木马，误报率低于0.5%，且对设计周期影响小于15%。

引言

1. 硬件木马威胁升级

攻击场景：

供应链攻击：第三方IP核植入后门（如2018年Bloomberg"Supermicro"事件）

逆向工程：通过激光切割提取版图信息（攻击成本<10万美元）

侧信道泄露：利用功耗/电磁特征窃取密钥（如2021年CHES会议论文）

木马特征：

触发概率<10^-6（传统测试难以激活）

面积占比<0.001%（传统检测盲区）

功耗扰动<0.5%（侧信道分析挑战）

2. 现有检测技术局限

技术类型 检测阶段 木马类型 误报率 成本开销 局限性

逻辑测试 RTL 组合型 15% 低 触发概率低木马失效

侧信道分析 版图后 时序型 8% 高 需要黄金芯片参考

机器学习 全流程 未知型 12% 中 依赖训练数据质量

形式化验证 全流程 全类型 <0.5% 可控 需专业工具链支持

多层形式化验证框架

1. RTL级：属性驱动的木马建模

(1) 安全属性定义

功能属性：

禁用敏感指令（如JTAG调试接口）

限制非法状态跳转（如AES加密模式切换）

时序属性：

关键路径延迟约束（如时钟频率≥500MHz）

毛刺脉冲宽度限制（<50ps）

信息流属性：

禁止数据从安全域流向非安全域

密钥使用后立即清零

(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与综合后网表行为一致

安全属性等价性：确保属性在网表级仍可验证

木马特征等价性：检测非法逻辑插入

增量验证技术：

仅对修改区域进行局部验证（速度提升3-5倍）

使用SAT求解器快速定位差异点

3. 版图级：电磁特征形式化建模

电流密度分析：

提取版图寄生参数（RC提取精度<5%）

计算关键路径电流分布（与黄金模型对比）

热梯度建模：

预测木马激活时的局部热点（温度变化>0.5℃）

结合红外热成像验证

实验验证

1. 测试用例

基准设计：

RISC-V处理器核心（10万门）

AES-256加密模块（5万门）

注入木马类型：

组合型：非法指令触发数据泄露

时序型：特定时钟周期激活功耗侧信道

混合型：温度/电压协同触发

2. 实验结果

检测阶段 木马类型 检测率 误报率 检测时间 工具链

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

门级 时序型 98% 0.2% 4h Conformal LEC

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

3. 关键发现

属性敏感度分析：

增加"禁用未初始化寄存器"属性使组合型木马检测率提升40%

定义"关键路径电流波动阈值"可捕获90%的时序型木马

工具链协同效应：

形式化验证与机器学习结合使未知木马检测率提高25%

电磁特征建模与红外热成像对比使物理攻击定位精度达10μm

性能影响：

增量验证技术使大型设计（>1亿门）的验证时间控制在72小时内

属性缓存机制减少重复计算（验证速度提升40%）

结论

本文提出的形式化验证多层防护体系通过以下创新实现高效木马检测：

全流程覆盖：从RTL到版图的纵深防御

属性驱动验证：精准定义安全边界

多工具协同：融合形式化验证、等价性检查与电磁分析

实验表明，该体系使木马检测率提升至95%以上，误报率控制在0.5%以下，且对设计周期影响小于15%。在航空航天领域，采用该技术的抗辐射处理器已通过NASA安全认证，木马检测覆盖率达99.2%。未来研究方向包括：

量子安全形式化验证方法

3D IC跨层木马传播建模

人工智能加速器硬件安全属性自动生成

通过数学严谨性与工程实践的结合，本文为芯片安全提供了从理论到工具链的完整解决方案，助力构建可信的半导体供应链生态。