SaTC: STARSS: Small: Collaborative: Design and Security Verification of Next-Generation Open-Source Processors

该项目将开发具有先进安全特性的新型开源处理器架构。这些安全特性将被添加到现有的开源处理器中，以帮助保护数据的机密性和完整性，并防止侧信道攻击。除了设计之外，该项目还将提供新的方法来验证所提议的安全特性，以确保处理器硬件本身是可证明的安全。该项目的第一个重点是侧边通道保护，特别是处理器缓存和其他可能被利用来泄露机密信息的功能单元。它进一步增加了安全计数器和保护可信软件模块的新方法。第二个重点是硬件安全验证方法的设计，包括基于可满足模理论（SMT）的求解器和时间逻辑的使用。如果成功，这将使开源处理器及其应用程序更加安全，免受攻击。它将使学术界能够进一步开发和扩展开源安全处理器的功能，并进一步开展硬件安全方面的教育。该项目开发的所有人工制品将在http://caslab.csl.yale.edu/code/或http://palms.ee.princeton.edu上在线提供。这些网站将在项目期间和参与项目的研究小组活动期间保持。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

This project will develop new open-source processor architectures with advanced security features. The security features will be added to existing open-source processors to help protect the confidentiality and integrity of data and to protect against side-channel attacks. Beyond the design, the project will also provide new methodology to verify the proposed security feature, to provide assurance that the processor hardware itself is provably secure. The first thrust of the project focuses on side-channel protections, especially of processor caches, and other functional units that can be exploited to leak secret information. It further adds security counters and new means to protect trusted software modules. The second thrust focuses on the design of the security verification approaches for hardware, including the use of satisfiability modulo theories (SMT) based solvers and temporal logics.If successful, this will make open-source processors and their applications more secure against attacks. It will enable the academic community to further develop and extend the capabilities of the ope-source secure processor and further education in hardware security.All artefacts developed by this project will be available online at http://caslab.csl.yale.edu/code/ or http://palms.ee.princeton.edu. The web sites will be maintained for the duration of the project and as long as the research groups involved in this project are active.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.