Verifying RISC-V Physical Memory Protection

TL;DR

This paper presents a formal verification of the RISC-V physical memory protection hardware, ensuring its correctness for security-critical systems like Keystone, using a translation to UCLID5 and formal proof techniques.

Contribution

It formalizes the PMP rules from the RISC-V ISA and verifies an open-source hardware implementation using the LIME tool and UCLID5, advancing hardware security verification.

Findings

Formalized PMP rules based on RISC-V ISA

Verified correctness of open-source PMP hardware implementation

Lays groundwork for verifying Keystone security framework

Abstract

We formally verify an open-source hardware implementation of physical memory protection (PMP) in RISC-V, which is a standard feature used for memory isolation in security critical systems such as the Keystone trusted execution environment. PMP provides per-hardware-thread machine-mode control registers that specify the access privileges for physical memory regions. We first formalize the functional property of the PMP rules based on the RISC-V ISA manual. Then, we use the LIME tool to translate an open-source implementation of the PMP hardware module written in Chisel to the UCLID5 formal verification language. We encode the formal specification in UCLID5 and verify the functional correctness of the hardware. This is an initial effort towards verifying the Keystone framework, where the trusted computing base (TCB) relies on PMP to provide security guarantees such as integrity and confidentiality.