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.