FMitF: Track II: Scaling Formal Hardware Security Verification with CheckMate from Research to Practice

计算机无处不在，并且执行越来越复杂的任务，从锁定和解锁智能门到驾驶汽车和诊断疾病。Spectre攻击是一种硬件安全漏洞，已被用于泄露现代计算机上处理的任意敏感数据，并影响数十亿微处理器。由于复杂微处理器的广泛部署，设计验证其安全执行的机制已成为一个非常重要的问题。该项目的创新之处在于硬件安全验证方面的进步，其目标是扩展CheckMate方法和工具（正式的硬件安全验证研究原型），以支持行业规模处理器设计的分析。该项目的影响是一种工业规模的硬件安全验证技术和工具，从而为未来数十亿个商用微处理器的安全设计和部署提供保障。这意味着我们今天委托计算机执行的许多重要任务的安全性得到了提高。该项目有几个目标，支持提供改进的CheckMate的目标，能够自动分析工业规模的处理器设计，并适合硬件工程师使用。该项目的第一个重点是开发一种抽象/细化方法，将直接从微处理器的寄存器传输级描述中提取用于安全分析的微体系结构模型。目前，CheckMate需要一个手动构建的公理化微体系结构规范作为输入，该规范捕获所有相关的处理器功能进行安全分析，同时抽象出不相关的功能。第二个项目推进模块化CheckMate工具，引入一个专用的“前端”，解析定义的领域特定语言，将结果交给一个可以轻松交换的“后端”求解器。这有助于对解决CheckMate产生的验证问题的不同方法进行实验和评估。第三个推力将CheckMate验证算法本身模块化，允许CheckMate跨硬件模块边界搜索潜在的漏洞。该项目与Arm Research合作，以帮助确保CheckMate扩展适用于商业处理器验证。此外，该研究还将CheckMate应用于Arm Cortex-R8微处理器的微架构描述，以评估该工具检测Spectre攻击敏感性的能力。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

Computers are ubiquitous and performing increasingly sophisticated tasks, from locking and unlocking smart doors to driving cars and diagnosing disease. Spectre attacks are a type of hardware security vulnerability that have been used to leak arbitrary sensitive data processed on modern computers and affect billions of shipped microprocessors. Given the widespread deployment of complex microprocessors, devising mechanisms for verifying their secure execution has become a deeply important problem. The project’s novelties are advances in hardware-security verification underpinned by the goal of extending the CheckMate methodology and tool (a formal hardware-security-verification research prototype) to support the analysis of industry-scale processor designs. The project’s impacts are an industrial-scale hardware-security verification technique and tool and consequently secure design and deployment for billions of future commercial microprocessors. This translates to improved security for the many important tasks to which we entrust computers today.The project has several thrusts that support the goal of delivering an improved CheckMate, capable of automatically analyzing industrial-scale processor designs, and which is suitable for use by hardware engineers. The first thrust of the project develops an abstraction/refinement methodology that will extract microarchitectural models for security analysis directly from the Register Transfer Level description of a microprocessor. At present, CheckMate requires as input a manually constructed axiomatic microarchitectural specification, which captures all relevant processor features for a security analysis while abstracting away the irrelevant ones. The second project thrust modularizes the CheckMate tool, introducing a dedicated "front end" that parses a defined Domain Specific Language, handing off the result to a "back end" solver that can be easily swapped out. This facilitates experimentation with, and evaluation of, different approaches to solving the verification problems that CheckMate produces. The third thrust modularizes the CheckMate verification algorithm itself, allowing CheckMate to search for potential exploits across hardware module boundaries. The project features a collaboration with Arm Research to help ensure that CheckMate extensions are suitable for commercial processor verification. Furthermore, the research features an application of CheckMate to a microarchitectural description of the Arm Cortex-R8 microprocessor to evaluate the tool’s ability to detect susceptibility to Spectre attacks.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.