Running Rust programs in seL4 using the sel4-sys crate

As the Rust programming language is becoming more and more popular, especially for secure systems development, more use cases for it emerge in innovative projects Antmicro is working on with its customers. While most popular operating systems such as Linux, Zephyr RTOS or seL4 are implemented in C, efforts to bring Rust interoperability to enable a new wave of modern systems development capabilities have been proliferating. In order to enable Rust also in the most secure environments, Antmicro has been working together with Google on enabling Rust applications for the seL4 microkernel, as part of a bigger effort towards building a Rust-based OS called KataOS on top of seL4 (which will at some point be described in separate blog notes).

SeL4 itself is an open source secure microkernel available for a variety of RISC-V and ARM platforms. SeL4’s claim to fame lies in its comprehensive formal verification, which makes it a perfect match for developing security-focused embedded applications in Rust which is also often chosen for its focus on (and excellent tooling for) minimizing the amount of bugs and side effects.

The seL4-sys crate

Thanks to the earlier efforts of the Robigalia project, the Rust+seL4 effort did not have to start from scratch; a crate named sel4-sys which allows building Rust applications for seL4 was used as a starting point.
Unfortunately, the project has not been in active development for some time now and became incompatible with the recent version of seL4.

In this effort Antmicro and Google have developed a new version of the crate which is designed with simplicity of future maintenance in mind, which hopefully will allow it to keep up with the evolving seL4 microkernel and Rust ecosystem.

In order to allow using seL4 from Rust code, the crate needs to define the API of the kernel. SeL4 provides sets of System Calls and Object Invocations. Additionally, it’s necessary to define data types for function arguments and interpreting return values of aforementioned system calls. All these, combined together in the sel4-sys crate, form the necessary interface to be imported in Rust source code.

The numbers of system calls and object invocations are generated during the build process. Conditional compilation allows compiling the minimal set of seL4 API that is needed, so specific values of system call numbers may change between builds, depending on configuration. This piece of code also has to be generated in Rust.

Object Invocations are those message-passing system calls which refer to the kernel itself. The crate uses a Python script to generate them from interface descriptions in XML files.
Using such a generic format allows storing information needed for both code and documentation in one place and generating syscall stubs for any programming language. The necessary information for the code generator is function name, arguments and return type. However, more information about possible error values, argument description and details about the function can also be useful for generating comments and documentation.

For example, here is some part of the description of seL4_TCB_SetPriority:

<method id="TCBSetPriority" name="SetPriority" manual_name="Set Priority" manual_label="tcb_setpriority">
	<param dir="in" name="authority" type="seL4_TCB"
    	description="Capability to the TCB to use the MCP from when setting the priority."/>
	<param dir="in" name="priority" type="seL4_Word"
    	description="The thread's new priority."/>
	...
</method>

The tools bundled with seL4 are capable of generating the function header in C:

LIBSEL4_INLINE seL4_Error
seL4_TCB_SetPriority(seL4_TCB _service, seL4_TCB authority, seL4_Word priority)
{…}

With the recent improvements, they can also generate the corresponding Rust code:

#[inline(always)]
pub unsafe fn seL4_TCB_SetPriority(_service: seL4_TCB, authority: seL4_TCB, priority: seL4_Word) -> seL4_Result
{...}

Integrating seL4 with the sel4-sys crate

Alongside the work on the sel4-sys crate, we have contributed to seL4 to allow generating these in Rust to allow a better integration with the crate and potentially other language bindings.

When the Rust API is generated, only one more thing is needed to allow building apps with seL4: the buildsystem of seL4 needs to be modified in order to replace the existing libsel4 with an alternative, which in this case is sel4-sys built as a static library.

In order to start a Rust project for seL4, you need to add sel4-sys to the Cargo.toml file, as a dependency.

[dependencies]
sel4-sys = { git = "https://github.com/AmbiML/sparrow-kata" }

In your main.rs, you can now use symbols from the crate.

use sel4_sys::seL4_BootInfo;
use sel4_sys::seL4_CPtr;
…

fn run() {
…
}

Now you’re all set! You can start implementing your applications for seL4 in Rust.

Platform support (RISC-V, ARM) and testing

Antmicro and Google have been working on making the system available for a wider community, and apart from contributing to the seL4 RISC-V implementation, we’ve improved architecture-specific code in sel4-sys.

The crate has been developed and tested for aarch64 and RISC-V targets, with some fixes to other targets also implemented in the process. Take a look at the list of hardware and simulation targets supported in seL4 to pick your platform.

One way of testing the interaction between Rust applications developed with sel4-sys and the seL4 kernel is the sel4test suite. Updates to the test suite related to sel4-sys are pending release. The progress for this and related efforts will be shared in upcoming notes.

Antmicro’s open source simulator, Renode, is also very useful for testing the ongoing seL4 work, both in the context of interactive development and CI testing. In another effort, described in a previous note, a seL4-specific OS awareness layer was developed, allowing users to easily debug userspace applications with GDB.

The next step for system programming in Rust

If you’re interested in creating secure embedded applications in Rust, you are encouraged to try it out with the seL4 microkernel. The best place to get started is the seL4 documentation and the main Sparrow project repository.

Seeing the increase in adoption of Rust in embedded systems, and being enthusiasts of the language, Antmicro has been working on making it easier to use in this context, including adding support for Rust-based peripheral models in Renode. Innovation is a strong focus of Antmicro’s open source based engineering services, which often translates to contributions to rising open source projects the company believes in. If you are looking to incorporate Rust and other modern technologies and tools in your workflow, reach out at contact@antmicro.com.