SaTC: STARSS: Small: Property Driven Hardware Security

SaTC：STARSS：小型：财产驱动的硬件安全

• 批准号: 1718586
• 负责人: Ryan Kastner
• 金额: $ 32.6万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-10-01 至 2022-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1718586&HistoricalAwards=false
• 关键词: SaTC; STARSS; Small; Property; Driven

The task of designing modern hardware that is impervious to any and every security attack is almost impossible to achieve. It is extremely hard to ensure that these complex, multi-billion transistor systems are functionally correct, let alone secure. Thus, it should not be surprising that there are a large and growing number of attacks that target hardware vulnerabilities. The state of the art for hardware design security relies heavily on functional verification, manual inspection, and code review to identify security vulnerabilities. This labor-intensive process does not scale, it significantly reduces productivity, and provides no guarantee that a security flaw will be identified. Continuing with the status quo will undoubtedly leave hardware designs susceptible to attacks manifested through hardware, firmware, and software vulnerabilities. This project develops a property driven approach to hardware security, which enables automatic verification of security properties on a hardware design. The project encompasses three major research goals: creating expressive security property languages, building comprehensive models that analyze the security of a hardware design, and generating tools that can verify security properties in an efficient and scalable manner. The investigators address these challenges by developing models that enable the specification of a wide variety of security properties. The project builds a novel security property specification languages leveraging these models, and develops new techniques that enable the verification of these properties using existing formal solvers, simulation environments, and emulation platforms. Finally, they address the usability of this property driven approach by verifying security properties on different hardware designs.

设计现代硬件的任务几乎无法实现任何安全攻击。很难确保这些复杂的数十亿个晶体管系统在功能上是正确的，更不用说安全了。因此，毫不奇怪的是，针对硬件漏洞的越来越多的攻击数量越来越多。硬件设计安全的最新技术在很大程度上依赖于功能验证，手动检查和代码审查以识别安全漏洞。这个劳动力密集型过程并不能大大降低生产率，并且不能保证将确定安全缺陷。继续保持现状，无疑会留下容易受到通过硬件，固件和软件漏洞表现出的攻击的硬件设计。该项目开发了一种以属性为导向的硬件安全性的方法，该方法可以自动验证硬件设计上的安全属性。该项目涵盖了三个主要的研究目标：创建表现力的安全性属性语言，构建分析硬件设计安全性的综合模型，并生成可以以高效且可扩展的方式验证安全属性的工具。研究人员通过开发模型来解决这些挑战，从而使各种安全性属性规范。该项目构建了利用这些模型的新型安全属性规范语言，并开发了使用现有正式求解器，仿真环境和仿真平台验证这些属性的新技术。最后，他们通过验证不同硬件设计上的安全性属性来解决此属性驱动方法的可用性。

项目成果

Clepsydra: Modeling timing flows in hardware designs

• DOI: 10.1109/iccad.2017.8203772
• 发表时间: 2017-11
• 期刊: 2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)
• 作者: Armaiti Ardeshiricham;Wei Hu;R. Kastner

Holistic Power Side-Channel Leakage Assessment: Towards a Robust Multidimensional Metric

整体电源侧通道泄漏评估：迈向稳健的多维指标

• DOI: 10.1109/iccad45719.2019.8942098
• 发表时间: 2019
• 期刊: International Conference on Computer Aided Design (ICCAD
• 作者: Althoff, Alric;Blackstone, Jeremy;Kastner, Ryan
• 通讯作者: Kastner, Ryan

VeriSketch: Synthesizing Secure Hardware Designs with Timing-Sensitive Information Flow Properties

VeriSketch：综合安全硬件设计与时间敏感信息流属性

• DOI: 10.1145/3319535.3354246
• 发表时间: 2019
• 期刊: ACM SIGSAC Conference on Computer and Communications Security
• 作者: Ardeshiricham, Armaiti;Takashima, Yoshiki;Gao, Sicun;Kastner, Ryan
• 通讯作者: Kastner, Ryan

Hardware Information Flow Tracking

• DOI: 10.1145/3447867
• 发表时间: 2021-04
• 期刊: ACM Computing Surveys (CSUR)
• 作者: Wei Hu;Armaiti Ardeshiricham;Ryan Kastner

An Overview of Hardware Security and Trust: Threats, Countermeasures, and Design Tools

• DOI: 10.1109/tcad.2020.3047976
• 发表时间: 2021-06-01
• 期刊: IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
• 影响因子: 2.9
• 作者: Hu, Wei;Chang, Chip-Hong;Li, Hai
• 通讯作者: Li, Hai