SaTC: STARSS: Small: Property Driven Hardware Security

设计不受任何安全攻击影响的现代硬件的任务几乎是不可能实现的。要确保这些复杂的、数十亿的晶体管系统在功能上是正确的，更不用说安全了，是极其困难的。因此，针对硬件漏洞的攻击数量越来越多，也就不足为奇了。硬件设计安全的最新技术在很大程度上依赖于功能验证、手动检查和代码审查来识别安全漏洞。这种劳动密集型流程不会扩展，它会显著降低工作效率，并且无法保证会发现安全漏洞。继续保持现状无疑会使硬件设计容易受到通过硬件、固件和软件漏洞表现出来的攻击。该项目开发了一种属性驱动的硬件安全方法，可以自动验证硬件设计上的安全属性。该项目包括三个主要研究目标：创建可表达的安全属性语言，构建分析硬件设计安全性的全面模型，以及生成能够以高效和可扩展的方式验证安全属性的工具。调查人员通过开发能够指定各种安全属性的模型来解决这些挑战。该项目利用这些模型构建了一种新的安全属性规范语言，并开发了新的技术，使这些属性能够使用现有的形式化求解器、模拟环境和仿真平台进行验证。最后，他们通过验证不同硬件设计上的安全属性来解决这种属性驱动方法的可用性问题。

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.