Security and Trust Verification of IoT SoCs

System-on-Chips (SoCs) are widely used in designing Internet-of-Things (IoT) devices. In order to ensure the security of IoT devices, it is crucial to guarantee the trustworthiness of SoCs. Verifying the trust in SoCs is a major challenge due to their long and globally distributed supply chain. Malicious components can be inserted in different stages of the design cycle. These malicious functionalities work as a backdoor to severely affect the security of the design by giving control of the system to adversaries. The threat creates a critical need for designing new validation approaches that are capable of identifying hidden Trojans. Existing validation techniques cannot efficiently activate and detect Trojans since Trojans are designed to be inactive most of the time and triggered using very rare events. For example, if an adversary wants to hide a Trojan in register-transfer level (RTL) designs, rare branches would be an ideal choice to host Trojans. In this chapter, we introduce a Trojan activation technique that utilizes an effective combination of symbolic simulation as well as concrete execution to identify Trojans that are hidden under rare branches and assignments. The technique is scalable as it considers one path at a time instead of considering the whole design. It uses satisfiability modulo theories (SMT) solvers to solve the path constraints in order to generate a valid test to explore a new path in the design. The exploration continues until all of the rare branches in the design are activated in the search for hidden Trojans.