發(fā)布時間：2018-05-22 13:50

  本文選題：IP軟核 + 硬件木馬�。� 參考：《江南大學》2017年碩士論文

【摘要】：隨著信息終端智能化程度的不斷提升,對芯片的規(guī)模和功能要求也越來越高,集多功能于一身的片上系統(tǒng)(System on Chip,So C)成為集成電路(Integrated Circuit,IC)設計的主流。考慮成本與效率以及快速搶占市場的需求,So C設計逐步趨向于知識產(chǎn)權(quán)(Intellectual property,IP)化。其中IP軟核與工藝無關(guān),具有較高的靈活性和可移植性,被廣泛的應用在So C的設計中。然而IP軟核多數(shù)由第三方供應商提供,IP軟核的安全性得不到保證,因此必須對IP軟核的安全性進行檢測。含有木馬代碼的IP軟核運用到芯片中,就會在芯片中形成硬件木馬。硬件木馬是對集成電路設計或制造過程中惡意添加或篡改的電路的統(tǒng)稱。硬件木馬能夠在特定條件下觸發(fā),使芯片失效或泄露秘密信息,給信息安全、國家安全等帶來了嚴重的隱患和危害。對應的木馬檢測技術(shù)也成為了硬件安全領域的研究熱點。本文中提出兩種IP軟核檢測方法:一種是利用自主研發(fā)的軟件分析IP核的電路結(jié)構(gòu)和內(nèi)部信號,縮小木馬電路的檢測范圍;另一種是使用定理證明器Coq,通過數(shù)學證明的方法證明IP軟核的安全性。論文主要研究工作如下:(1)介紹硬件木馬的基本概念以及相應的檢測方法,研究了數(shù)據(jù)加密標準(Data Encryption Standard,DES)和高級加密標準(Advanced Encryption Standard,AES)兩種數(shù)據(jù)加密算法。(2)根據(jù)IP軟核木馬隱蔽性強的特點,提出通過分析IP軟核電路結(jié)構(gòu)和內(nèi)部信號來檢測木馬的方法,并使用JAVA語言開發(fā)了專用的硬件木馬檢測軟件。對電路中常見結(jié)構(gòu)模塊進行建模,如累加器、狀態(tài)機、偽隨機序列和線性移位寄存器等,形成軟件木馬庫。然后再利用軟件分析代碼結(jié)構(gòu),梳理信號在模塊中流向,并對信號傳輸?shù)陌踩赃M行分析,進而判斷信號是否被篡改。(3)為進一步分析IP軟核的安全性與后門漏洞,提出利用定理證明器Coq通過數(shù)學證明手段來證明IP軟核安全性的方法。本文中建立了從RTL代碼到Coq代碼的轉(zhuǎn)換規(guī)則,構(gòu)造相應的組合邏輯電路、時序邏輯電路等電路模型,并將DES和AES的verilog代碼按照定義的規(guī)則轉(zhuǎn)換為Coq代碼。IP軟核使用者可依據(jù)轉(zhuǎn)換規(guī)則將RTL代碼轉(zhuǎn)換為與原始電路結(jié)構(gòu)相同的Coq代碼。在轉(zhuǎn)換代碼時,對電路中的信號附加一個密級屬性,并依據(jù)電路的具體結(jié)構(gòu)定義信號的密級。附加的密級屬性是檢測IP軟核中是否存在安全漏洞的重要依據(jù)。(4)用Coq語言定義DES和AES兩種加密算法中涉密信息的安全性定理,使用轉(zhuǎn)換得到的Coq代碼對安全性定理進行證明。實驗結(jié)果表明,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

【相似文獻】

相關(guān)期刊論文 前10條

1 賁可榮;陳火旺;;機器定理證明中的一般問題[J];計算機科學;1992年05期

2 張東摩;朱梧i，

本文編號：1922348