| In April1965, Moore made Moore’s Law in an article in the magazine of "e-learning", the industry of semiconductor has a rapid development. IC has been applied to various fields, everywhere, cell phones and other digital products into every person’s life, becoming a product of an integral part of people’s lives. Therefore, people pay more and more attention to the security of integrated circuits.With the continuous development of integrated circuit technology, in order to adapt to the market, reduce design costs and circuits’development cycle, SoC design has become the mainstream of the development of the integrated circuit. IP library is an important part of SoC designs, the use of third-party IP libraries makes the security has become a prominent issue. Integrated circuit design and manufacturing’s separation, relocated to low labor cost areas, many design also outsourced to other design companies, in the integrated circuit design process will be used to provide a variety of electronic design automation software, so semiconductor chips now become easier than ever to malicious modifications in the design process.To address this issue this paper use Coq to prove the safety of circuit. Coq is a theorem proving software, suitable for theorem correctness verification. Firse we build the model of RTL code with Coq, and then the circuit’s RTL code will be converted into Coq using this model. In order to verify whether there are hardware malicious Trojan horse in RTL code or man-made modifications, using Coq to verify the RTL code is consistent with the design, in order to determine the chip’s security.With the development of integrated circuits, many algorithms password fields are implemented using SoC. Coq not only for RTL code level’s security verification, also can be used for cryptographic SoC’s security verification. Combined with the random oracle model, this paper makes a theoretical explanation for the computational security, to lay a theoretical foundation for the next step of work. |
PDF Full Text Request