COSMIC Project
CHERI for Operational Safety in Memory-Isolated Cores
CHERI for Operational Safety in Memory-Isolated Cores
The COSMIC Project, led by lowRISC® and partnering with Capabilities Limited, is backed by the UK Department for Science, Innovation and Technology (DSIT) and InnovateUK.
CHERI is a technology that has now reached the point it can be used in production grade chips. lowRISC will undertake, as part of this project, to deliver open source, reference 64-bit CHERI capable designs to cut down the time to market for commercial adoption. A self-funded, large, multinational technology organisation will investigate utilising the designs for two distinct use-cases that each address multi-billion dollar markets. lowRISC have also entered into preliminary discussions with multiple other organisations, several of which are keen to use the designs produced.
During stage 1 of the project the initial architecture and repositories will be set up to enable the consolidated design to be worked on. This design will be based on OpenTitan®’s Darjeeling, Integrated variant and use CVA6 CHERI to extend the capability to what is required for secure enclave environments. Combining the memory safety features with the core functionality required for a secure root-of-trust will enable many large organisations to consider adopting it into their use-cases. The self-funded backer will direct some of the design requirements to ensure that the designs will be suitable for the two distinct use-cases. It is expected that more organisations will become involved by the end of stage 1.
At the end of stage 1 of COSMIC there will be an open source repository with the first reference design of CHERI Mocha. There will also be a reference FPGA target platform that will be supported such that interested parties can buy the supported board and try out COSMIC.
During stage 2, continued verification efforts will be coupled with formal verification to ensure that both the hardware and the software maintain the properties of a memory safe system. Previous work using formal analysis uncovered bugs in an initial design that would otherwise have taken a long time to discover. As the complexity increases, moving from a 32-bit microcontroller to a 64-bit application class core, the need for formal verification increases so that there is confidence that the properties and principles of CHERI are adhered to in the implementation. Capabilities Limited brings its extensive CHERI experience in architecture, microarchitecture, and software to the table, along with its existing open-source CVA6-CHERI prototype core, and joins the COSMIC team to improve the quality, completeness, and performance of the processor and its software stack targeting the Secure Enclave use case. lowRISC will also be using experts in formal verification to work on the bleeding-edge solutions which will be used to assess the designs produced.
The CHERI-enabled devices will be SoCs that contain a modified OpenTitan design with a CVA6 CHERI core, resembling a Secure Enclave (SE). The SE operates independently from the rest of the SoC and without the need for any bootstrapping from the outside.
The design will be used as an IP for integration focusing initially on two distinct use-cases that will be used to assess the designs readiness for tape-out.
Verifying the designs will increase the likelihood that there is a successful intercept of commercial tape-outs and utilisation in production. Having a successful production tape-out will lead to others incorporating the design and taping out other SoCs. By being open source, the designs can be incorporated into other products and enable second sourcing, which is a prerequisite for Critical National Infrastructure applications.
lowRISC will combine the outputs of COSMIC into a set of open source (Apache 2.0 licensed) collateral, subject to the same production grade verification, continuous integration, documentation that OpenTitan adheres to. This will enable multiple CHERI-enabled products and reduce the time to market.