TrustedCPU: Formally verified microcode customization for security exploit mitigation
Abstract
Proposal title: TrustedCPU: Formally verified microcode customization for security exploit mitigationAgency: ONRBAA Number: N0001424SB001Program Officer: Dr. Ryan Craven, ONR Code 311, Email address: ryan.m.craven2.civ@us.navy.milThe project proposes to leverage the CISC-to-RISC micro-op translation interface available in modern x86 hardware for mitigating security exploits, especially for legacy software, with no changes to the software stack, no changes to the x86 ISA, and no intrusive changes to the x86 CPU microarchitecture. Security exploits including memory corruption (e.g., memory safety exploits) and transient execution attacks (e.g., Spectre)continue to plague modern software systems. State-of-the-art mitigations involve intrusive modifications to the software stack (e.g., source code instrumentation, compile-time/run-time checks, binary instrumentation/rewriting), or using ISA extensions (e.g., ARM s MTE and PAC, Intel MPX), or using new hardware (e.g., CHERI, ARM Morello).Although effective, applying these mitigations is challenging for legacy software, especially for x86 software which is ubiquitous and exists in copious amounts. The project envisions thatthe CISC-to-RISC micro-op translation interface in x86 hardware is an effective abstraction for applying exploit mitigations without any changes to the software stack or the ISA, and proposes three research directions at the micro-op translation interface:1)microcode-level exploit mitigation, including memory exploit mitigation, mitigating transient execution attacks, and software sandboxing;2)OS-based microcode programming framework that enables writing microcode patches as (Linux) OS kernel modules or as eBPF programs; and 3)formal, fully automatic microcode verification that ensures that microcode patches provably satisfy a class of security properties including non-interference. The project proposes to demonstrate the research results in each of the three directions in Red-Unlocked x86 CPUs (a CPU mode that enables JTAG debugging of internal CPU components using external hardware). The project is anticipated to contribute to improving the security of Navy s legacy software systems through security exploit mitigations implemented at theCPU microcode level, avoiding invasive and expensive software stack modifications and hardware changes.Approved for Public Release
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Nov 09, 2024
- Source ID
- N000142412642
Entities
People
- Binoy Ravindran
Organizations
- Office of Naval Research
- United States Navy
- Virginia Tech