Tarides Logo
CPU chip hovering over a motherboard.

Secure From the Ground Up: Introducing the FIDES Project Combining RISC-V and MirageOS

Posted on Wed, 05 Jun 2024

We entrust some of our most sensitive information to an invisible stream of information flowing back and forth across the globe. Cybersecurity concerns everyone, and Tarides is developing secure, lasting, and high-performing solutions for a diverse set of users. This post introduces you to cutting-edge technology, employing some of the latest research in software development and cybersecurity to give you a sense of what the future of hardware and software security looks like.

Tarides is collaborating with the Indian Institute of Technology (IIT), Madras on the FIDES project. The project employs a hardware-enabled intra-process compartmentalisation technique on the Shakti RISC-V processor, capable of running bare-metal MirageOS unikernels written in OCaml safely alongside C code. This combined hardware and software solution leverages hardware-enabled compartments and OCaml's safety guarantees to ensure excellent security for real-world applications that mix safe and unsafe code.

Why Choose RISC-V and Shakti?

You might have heard of CHERI, a UK-based project that adds security features on top of ARM. As of 2022 ARM is the most widely used family of ISAs, and ARM processors power anything from smartphones to supercomputers.

The goal of the FIDES project is similar to CHERI. It extends the open-source Shakti RISC-V processors with additional security features. Unlike CHERI, FIDES is specialised to run MirageOS applications on top. MirageOS is a library operating system that uses properties of OCaml (a highly-secure programming language) to construct Unikernels to make secure, high-performance, network applications compatible with a variety of cloud computing and mobile platforms. The key benefit of the FIDES approach is that we can take advantage of the language-level security offered by OCaml to alleviate some of the overheads of enforcing security purely through hardware. With FIDES, the user gets a secure system from the hardware all the way up to the application layer.

But what is RISC-V? In 2015, the University of California, Berkeley, wanted to encourage "an open, collaborative community of software and hardware innovators based on the RISC-V ISA" by founding the RISC-V International Foundation. ‘RISC’ stands for ‘Reduced Instruction Set Computer’ and RISC-V is an open standard Instruction Set Architecture (ISA), offered free of charge alongside its extensions for anyone looking to build solutions and services. The initiative has sparked countless projects since its inception.

Using the RISC-V design and ISA is already a good start for security. It has strong academic roots, originally developed from a series of computer design projects by experts at Berkeley. This solid foundation has only been strengthened by being open-source, where the entire RISC-V architecture can be scrutinised in the public domain. Unlike in closed-source projects where they can't see the code, users can be sure there are no back doors or hidden channels. Having a free, open-source alternative also increases competition in the sector; developers can use publicly available extensions and reference designs to create more secure options for the closed-source solutions available.

The Shakti initiative is an open-source project spearheaded by the Reconfigurable Intelligent Systems Engineering (RISE) team at IIT Madras. The project encompasses a family of processors that use the RISC-V ISA to create scalable, cost-efficient, and open-source hardware solutions.

The FIDES project combines the Shakti processor (using the RISC-V ISA), and runs secure MirageOS OCaml unikernels on top.

The FIDES Approach

FIDES provides two extensions on top of the base Shakti RISC-V code. The first is a fine-grained compartmentalisation scheme that splits a process into multiple logical code partitions with an explicit access policy. This restricts what code can be called from functions in a given compartment. For example, the code of the display driver in a point-of-sale device has no reason to call into crypto code. Therefore, the two can be statically partitioned into separate compartments. This prevents vulnerabilities in the display driver from affecting the crypto modules. In addition, using a language like OCaml guarantees memory- and temporal- safety through its compiler and garbage collector. Thus, the programming language mitigates common memory error vulnerabilities while the compartmentalisation scheme mitigates privilege escalation vulnerabilities.

The second extension that FIDES provides is a fat-pointer scheme for C code. A significant amount of code is written in C, and we want to be able to make use of those programs without compromising on security. When C programs are combined with OCaml programs in the same application (such as a MirageOS unikernel), the vulnerabilities in the C code can compromise the security guarantees of the OCaml code. Every MirageOS unikernel has a significant chunk of C code present in the OCaml runtime that connects external libraries implementing core components such as fast crypto modules.

The FIDES fat pointer augments a pointer to a memory region with additional information that records the address range of a memory region (which is used for spatial memory safety) and a temporal cookie (for temporal memory safety). The spatial and temporal safety is checked on every access. The fat-pointer scheme ensures that the C code also has spatial and temporal memory safety. In this way, fat-pointers for C ensure that when linked with OCaml, the security guarantees of OCaml are not violated by memory vulnerabilities in the C code.

For performance reasons, the compartmentalisation and the fat pointer scheme for C are accelerated with hardware support. Importantly, since OCaml has language-level safety, FIDES does not use fat pointers for OCaml and pays neither the memory overhead of fat pointers nor the performance overhead of checking their validity at runtime. Given that MirageOS lets the developers build much of the typical operating system services directly in OCaml, FIDES is able to pay the additional performance cost for security only for C code.

Since OCaml and C code can interact seamlessly the developer benefits from both safety and flexibility. The compartmental approach limits additional vulnerabilities and fat-pointers ensure that C code interacts safely with OCaml code. On top of this, FIDES deploys secure-by-design MirageOS applications, extending the MirageOS backend to execute on bare-metal RISC-V processors. In this way, from metal to application, FIDES combines open-source technologies with strong security guarantees to give users a transparent, safe, and flexible solution.

Benefits

Let's conclude with the key benefits of using FIDES:

  • Secure: Memory safety is guaranteed, and FIDES seamlessly supports linking to unsafe C code without compromising overall safety.
  • Light-Weight: Does not require a memory management unit, an OS, or a hypervisor to guarantee isolation. It protects bare metal resource-constrained systems.
  • User Friendly: FIDES is designed to let users stay oblivious to the compartment policies and use unmodified OCaml and C code without issue. The FIDES design also permits a security engineer to perform critical compartment mapping tasks as part of deployment rather than development.

Until Next Time!

What sets FIDES apart is its focus on security, combining safety features for software and hardware to provide a secure and convenient way to deploy applications. Running MirageOS on the Shakti RISC-V processor shows excellent potential for delivering a high-performance, secure user experience.

Connect with us on X and LinkedIn for the latest updates on our projects. You can also contact us directly on our website with any feedback or questions. See you next time!

Open-Source Development

Tarides champions open-source development. We create and maintain key features of the OCaml language in collaboration with the OCaml community. To learn more about how you can support our open-source work, discover our page on GitHub.

Explore Commercial Opportunities

We are always happy to discuss commercial opportunities around OCaml. We provide core services, including training, tailor-made tools, and secure solutions. Tarides can help your teams realise their vision