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

SaTC：STARSS：小型：协作：下一代开源处理器的设计和安全验证

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

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.

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

项目成果

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

Secure TLBs

• DOI: 10.1145/3307650.3322238
• 发表时间: 2019-06
• 期刊: 2019 ACM/IEEE 46th Annual International Symposium on Computer Architecture (ISCA)
• 作者: Shuwen Deng;Wenjie Xiong;Jakub Szefer

A Benchmark Suite for Evaluating Caches' Vulnerability to Timing Attacks

• DOI: 10.1145/3373376.3378510
• 发表时间: 2019-11
• 期刊: Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems
• 作者: Shuwen Deng;Wenjie Xiong;Jakub Szefer

Analysis of Secure Caches Using a Three-Step Model for Timing-Based Attacks

• DOI: 10.1007/s41635-019-00075-9
• 发表时间: 2019-11
• 期刊: Journal of Hardware and Systems Security
• 作者: Shuwen Deng;Wenjie Xiong;Jakub Szefer

Leaking Information Through Cache LRU States

通过缓存 LRU 状态泄漏信息

• DOI: 10.1109/hpca47549.2020.00021
• 发表时间: 2020
• 期刊: International Symposium on High-Performance Computer Architecture
• 作者: Xiong, Wenjie;Szefer, Jakub
• 通讯作者: Szefer, Jakub