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

STARSS：小型：协作：安全硬件的规范和验证

• 批准号: 1525527
• 负责人: Randal Bryant
• 金额: $ 15.33万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-08-15 至 2019-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1525527&HistoricalAwards=false
• 关键词: STARSS; Small; Collaborative; Specification; Verification

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.

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