一种基于门级污染标签跟踪模型的硬件安全漏洞检测方法

摘要

本申请公开了一种基于门级污染标签跟踪模型的硬件安全漏洞检测方法，包括：将以硬件描述语言描述的硬件设计综合为门级网表；构建污染标签跟踪逻辑库；基于污染标签跟踪逻辑库和门级网表，建立污染标签跟踪逻辑模型；形式化描述期望信息流安全属性，形成断言；将污染标签跟踪逻辑库、污染标签跟踪逻辑模型和断言作为输入，进行形式化安全验证，得到验证结果；分析验证结果。本申请的方法减少了硬件设计语言和形式化语言之间语句转换所产生的额外设计开销，提高了效率，能够有效地甄别违反信息流安全策略的安全漏洞，具有适用性强的特点，便于与现有的形式化工具相整合，能够以极高的验证覆盖率验证期望的信息流安全属性。