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

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

• 批准号: 1528108
• 负责人: Sanjit Seshia
• 金额: $ 14.67万
• 依托单位: University of California-Berkeley
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-08-15 至 2018-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1528108&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.

对检测硬件和硬件-软件接口处的安全漏洞的技术的需求日益增长。此类漏洞源于对处理器和片上系统组件使用不可信的供应链，以及恶意代理通过利用由设计错误、不完整规范或恶意插入的块引起的硬件缺陷来破坏系统的范围。该项目通过开发硬件安全属性的形式化和半形式化描述和验证的基本技术和工具来解决这一问题。该项目解决了当前硬件设计规范和验证过程中的空白。在给定设计和(可能是非正式的)规范的情况下，该方法首先识别与设计的高度完整性或机密部分相对应的信号，例如特权模式标志或密钥。该方法使用这些信息来执行关键信号分析、规范生成、安全感知规范分析以及测试表征和增强。反复执行这些步骤，直到达到适当的安全保证级别。这些方法建立在用于布尔推理、符号模拟和模型检查的正式计算引擎之上。该项目使用基于处理器核心和非处理器模块的案例研究进行评估，其中每个案例研究既包括进攻部分也包括防御部分。具体成果将包括理论、威胁模型、软件工具、基准和案例研究。该项目的结果被纳入由私人投资促进机构编写的课程和教科书中，以教会学生如何以安全的心态设计系统。