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

计算机无处不在，执行着越来越复杂的任务，从锁和解锁智能车门到驾驶汽车和诊断疾病。幽灵攻击是一种硬件安全漏洞，已被用来泄露在现代计算机上处理的任意敏感数据，并影响数十亿出厂的微处理器。鉴于复杂微处理器的广泛部署，设计验证其安全执行的机制已成为一个非常重要的问题。该项目的新颖性是硬件安全验证方面的进步，其目标是扩展Checkmate方法和工具(正式的硬件安全验证研究原型)，以支持对工业规模处理器设计的分析。该项目的影响是一种工业规模的硬件安全验证技术和工具，从而确保未来数十亿个商业微处理器的设计和部署。这转化为提高了我们今天委托计算机执行的许多重要任务的安全性。该项目有几个推力，支持交付改进的将军的目标，能够自动分析工业规模的处理器设计，并且适合硬件工程师使用。该项目的第一个重点是开发一种抽象/改进方法，该方法将直接从微处理器的寄存器传输级别描述中提取用于安全分析的微体系结构模型。目前，CheckMate需要一个手动构建的公理微体系结构规范作为输入，该规范捕获用于安全分析的所有相关处理器特性，同时抽象出不相关的特性。第二个项目将Checkmate工具模块化，引入了一个专用的“前端”来解析定义的领域特定语言，并将结果传递给一个“后端”求解器，该求解器可以很容易地被换出。这便于试验和评估解决Check Mate产生的验证问题的不同方法。第三个推力使Check Mate验证算法本身模块化，允许Check Mate跨硬件模块边界搜索潜在的漏洞。该项目的特点是与ARM Research合作，以帮助确保Check Mate扩展适合商业处理器验证。此外，这项研究的特点是将Check Mate应用于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.