The Design and Implementation of a
Virtual Firmware Monitor
SOSP 2025
Charly Castes1 François Costa2 Neelu S. Kalani1
Timothy Roscoe2 Nate Foster3 Thomas Bourgeat1 Edouard Bugnion1
Summary
Problem: Firmware has become a security liability
We need to limit the blast radius in case of compromise!
Solution: Firmware-level virtualization
2
Charly Castes | SOSP’25
Background: Firmware
3
Background: Firmware
Firmware comes in two flavors:
4
Definition: Firmware is all the software that is required to set and maintain the hardware in an operable state.
Charly Castes | SOSP’25
Background: Firmware
5
U-Mode
M-Mode
S-Mode
Firmware
EL1
EL3
EL2
Hypervisor
Kernel
User App
EL0
In this talk, we focus on the application CPU firmware
Firmware
Kernel
User App
Charly Castes | SOSP’25
Background: Server-Grade Firmware
Cavium ThunderX firmware:
6
Towards a Unified Firmware for Enzian, Thomas Meyer-Lehnert (ETHZ)
There is a full-blown OS below the OS!
1 million LoC
Charly Castes | SOSP’25
Background: Firmware is a Security Liability
7
Firmware is a time bomb, we need to be prepared
Charly Castes | SOSP’25
Solution: Virtual Firmware Monitors
(VFM)
8
Classical virtualization, also called software virtualisation, relies on trapping and emulating privileged instructions
9
Hypervisor
App
De-privileged
Kernel
U-Mode
S-Mode
Formal requirements for virtualizable third generation architectures, GJ Popek, RP Goldberg, 1974
Charly Castes | SOSP’25
Classical virtualization, also called software virtualisation, relies on trapping and emulating privileged instructions
10
Virtual Firmware Monitor
App
Kernel
De-privileged
Firmware
M-Mode
U-Mode
S-Mode
Charly Castes | SOSP’25
The Popek & Goldberg virtualization requirements [1]:
An ISA is virtualizable if all sensitive instructions are privileged.
After a review of the main ISAs:
11
[1]: Formal requirements for virtualizable third generation architectures, GJ Popek, RP Goldberg, 1974
Charly Castes | SOSP’25
Miralis
The Miralis Virtual Firmware Monitor
Simpler than an hypervisor:
13
Firmware
App
Kernel
U-Mode
S-Mode
M-Mode
Miralis is 6.2K lines of Rust, and runs un-modified firmware in user-space
Charly Castes | SOSP’25
The Miralis Virtual Firmware Monitor
14
Miralis supports 3 different platforms with unmodified vendor firmware:
~1 trap/s
Charly Castes | SOSP’25
The Miralis Virtual Firmware Monitor
15
Firmware
App
Kernel
U-Mode
S-Mode
M-Mode
Enclave
Runtime
Miralis can be extended with isolation policies
+
Charly Castes | SOSP’25
Lightweight VFM Verification
16
Lightweight VFM Verification
Virtual firmware monitors are especially good targets for automated verification.
On Miralis, we verified:
17
Charly Castes | SOSP’25
Lightweight VFM Verification
We use the official RISC-V specification that we automatically translate into a RISC-V Rust model
Official Spec (Sail)
Rust Model
18
Charly Castes | SOSP’25
Lightweight VFM Verification
The Rust model can be used to verify the result of the Miralis emulator
19
R i
R’
R’’
≃?
With symbolic execution we can prove the correctness of the emulator (43.5% of the code base)
Charly Castes | SOSP’25
The Design and Implementation of a
Virtual Firmware Monitor
Firmware is a security liability.
On virtualizable architectures, firmware can be efficiently de-privileged.
Miralis is a RISC-V Virtual Firmware Monitor. It supports un-modified firmware, has no measurable performance overhead, and has a small TCB.
See SOSP’25 paper for details!
20
Charly Castes | SOSP’25
Lightweight VFM Verification - Bugs
Example: memory protection
21
Charly Castes | SOSP’25
Lightweight VFM Verification - Bugs
Example: adding new extensions
22
Charly Castes | SOSP’25