STARSS: Small: Collaborative: Specification and Verification for Secure Hardware

对检测硬件和硬件-软件接口中的安全漏洞的技术的需求日益增长。此类漏洞源于处理器和片上系统组件使用不受信任的供应链，以及恶意代理通过利用因设计错误、不完整的规格或恶意插入块而产生的硬件缺陷来颠覆系统的范围。该项目通过开发用于正式和半正式规范以及硬件安全属性验证的基础技术和工具来解决该问题。该项目解决了当前硬件设计规范和验证过程中的差距。给定设计和（可能是非正式的）规范，该方法首先识别与设计的高完整性或机密部分相对应的信号，例如特权模式标志或密钥。该方法使用此信息来执行关键信号分析、规范生成、安全意识规​​范分析以及测试表征和增强。重复这些步骤，直到达到适当的安全保证级别。这些方法建立在用于布尔推理、符号模拟和模型检查的正式计算引擎之上。该项目使用基于处理器核心和非处理器块的案例研究进行评估，其中每个案例研究都包括进攻和防御组件。有形的结果将包括理论、威胁模型、软件工具、基准测试和案例研究。该项目的结果被纳入 PI 编写的课程和教科书中，教学生如何以安全思维设计系统。

There is a growing need for techniques to detect security vulnerabilities in hardware and at the hardware-software interface. Such vulnerabilities arise from the use of untrusted supply chains for processors and system-on-chip components and from the scope for malicious agents to subvert a system by exploiting hardware defects arising from design errors, incomplete specifications, or maliciously inserted blocks. This project addresses the problem by developing foundational techniques and tools for formal and semi-formal specification and verification of security properties of hardware. This project addresses gaps in the current specification and verification processes for hardware designs. Given a design and a (possibly informal) specification, the approach first identifies signals that correspond to high-integrity or confidential parts of the design, such as privileged mode flags or secret keys. The approach uses this information to perform critical signal analysis, specification generation, security-aware specification analysis, and test characterization and augmentation. These steps are iterated until a suitable level of security assurance is attained. The methods build upon formal computational engines for Boolean reasoning, symbolic simulation, and model checking. The project is evaluated using case studies based on processor cores and non-processor blocks, where each case study includes both offensive and defensive components. Tangible results will include theories, threat models, software tools, benchmarks, and case studies. Results from the project are incorporated into courses and textbooks written by the PIs to teach students how to design systems with a security mindset.