Reverse Engineering Of Integrated Circuits Using Formal Modelling Approach

Abstract

ABSTRACT: An integrated circuit (IC) is a set of electronic devices on a small chip which are the backbone of modern day hardware devices. These chips are now embedded in everything from mobiles and computers to the fighter planes. These chips have billions of components which are made in advanced fabrication facilities. However, the cost of production is up to tens of billions of dollars. The design and manufacturing process of the IC chips has changed in the form of globalization and outsourcing. Due to increasing demand and high cost for production of IC chips, the recent trend in the supply chain consists of a fabless design. In this model the requirements and the design are provided by the company to an outside foundry for manufacturing and testing. The cheap labor in third world countries also attracts a lot of companies for the fabless model. Due to wide-spread increase in applications of embedded systems that use IC’s, their demand has increased in every field of life but low security of these chips is a great problem. Camouflaging is the technique to hide the components of a circuit to save it from hackers, but the recent research showed that these techniques are easily deciphered. The chip piracy and IP infringement are important serious issues in the IC supply chain process as they directly effect the revenue of the semiconductor industry. The aim for reverse engineering is to protect the IC circuits from the malicious modifications, (Intellectual Property) IP violations and infringements. Our work aims at securing these circuits from the IP theft which occur during the fabless manufacturing. The research work is based on reverse engineering of the IC using the formal modeling approach. The netlist xiii Contents of the IC circuit is used for this purpose to model a circuit in the form of a finite state automata. The observations are encoded in the form of temporal logic patterns. The model checking algorithm then iterates through components of a circuit an identifies the hidden gates on the basis of output of (Computation Tree Logic) CTL formula. Finally an application has been developed which takes (Symbolic Model Verifier) SMV files as input and generates the list of hidden components in the circuit. The performance of the application has been tested on benchmark circuits used in previous literature. The results showed that our approach successfully reverse engineer the largest netlist circuit s38584 with 11448 gates in 180 seconds.The developed application can be parallelized in future to tackle larger circuits.