软核IP的安全性分析与后门漏洞检测

发布时间：2018-05-22 13:50

本文选题：IP软核 + 硬件木马　；参考：《江南大学》2017年硕士论文

【摘要】：随着信息终端智能化程度的不断提升,对芯片的规模和功能要求也越来越高,集多功能于一身的片上系统(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能成功检测出软核中以代码形式存在的硬件木马。
[Abstract]:With the improvement of the intelligence of information terminal, the scale and function of the chip are required more and more. The system on chip so C (integrated circuit IC) design has become the mainstream of integrated circuit design. Considering the cost and efficiency as well as the demand for rapid market capture, the design of so C is gradually moving towards intellectual property IP. IP soft core is process independent and has high flexibility and portability, so it is widely used in the design of so C. However, the security of IP soft core is not guaranteed by the third party provider, so it is necessary to check the security of IP soft core. The IP soft core that contains Trojan horse code applies to chip, can form hardware Trojan horse in chip. Hardware Trojans are the general names of circuits that are maliciously added or tampered with in the process of IC design or manufacture. The hardware Trojan can trigger under certain conditions, make the chip invalid or leak secret information, and bring serious hidden trouble and harm to information security and national security. The corresponding Trojan horse detection technology has also become a research hotspot in the field of hardware security. In this paper, two detection methods of IP soft core are put forward: one is to analyze the circuit structure and internal signal of IP core by using the software developed by ourselves, so as to reduce the detection range of Trojan horse circuit; The other is to prove the security of IP soft core by means of mathematical proof using theorem prover Coq. The main research work of this paper is as follows: (1) introducing the basic concept of the hardware Trojan horse and the corresponding detection methods. This paper studies two data encryption algorithms, data Encryption Standard (des) and Advanced Encryption Standard (AES2). According to the strong concealment of IP soft core Trojan horse, this paper puts forward a method to detect Trojan horse by analyzing the structure and internal signal of IP soft nuclear power system. And use JAVA language to develop a special hardware Trojan detection software. The common structural modules in the circuit, such as accumulator, state machine, pseudorandom sequence and linear shift register, are modeled to form the software Trojan library. Then using software to analyze the code structure, comb the signal flow in the module, and analyze the security of signal transmission, and then determine whether the signal has been tampered with. This paper presents a method to prove the security of IP soft core by means of mathematical proof using theorem prover Coq. In this paper, the conversion rules from RTL code to Coq code are established, and the corresponding combinatorial logic circuits, sequential logic circuits and other circuit models are constructed. According to the defined rules, the verilog code of DES and AES can be converted into Coq code. IP soft core user can convert RTL code into Coq code with the same structure as original circuit according to the conversion rule. In the process of code conversion, a secret class attribute is attached to the signal in the circuit, and the secret level of the signal is defined according to the specific structure of the circuit. The additional cryptographic attribute is an important basis for detecting the existence of security vulnerabilities in IP soft core. (4) the security theorem of secret information in DES and AES encryption algorithms is defined by Coq language, and the security theorem is proved by the transformed Coq code. The experimental results show that Coq can successfully detect the hardware Trojan horse in the form of code in the soft core.
【学位授予单位】：江南大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TN407

【相似文献】