寄存器传输级硬件设计信息流建模与安全验证

作     者：秦茂源 侯佳滢 李家乐 唐时博 邰瑜 QIN Maoyuan;HOU Jiaying;LI Jiale;TANG Shibo;TAI Yu

作者机构：西安工业大学计算机科学与工程学院陕西西安710021 西北工业大学网络空间安全学院陕西西安710072 

出 版 物：《西北工业大学学报》 (Journal of Northwestern Polytechnical University)

年 卷 期：2024年第42卷第3期

页      面：506-513页

核心收录：

学科分类：0839[工学-网络空间安全] 08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金(U23B2041,62074131) 西安市碑林区科技计划(GX2136) 陕西省科技计划(2022JM-379)资助 

主　　题：硬件安全 信息流安全模型 信息流安全验证 安全漏洞检测 

摘      要：近年来,已有大量研究证明信息流分析能够有效地对设计安全属性与安全行为进行建模。然而,现有的门级抽象层次的信息流分析方法往往受制于算力和验证效力等因素难以应对大规模设计,而RTL抽象层次的信息流分析方法需借助类型系统等形式化语言对硬件设计进行重新描述。因此,提出了一种寄存器传输级硬件设计信息流建模与安全验证方法。该方法在寄存器传输级功能模型的基础上构建附加安全属性的信息流跟踪逻辑模型,从信息流角度建模设计安全行为和安全属性,并利用EDA测试验证工具,以无干扰为策略捕捉违反安全策略的有害信息流,检测硬件设计安全漏洞。以Trust-Hub硬件木马测试集为测试对象的实验结果表明:所提方法能够有效检测设计内潜藏的硬件木马。