SaTC: STARSS: Small: Tackling the Corner Cases: Finding Security Vulnerabilities in CPU Designs

包括处理器、内存库和通信总线在内的计算硬件可能存在漏洞，使攻击者能够未经授权访问计算机上的程序和数据。硬件设计人员和安全专家花费大量时间和精力在设计阶段早期消除这些漏洞。这项研究的重点是支持这些活动，以提高效率和成果。在开发硬件安全漏洞的方法和工具的过程中，本研究将推动硬件设计安全验证领域的发展。本课题针对中央处理器在设计阶段的安全性验证进行研究。该项目有两个目标：1)识别处理器的安全关键属性。这些属性将在寄存器传输级设计的时序逻辑中声明。2)开发方法和工具来自动查找和上下文化违反这些属性的行为。本研究的一个关键创新将是符号执行在硬件设计中的应用。为了使通过多个时钟周期符号化执行复杂硬件设计可行，本研究将开发一种有针对性的向后搜索策略。如果成功，该项目有可能大大减少恶意行为者对硬件发起有效攻击的机会，从而提高计算机系统的安全性。这项研究的工具、试验台、论文和报告将在https://cs.unc.edu/~csturton.This链接的网站上提供，该网站反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

Computing hardware including processors, memory banks, and communication busses can harbor vulnerabilities that allow an attacker to gain unauthorized access to the programs and data on a machine. Hardware designers and security experts expend considerable time and effort to eliminate these vulnerabilities early in the design stage. The focus of this research is to support these activities towards improving efficiency and outcomes. In developing the methodologies and tools to find and contextualize hardware security vulnerabilities, this research will move the field of security validation of hardware designs forward.The research targets the security validation of central processing units in the design stage. The project has two goals: 1) To identify security critical properties of a processor. These properties will be stated in a temporal logic over the register transfer level design. 2) To develop the methodology and tools to automatically find and contextualize violations of those properties. A key innovation of this research will be the application of symbolic execution to hardware designs. In order to make symbolically executing a complex hardware design through multiple clock cycles feasible, the research will develop a targeted, backward search strategy.If successful, the project has the potential to significantly reduce the opportunity for a malicious actor to launch an effective attack against hardware, improving the security of computer systems.The tools, testbenches, papers, and presentations resulting from this research will be available at a site linked from https://cs.unc.edu/~csturton.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.