SaTC: STARSS: ICM: Invariant Carrying Machine for Hardware Assurance

复杂半导体电路和系统的设计需要许多步骤，涉及数百名工程师，并且通常分布在全球多个地点和组织。半导体设计的常规工艺和工具可以保证正确性，也就是说，最终的产品做它应该做的事情。然而，这些过程不能保证芯片是否被改变，从而提供未经授权的访问或控制。这种不受欢迎的行为可能是由于设计中的弱点导致无意的侧通道或由于恶意插入的木马硬件。本项目开发提高硬件系统可靠性和可信度的技术。在这个项目中开发的不变量承载机（ICM）方法是基于轻量级的形式化方法，并且只需要在传统的设计过程中进行少量的添加。在这种方法中，每个设计都带有一个用于保证安全性的归纳不变量。当从第三方接收设计或经过复杂的设计过程后，用户可以检查电路是否感性地满足不变量，不变量是否满足安全规则。任何违规行为都将对部署该设计发出危险信号。该项目开发用于检查归纳不变量的原则和工具，研究合适的安全属性，并通过在硬件木马基准测试上验证该方法。

Design of complex semiconductor circuits and systems requires many steps, involves hundreds of engineers, and is typically distributed across multiple locations and organizations worldwide. The conventional processes and tools for design of semiconductors can ensure the correctness, that is, the resulting product does what it is supposed to do. However, these processes do not provide confidence about whether the chip is altered such that it provides unauthorized access or control. Such undesirable behavior may due to a weakness in the design that results in an unintentional side channel or due to maliciously inserted Trojan hardware. This project develops techniques for improving the reliability and trustworthiness of hardware systems.The Invariant-Carrying Machine (ICM) approach developed in this project is based on light-weight formal methods, and requires only minor additions over the conventional design process. In this approach, each design carries with it an inductive invariant that is used to guarantee the security. When receiving a design from the third party or after a complex design process, the user can check whether the circuit inductively satisfies the invariant and whether the invariant satisfies the security rules. Any violation will raise a red flag for deploying the design. The project develops principles and tools for checking inductive invariants, investigates suitable security properties, and validates the approach by testing on hardware Trojan benchmarks.