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).
Comments
IshKebab•5h ago
Can you explain what the relationship is between this and CoVE? Is ACE (this repo) the firmware, and CoVE the RISC-V hardware extensions that it requires?
How does it run on a P550 if that doesn't support CoVE?
aseipp•4h ago
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.
neom•4h ago
Developers have faced in the confidential computing space, particularly with x86 TEEs, fragmentation leading to vendor lockin and a difficult developer experience due to multiple, somewhat incompatible standards/approaches. Does the CoVE effort, and IBM's involvement in it, aim to prevent a similar situation in the RISC-V world, fostering a more open and standardized TEE ecosystem? Are you using CCC to align RISC-V CoVE with efforts to improve the developer experience? I hope we see common abstractions across different TEE architectures!!!
anonymousDan•3h ago
How does this differ from Keystone?
hyperhello•3h ago
> ACE supports local attestation, a mechanism to authenticate confidential VMs intended for embedded systems with limited or no network connectivity.
I'm interested to know the safe definition of 'limited' connectivity - is there some kind of boundary which logical reasoning can't support?
IshKebab•5h ago
How does it run on a P550 if that doesn't support CoVE?
aseipp•4h ago
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.