论文部分内容阅读
随着信息终端智能化程度的不断提升,对芯片的规模和功能要求也越来越高,集多功能于一身的片上系统(System on Chip,So C)成为集成电路(Integrated Circuit,IC)设计的主流。考虑成本与效率以及快速抢占市场的需求,So C设计逐步趋向于知识产权(Intellectual property,IP)化。其中IP软核与工艺无关,具有较高的灵活性和可移植性,被广泛的应用在So C的设计中。然而IP软核多数由第三方供应商提供,IP软核的安全性得不到保证,因此必须对IP软核的安全性进行检测。含有木马代码的IP软核运用到芯片中,就会在芯片中形成硬件木马。硬件木马是对集成电路设计或制造过程中恶意添加或篡改的电路的统称。硬件木马能够在特定条件下触发,使芯片失效或泄露秘密信息,给信息安全、国家安全等带来了严重的隐患和危害。对应的木马检测技术也成为了硬件安全领域的研究热点。本文中提出两种IP软核检测方法:一种是利用自主研发的软件分析IP核的电路结构和内部信号,缩小木马电路的检测范围;另一种是使用定理证明器Coq,通过数学证明的方法证明IP软核的安全性。论文主要研究工作如下:(1)介绍硬件木马的基本概念以及相应的检测方法,研究了数据加密标准(Data Encryption Standard,DES)和高级加密标准(Advanced Encryption Standard,AES)两种数据加密算法。(2)根据IP软核木马隐蔽性强的特点,提出通过分析IP软核电路结构和内部信号来检测木马的方法,并使用JAVA语言开发了专用的硬件木马检测软件。对电路中常见结构模块进行建模,如累加器、状态机、伪随机序列和线性移位寄存器等,形成软件木马库。然后再利用软件分析代码结构,梳理信号在模块中流向,并对信号传输的安全性进行分析,进而判断信号是否被篡改。(3)为进一步分析IP软核的安全性与后门漏洞,提出利用定理证明器Coq通过数学证明手段来证明IP软核安全性的方法。本文中建立了从RTL代码到Coq代码的转换规则,构造相应的组合逻辑电路、时序逻辑电路等电路模型,并将DES和AES的verilog代码按照定义的规则转换为Coq代码。IP软核使用者可依据转换规则将RTL代码转换为与原始电路结构相同的Coq代码。在转换代码时,对电路中的信号附加一个密级属性,并依据电路的具体结构定义信号的密级。附加的密级属性是检测IP软核中是否存在安全漏洞的重要依据。(4)用Coq语言定义DES和AES两种加密算法中涉密信息的安全性定理,使用转换得到的Coq代码对安全性定理进行证明。实验结果表明,Coq能成功检测出软核中以代码形式存在的硬件木马。