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

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

【相似文獻(xiàn)】

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

1 賁可榮;陳火旺;;機(jī)器定理證明中的一般問(wèn)題[J];計(jì)算機(jī)科學(xué);1992年05期

2 張東摩;朱梧i，

本文編號(hào)：1922348