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

Assured Confidential Execution (ACE) for RISC-V ACE-RISCV is an open-source project, whose goal is to deliver a confidential computing framework with a formally proven security monitor. It is based on the canonical architecture and targets RISC-V with the goal of being portable to other architectures. The formal verification efforts focus on the security monitor implementation. We invite collaborators to work with us to push the boundaries of provable confidential computing technology. Formal verification: This project implements the RISC-V CoVE spec's deployment model 3 referenced in Appendix D. The formal specification is embedded in the security monitor's source code and the proofs are in the verification/ folder. Please read our paper1 and paper2 to learn about the approach and goals. Post-Quantum Cryptography (PQC) and Attestation: ACE supports local attestation, a mechanism to authenticate confidential VMs intended for embedded systems with limited or no network connectivity. ... Read full article.