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

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

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.