Towards a Formally Verified Security Monitor for VM-based Confidential Computing

Abstract

This paper proposes a novel methodology for formally modeling and proving a security monitor for VM-based confidential computing, addressing the lack of verification in existing systems critical for high-assurance applications. It introduces a canonical architecture that abstracts processor-specific components, identifying only a minimal set of required hardware primitives. The approach is demonstrated via a concrete example drawn from a Rust implementation of the security monitor targeting the RISC-V platform.

Report

Key Highlights

• Formal Verification Focus: The core innovation is providing a methodology for formal verification, addressing the certification requirements for confidential computing systems in critical infrastructure (e.g., aircraft, hardware security modules).
• Canonical Architecture: The work defines a standard, canonical architecture specifically for virtual machine (VM)-based confidential computing systems.
• Processor Abstraction: The approach is designed to abstract away processor-specific components, focusing instead on identifying the minimum necessary hardware primitives required by the trusted security monitor.
• RISC-V Implementation: The proposed methodology is validated using an example derived from a security monitor implementation written in Rust and targeted for the RISC-V architecture.

Technical Details

• System Component: A security monitor designed to operate within a VM-based confidential computing environment.
• Modeling Goal: Formally modeling and proving the security monitor to ensure security guarantees are enforced correctly.
• Abstraction Layer: By abstracting processor-specific hardware, the focus shifts to defining a minimal, core set of hardware primitives that any underlying platform must offer for the monitor to function securely.
• Implementation Technology: The demonstration involves a practical example from an implementation written in the Rust programming language.
• Target Hardware: The chosen target architecture for demonstrating the security monitor is RISC-V.

Implications

• Enabling Critical Adoption: Providing formal verification dramatically increases the assurance level of confidential computing, allowing this technology to be adopted in highly regulated and safety-critical domains where current solutions are insufficient due to verification deficits.
• Strengthening RISC-V Security Ecosystem: The demonstration on RISC-V helps position the architecture as a viable and trustworthy choice for confidential computing initiatives, particularly those requiring high-assurance security components like security monitors.
• Portability and Reliability: The development of a canonical VM architecture and the abstraction of hardware primitives promotes the development of more portable and robust trusted computing base (TCB) components that can be more easily adapted across diverse RISC-V silicon implementations.