Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

ACE: Confidential Computing for Embedded RISC-V Systems

Wojciech Ozga, Guerney D. H. Hunt, Michael V. Le, Lennard Gäher, Avraham Shinnar, Elaine R. Palmer, Hani Jamjoom, Silvio Dragone

TL;DR

ACE addresses the challenge of safely running safety- and security-critical embedded software by introducing a VM-based confidential computing framework for embedded RISC-V systems. It blends a lightweight, verifiable architecture (TSM, hypervisor, TVMs) with a verification-friendly design methodology, modular Rust-based implementations, and formal proofs via RefinedRust and Rocq. The authors demonstrate a working ACE prototype on the first virtualization-capable RISC-V hardware, show that memory safety and isolation can be established with a small trusted base, and quantify overheads in boot, I/O, and multi-VM workloads, finding practicality for embedded use cases. The work facilitates higher assurance in regulated environments by providing open-source tooling, local attestation, and a scalable verification workflow that can be extended to other embedded systems requiring formal verification.

Abstract

Confidential computing plays an important role in isolating sensitive applications from the vast amount of untrusted code commonly found in the modern cloud. We argue that it can also be leveraged to build safer and more secure mission-critical embedded systems. In this paper, we introduce the Assured Confidential Execution (ACE), an open-source and royalty-free confidential computing technology targeted for embedded RISC-V systems. We present a set of principles and a methodology that we used to build \ACE and that might be applied for developing other embedded systems that require formal verification. An evaluation of our prototype on the first available RISC-V hardware supporting virtualization indicates that ACE is a viable candidate for our target systems.

ACE: Confidential Computing for Embedded RISC-V Systems

TL;DR

ACE addresses the challenge of safely running safety- and security-critical embedded software by introducing a VM-based confidential computing framework for embedded RISC-V systems. It blends a lightweight, verifiable architecture (TSM, hypervisor, TVMs) with a verification-friendly design methodology, modular Rust-based implementations, and formal proofs via RefinedRust and Rocq. The authors demonstrate a working ACE prototype on the first virtualization-capable RISC-V hardware, show that memory safety and isolation can be established with a small trusted base, and quantify overheads in boot, I/O, and multi-VM workloads, finding practicality for embedded use cases. The work facilitates higher assurance in regulated environments by providing open-source tooling, local attestation, and a scalable verification workflow that can be extended to other embedded systems requiring formal verification.

Abstract

Confidential computing plays an important role in isolating sensitive applications from the vast amount of untrusted code commonly found in the modern cloud. We argue that it can also be leveraged to build safer and more secure mission-critical embedded systems. In this paper, we introduce the Assured Confidential Execution (ACE), an open-source and royalty-free confidential computing technology targeted for embedded RISC-V systems. We present a set of principles and a methodology that we used to build \ACE and that might be applied for developing other embedded systems that require formal verification. An evaluation of our prototype on the first available RISC-V hardware supporting virtualization indicates that ACE is a viable candidate for our target systems.
Paper Structure (24 sections, 9 figures, 1 table)

This paper contains 24 sections, 9 figures, 1 table.

Table of Contents

  1. Abstract
  2. Introduction
  3. Overview of ACE
  4. Open Source and Compliance
  5. Threat Model
  6. Design
  7. Design Methodology
  8. Key Design Choices & Invariants
  9. Implementation
  10. System Initialization
  11. Runtime
  12. Selected Non-confidential Flow Handlers
  13. Selected Confidential Flow Handlers
  14. Formal Verification Foundation
  15. Rust memory safety
  16. ...and 9 more sections

Figures (9)

  • Figure 1: High-level overview of ACE, a VM-based confidential computing architecture for embedded RISC-V processors. The TSM (➋) leverages hardware features (➊) to multiplex execution of different security domains (➌) and (➍) on top of the same hardware while preserving security guarantees.
  • Figure 2: Our methodology to develop formally verified low-level computing systems.
  • Figure 3: Pyramid of proof dependencies.
  • Figure 4: Finite state machine (FSM) shows the execution flow of the TSM on a single physical core on which the hypervisor and a TVM execute concurrently.
  • Figure 5: Definition of the page token invariant in the RefinedRust specification language.
  • ...and 4 more figures