Show HN: Confidential computing for high-assurance RISC-V embedded systems

Dear HN community! Looking forward to hearing your feedback on ACE (assured confidential execution), technology that implements VM-based trusted execution environment (TEE) for embedded RISC-V systems with focus on a formally verified and auditable firmware. We target high-assurance systems that can benefit from compartmentalization and hardware-backed isolation. The key ingredient called security monitor (firmware) is implemented in Rust. The formal specification is defined as annotations directly in code and gets translated to Coq using RefinedRust automation. ACE design is now part of the RISCV confidential VM extension (CoVE) specification (deployment model 3).

Show HN: Confidential computing for high-assurance RISC-V embedded systems
github.com

Yes, that's basically the relationship between CoVE and ACE, from a quick glance. In this case, ACE is simply implementing a formally modeled and verified security monitor where the design has been extracted to Coq and the invariants proven.

It can work on P550 because CoVE supports several "Deployment strategies", the one ACE uses is referenced in the README: CoVE spec, Appendix D, "M-mode [Trusted Security Manager] based deployment model" https://github.com/riscv-non-isa/riscv-ap-tee/blob/main/src/... -- the other appendicies detail e.g. Smmtt based designs, and apparently there's a not-yet-written "Nested Virtualization" design in Appendix C.

They also note that the P550 isn't a "true" port due to the preliminary, non-ratified H extension, and it also misses another required extension called "Sstc" but they just emulate it. (Sstc is interesting; it seems to be a performance optimization for delivering timer interrupts directly to supervisors, but I can imagine in the case of CoVE timer interrupts going through M-mode could leak data, making it more of a security issue.)

Leveraging M-mode is basically how previous security monitors like keystone worked too, back on the original HiFive Unleashed. It just sorta treats M-mode as an analogue to the "secure world" in ARM parlance, though there is no requirement that M-mode has e.g. an encrypted memory controller and dedicated memory region, and I'm guessing other things (I'm not super familiar with TrustZone.)

Broadly speaking this reminds me as a kind of a evolution/combination of Microsoft's Komodo (formally verified, but was only for e.g. SGX-style enclaves) and existing M-mode TEE systems like Keystone -- but upgraded to support "Confidental Computing" virtual machines. So that's quite nice.

How does this differ from Keystone?

There are two key differences:

(1) ACE leverages hardware virtualization support, including an MMU, to enable confidential virtual machines. In contrast, Keystone is designed for simpler processors that rely on just machine/supervisor/user privilege levels and physical memory protection (PMP), making it more suitable for process-based enclaves—similar to architectures like Komodo or Intel SGX. In that sense, ACE is conceptually closer to Intel TDX, but tailored for a different domain: embedded systems rather than cloud infrastructure.

(2) In ACE, the architecture and code are simplified to facilitate formal verification.