保障型设计：运用功能验证工具抵御 3PIP 中的硬件木马威胁
密码学与安全
2025-09-09 v1
摘要
第三方知识产权核是现代片上系统与集成电路设计的基本构建模块。然而，这些设计组件通常来自不同信任等级的供应商，并可能包含未文档化的设计功能。由于缺乏黄金参考，区分此类隐蔽的轻量级恶意设计修改可能是一项具有挑战性的任务。在这项工作中，我们迈向保障型设计，开发了一种利用硬件设计者熟悉的功能验证工具与语言来识别并预防硬件木马的方法。我们导出映射到现场可编程门阵列技术库的综合设计网表，并在查找表（LUTs）粒度上执行翻转与覆盖率分析，以识别虚假信号与单元。我们自动提取并形式化证明与翻转和覆盖率相关的属性，从而能够还原木马触发条件。我们进一步提供了一种通过重新配置已确认的恶意 LUT 来阻止木马激活的解决方案。实验结果已表明，我们的方法能够检测并缓解 Trust-Hub 以及近期报道的无关项（don't care）木马。
引用
@article{arxiv.2311.12321,
title = {Design for Assurance: Employing Functional Verification Tools for Thwarting Hardware Trojan Threat in 3PIPs},
author = {Wei Hu and Beibei Li and Lingjuan Wu and Yiwei Li and Xuefei Li and Liang Hong},
journal= {arXiv preprint arXiv:2311.12321},
year = {2025}
}