一种用于非干涉加速器中木马检测的无黄金模型形式化方法
密码学与安全
2023-12-12 v1
摘要
硬件木马（HTs）在密码加速器等安全关键IP中的威胁带来了严重的安全风险。目前可用的HT检测方法大多依赖于黄金模型和详细的电路规格。它们通常特定于某些HT有效载荷类型，这使得流片前验证变得困难，并导致安全漏洞。我们提出了一种新颖的形式化验证方法，用于在寄存器传输级（RTL）对非干涉加速器进行HT检测，采用标准的形式属性检查。我们的方法保证了对任何时序HT的穷举检测，独立于其有效载荷行为，包括物理侧信道。它不需要黄金模型或设计的功能规格。实验结果证明了在Trust-Hub上可用的加速器中，对所有时序HT（包括具有复杂触发器和有效载荷的HT）的有效且高效的检测。
引用
@article{arxiv.2312.06515,
title = {A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators},
author = {Anna Lena Duque Antón and Johannes Müller and Lucas Deutschmann and Mohammad Rahmani Fadiheh and Dominik Stoffel and Wolfgang Kunz},
journal= {arXiv preprint arXiv:2312.06515},
year = {2023}
}
备注
Accepted for publication at the 27th Design, Automation and Test in Europe Conference (DATE'24), Mar 25-27 2024, Valencia, Spain