8. Formal Approaches to Hardware Trust Verification

Trust establishment in semiconductor designs has become a major challenge for design houses and government since several countries and companies are involved during different stages of a design life cycle. The variety of vendors increases the risk of security vulnerabilities within the supply chain of integrated circuits. Hardware Trojans are malfunctions which can be inserted during any stage of design such as defining specification, designing intellectual properties (e.g., high-level models, RTL modules, and gate-level netlists), layout extraction, and manufacturing. A triggered hardware Trojan can severely affect the integrity and security of the circuit by causing system failures such as deadlock, denial of service, or granting an unauthorized access to secret information. Hardware Trojans are designed in a way that they are inactive most of the time and can be triggered with a very rare input sequence. Therefore, using simulation-based validation is not effective to detect potential Trojans in a design because of the Trojan’s stealthy nature. In other words, the rare trigger conditions may not be tested during validation time, and a Trojan-inserted circuit cannot be differentiated from a Trojan-free one. From the security perspective, a useful validation approach is the one that can prove the correct functionality of a design, nothing more nothing less. Formal methods are promising to prove the security properties; however, the conventional formal methods suffer from scalability concerns. There are several scalable formal approaches to detect hardware Trojans based on satisfiability solvers, model checkers, theorem provers, symbolic algebra, and combination of them. In this chapter, we discuss hardware trust validation techniques based on formal methods.