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

SaTC：STARSS：ICM：不变承载机硬件保障

• 批准号: 1441695
• 负责人: Hai Zhou
• 金额: $ 33.33万
• 依托单位: Northwestern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-10-01 至 2019-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1441695&HistoricalAwards=false
• 关键词: SaTC; STARSS; ICM; Invariant; Carrying

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.

复杂半导体电路和系统的设计需要许多步骤，涉及数百名工程师，并且通常分布在全球多个地点和组织。半导体设计的传统工艺和工具可以确保正确性，即最终产品做它应该做的事情。然而，这些过程不提供关于芯片是否被改变使得其提供未授权访问或控制的置信度。这种不良行为可能是由于设计中的弱点导致无意的侧通道或由于恶意插入的特洛伊木马硬件。本计画发展改善硬体系统可靠性与可信度的技术，其中不变携带机（ICM）方法是以轻量形式化方法为基础，且仅需在传统设计过程中做微小的增加。在这种方法中，每个设计都带有一个用于保证安全性的归纳不变量。当从第三方接收设计时或在复杂的设计过程之后，用户可以检查电路是否感应地满足不变量以及不变量是否满足安全规则。任何违规行为都将引发部署设计的危险信号。该项目开发的原则和工具，检查归纳不变量，调查合适的安全属性，并验证硬件木马基准测试的方法。

项目成果

Using Security Invariant To Verify Confidentiality in Hardware Design

使用安全不变式来验证硬件设计中的机密性

• DOI: 10.1145/3060403.3060456
• 发表时间: 2017
• 期刊: ACM Great Lakes Symposium on VLSI
• 作者: Kong, Shuyu;Shen, Yuanqi;Zhou, Hai
• 通讯作者: Zhou, Hai