Even the most diligent chip design companies can find their silicon compromised when malicious hackers implement stealthy fabrication-time attacks that skirt post-fabrication testing. According to research published in Communications of the ACM, a backdoor vulnerability could be exploited through a single gate, surreptitiously siphoning power from routed wires to charge a “remotely controllable privilege escalation.”
One only needs to peruse the CWE List to view the numerous ways in which the systems that we depend on every day are vulnerable. Thousands of vulnerabilities exist in the classes of Access Control, Calculation Errors, Control Flow Management, and Error Handling.
Generally these issues get resolved and fixes pushed out to consumers. But, as the patches get more complex, the hackers get smarter, and so on, and so on in a cycle of fear and frustration technology developers have been facing since the invention of the integrated circuit.
But, it shouldn’t have to be that way, and the seL4 microkernel is providing us a glimpse of a world in which it isn’t. Since the seL4 microkernel is built upon strict proofs covering many of these very vulnerabilities, the kernel will not share these same programming errors. That can be proven.
A key assumption of the mathematical proof behind the seL4 microkernel is that the hardware its running on behaves “correctly.” This means the chip and its peripherals perform everything expected of them, and nothing more. Currently, the only fully verified configuration uses the ARMv7 i.MX 6. This verification requires that some useful features on the chip are disabled and assumes that this feature disablement and the enabled functionality of the processor behave correctly.
The RISC-V architecture, meanwhile, provides an open source path to maximizing the potential security features of seL4. The RISC-V configuration has not been formally verified, but Data61 is working on completing the verification process using formal methods tools and techniques to create a secure computing environment from the hardware to user space. Emulation tools can be used to work out the kinks in many configurations before deploying to hardware. One of the new tools in the space is the Renode emulation framework from Antmicro, which brings the ability to emulate complex multi-node systems and offers a convenient testing interface to plug into modern CI workflows.
Renode provides easy support for custom defined processor boards using board configuration files and is licensed under a less restrictive license than competing emulator software.
A tutorial on building and testing seL4 configurations on a RISC-V platform with Renode was presented by DornerWorks at the RISC-V Summit in 2019. This tutorial outlines both of these technologies and shows how to set up and build and configure the software necessary to emulate an seL4 based application on the RISC-V Renode system, a starting point for embedded developers to start building the next highly secure systems with seL4 on RISC-V.
You can find the slides from the RISC-V Summit presentation here: https://riscv.org/2019/12/risc-v-summit-2019-proceedings
Especially in the aerospace and defense markets, where security is a constant concern, the seL4 microkernel has been showing promise in keeping hackers at bay. Using the Renode framework to perform initial validation of an seL4 system on a new open source RISC-V platform brings down the investment of developing secure products for these markets.
DornerWorks provides technology engineering so you can focus on your customers. With embedded electronics, FPGA, and software engineering expertise, we accelerate your product development and lower risk for adopting advanced technologies. One of our specialties is embedded virtualization technology, including Virtuosity hypervisor and seL4 secure microkernel-based solutions.