STARSS: Small: Detection of Hardware Trojans Hidden in Unspecified Design Functionality

对我们的电子系统和基础设施的安全和可靠性的担忧达到了前所未有的高度。经济因素决定了硅芯片的设计、制造、测试和部署分散在许多目标和利益不同且往往相互冲突的公司和国家。在现代复杂的数字设计中，在许多操作周期中，相当一部分可观察到的输出信号的行为是未指明的，容易受到恶意修改，即所谓的硬件特洛伊木马程序的攻击。由于验证和测试是一个主要瓶颈，目前验证工作的重点是增加对指定功能正确性的信心，这意味着修改未指定行为的特洛伊木马将不会被检测到。本研究的重点是防止和检测硬件木马在未指定的设计空间中的插入。针对这一新出现的强大威胁，该项目推动了硬件验证领域的发展，增加了社会的稳定性。该项目只关注与攻击者可控或可观察信号相关的设计部分，从而有效地遍历未指定的设计空间。在确定潜在危险的功能后，正式方法和基于模拟的方法的混合将确认该功能是否危险，并为验证团队提供具体的跟踪，说明可能的攻击场景。该方法已成功应用于多个寄存器传输级(RTL)设计。此外，该项目将提供允许设计所有者在安全性与木马预防/检测成本之间进行权衡的指标，这些成本包括面积/电源/定时开销、手动工作和分析时间。

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.