STARSS: Small: Collaborative: Practical and Scalable Security Verification of Security-Aware Hardware Architectures

STARSS：小型：协作：安全感知硬件架构的实用且可扩展的安全验证

• 批准号: 1524680
• 负责人: Jakub Szefer
• 金额: $ 16.67万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-10-01 至 2018-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1524680&HistoricalAwards=false
• 关键词: STARSS; Small; Collaborative; Practical; Scalable

Computers form the backbone of any modern society, and often process large amounts of sensitive and private information. To help secure the software, and the sensitive data, a number of secure hardware-software and processor architectures have been proposed. These architectures incorporate novel protection and defense mechanisms directly in the hardware where they cannot be modified or bypassed, unlike software protections. However, due to lack of practical and scalable security verification tools and methodologies, very few of the proposed hardware security architectures have been commercially deployed. This project develops a security verification methodology that is applicable to different hardware-software security architectures. This project develops security invariants and methodology that hardware architects can deploy to check the security properties of their architectures in a scalable and semi-automated manner. The methodology is applied to verify hardware-enhanced isolation architectures and architectures that minimize the attack surface in cloud computing. Verification of a secure cache's resistance to cache side channel attacks is also investigated. Researchers and designers will have a new method to systematically check their designs, and show to others the conditions under which they work. Hardware manufacturers will gain assurance to actually implement these security architectures in real products. In turn, customers will gain assurance about the secure hardware that protects their computations running on their devices or virtual machines running on remote cloud servers. Security architectures are important to customers and hardware manufacturers, however, security verification is needed to make them a reality.

计算机构成了任何现代社会的骨干，并且经常处理大量敏感和私人信息。 为了帮助保护软件和敏感数据，已经提出了许多安全的硬件软件和处理器架构。 这些体系结构将新颖的保护和防御机制直接包含在无法修改或绕过的硬件中，与软件保护不同。 但是，由于缺乏实用和可扩展的安全验证工具和方法，很少有商业部署所提出的硬件安全体系结构。 该项目开发了一种适用于不同硬件软件安全体系结构的安全验证方法。该项目开发了硬件架构师可以部署的安全不变性和方法，以以可扩展和半自动化的方式检查其体系结构的安全性。该方法用于验证硬件增强的隔离体系结构和体系结构，以最大程度地减少云计算中的攻击表面。 还研究了安全缓存对缓存侧通道攻击的阻力的验证。研究人员和设计师将有一种新的方法来系统地检查其设计，并向其他人展示他们工作的条件。 硬件制造商将获得保证，以在真实产品中实际实施这些安全体系结构。 反过来，客户将获得有关保护其在远程云服务器上运行的设备或虚拟机上运行的安全硬件的保证。安全体系结构对客户和硬件制造商很重要，但是，需要安全验证才能使它们成为现实。

项目成果

SecChisel Framework for Security Verification of Secure Processor Architectures

用于安全处理器架构安全验证的 SecChisel 框架

• DOI: 10.1145/3337167.3337174
• 发表时间: 2019
• 期刊: Workshop on Hardware and Architectural Support for Security and Privacy
• 作者: Deng, Shuwen;Gümüşoğlu, Doğuhan;Xiong, Wenjie;Sari, Sercan;Gener, Y. Serhan;Lu, Corine;Demir, Onur;Szefer, Jakub
• 通讯作者: Szefer, Jakub

Cache timing side-channel vulnerability checking with computation tree logic

• DOI: 10.1145/3214292.3214294
• 发表时间: 2018-06
• 期刊: Proceedings of the 7th International Workshop on Hardware and Architectural Support for Security and Privacy
• 作者: Shuwen Deng;Wenjie Xiong;Jakub Szefer

Survey of microarchitectural side and covert channels, attacks, and defenses

• DOI: 10.1007/s41635-018-0046-1
• 发表时间: 2019-01-01
• 期刊: J. Hardw. Syst. Secur.
• 作者: Szefer, Jakub