Building RISC-V systems on the secure seL4 microkernel in Renode

The increasing complexity of IoT applications comes with a bigger risk of potential cyber-attacks that can target multiple layers and components of a system. The ever-growing Common Weakness Enumeration (CWE) list, with thousands of entries related to both hardware and software, constantly reminds system architects that security should be one of the industry’s top concerns.

At Antmicro, we often help our customers design systems that need to be secure, building trusted execution environments, secure boot or secure remote management systems, security vulnerability prevention platforms etc. We are assisted in this by open source and transparent tools and workflows that we develop to boost collaboration, control and freedom to modify and improve all parts of the technology stack. One such tool is our open source Renode simulation framework, in use by a wide array of customers and partners ranging from startups to the industry’s largest players such as Arm, Microchip and Google. In one of the many recent fascinating user stories recently enabled by Renode (including such disparate topics as Zephyr, NuttX, mbed, OPC-UA and platform.io), one very interesting security-focused case study stands out, where Renode was used by DornerWorks to demonstrate the secure seL4 microkernel on RISC-V, two fascinating security-oriented technologies in their own right.

Embedded security with seL4

Embedded systems used in machines performing critical operations in aerospace, defense, aviation or automotive must be built on the basis of the most reliable and rigorously tested solutions to prevent malicious activity. The OS kernel in particular needs to be fully secure to ensure that the system running on it behaves as intended at all times, as it controls all resource accesses and separates critical and non-critical system components.

SeL4 claims the crown of the world’s only microkernel with formal verification, that is mathematically-checked code correctness. Its merits have been demonstrated in a number of real-world use cases, such as the DARPA-funded HACMS program, where seL4 successfully prevented cyber attacks on embedded systems in unmanned air vehicles, or the Cross Domain Desktop Compositor (CDDC) - a system for handling classified military information, developed with the Australian Department of Defence. It has also powered a fleet of satellites and run applications in autonomous cars.

Develop and test security features in Renode

The original seL4 RISC-V port was created by Hesham Almatary and Data61, and later improved by DornerWorks, at a time when RISC-V hardware was more difficult to obtain.
Dorner’s choice of Renode for showcasing seL4 on RISC-V is not incidental. In the associated presentation, they discuss Renode’s strengths such as:

• the ability to declaratively build complex environments,
• support for heterogeneous systems,
• advanced scripting,
• fine-grained control over execution,
• I/O and acceptance testing,

and show how the framework can be used to simulate and test a variety of seL4 use cases.

Antmicro are no strangers to application domains where security plays a critical role, with experience creating advanced systems meant to protect critical infrastructure, aerospace on-board computers and automotive applications. We routinely involve simulation in our security-oriented work, as extensive, reproducible testing - allowed by Continuous Integration which is Renode’s major focus - is key to building secure systems. That is why Microchip partnered with us to build a full pre- and post-silicon software development platform for their new, security-oriented PolarFire RISC-V FPGA SoC using Renode, offering the simulation framework for their customers and showcasing its use in an ongoing series of webinars. Renode can also integrate with Verilator for HDL co-simulation of IP in the programmable logic, for a variety of potential applications where part of the security logic is HW-accelerated in FPGA.

Renode can also be used to build secure systems from the ground up, including in the design space exploration and SoC development process, as exemplified by our partnership with Dover Microsystems. Dover, whose cybersecurity IP - CoreGuard - can be found in some of NXP’s latest secure microcontrollers, are leveraging Renode’s capabilities to simulate their product and to design systems around it before going for physical hardware implementation.

RISC-V support

Security is one of the primary focus areas of the RISC-V architecture, which aims to deliver robustness and reliability through offering and advocating transparency in hardware designs. As a Strategic Founding member of RISC-V International, we make sure the ISA is well-supported in Renode and provides an open and collaborative ecosystem for comprehensive development of hardware-assisted security features. RISC-V is also the first choice of cyber security researchers looking for the most trustworthy technologies - as reflected by the interest and discussion it generated at the international Workshop on Secure RISC-V Architecture Design in August this year.

The RISC-V port for seL4 developed and tested in Renode enables developers to combine the best tools, OS software and an open processor architecture to create advanced and highly secure systems. DornerWorks’ Jesse Millwood did a tutorial on how to run seL4 on RISC-V in Renode at the RISC-V summit in 2019, which happened to fall on the same time slot as our joint tutorial with Google about the Fomu FPGA and Renode at the same event. The related seL4 manifests and test code for Renode are available on GitHub and part of our CI suite.

Renode provides a wide array of security and collaboration oriented features, as well as a range of pre-defined building blocks that can be freely combined to create custom applications, from the CPU, to the SoC, up to complex multi-node systems.
If you design advanced embedded and IoT applications, including systems that require highest security, contact us at contact@antmicro.com to find out how our services and tools can help you achieve your goals.