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

Stanford University, Stanford CA

Investigators

Abstract

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.