Concern about the security and reliability of our electronic systems and infrastructure is at an all-time high. Economic factors dictate that the design, manufacturing, testing, and deployment of silicon chips are spread across many companies and countries with different and often conflicting goals and interests. In modern complex digital designs, behaviors at a good fraction of observable output signals for many operational cycles are unspecified and vulnerable to malicious modifications, known as Hardware Trojans. Since verification and testing is a major bottleneck, currently the verification effort is focused on increasing confidence in the correctness of specified functionality, meaning Trojans modifying unspecified behavior will go undetected. This research focuses on preventing and detecting the insertion of Hardware Trojans in unspecified design space. Addressing this emerging yet powerful threat, this project advances the field of hardware verification and increases the stability of our society.
This project traverses the unspecified design space efficiently by focusing analysis only on portions of the design related to attacker controllable or observable signals. After identifying potentially dangerous functionality, a mixture of formal and simulation-based methods confirm if the functionality is dangerous, and provide the verification team with a concrete trace illustrating a possible attack scenario. This methodology has been successfully applied to several register-transfer level (RTL) designs. Additionally, the project will provide metrics allowing design owners to trade-off security with the costs of Trojan prevention/detection, which include area/power/timing overhead, manual effort, and analysis time
|