To effortlessly develop seL4 systems in rust

… and its underlying ecosystem.

Summary

To draw from the tagline for the Rust project

A language empowering everyone to build reliable and efficient software.

seL4 is exceptional with regards to reliability and efficiency. The goal here, is to bring the "empowering everyone" qualities of Rust to seL4, by way of seamlessly reaching into seL4 development from Rust.

Motivation

Community attraction to rust

Rust is highly attractive to the dev-community at large. Stack overflow surveys has it as "most loved" seven years running, and in 2022, it was surveyed as being "most wanted".

To make writing Rust for seL4 ejoyable and productive "out of the box" is to make seL4 development an attractive endeavour to a wider community

Provide dev-tooling that has trustworthiness as a first-class principal

TODO:? Add motivations that explicitly outline the benefits of rust?

Make Rust a language choice that does not come with handicaps

Currently, there are a lot of limitations and considerations needed in order to develop with Rust. The choice between C and Rust would ideally be solely based on language qualities.

Guide-level explanation

Roadmap

This could be an RFC in and of itself. There are independant projects out there, each a demonstration that there is a will, desire, and feasability to making Rust a supported tool for building seL4 based systems. In way to move towards a goal, and what reaching that goal would look like, is ambiguous at this point.

Rust ecosystem-centric principals

The Rust ecosystem is a potentially powerful tool for improving the ability to organise, maintain, and make available, libraries and tooling. For specific examples.

Consider this (hypothetical) workflow. No other build dependancies required.

# Create your hello world
cargo new sel4_hello_world
cd sel4_hello_world

# Import the core sel4 library, opting into a 
# rapid-prototyping utility library
cargo add --features utils sel4

# annotate the main function as the root server
sed -i '1i#[sel4::root]' src/main.rs 

# Simulate a default(native-platform-based QEMU) "hello-world" in debug mode, 
cargo run 

# Simulate in release mode, using features provided by `utils` to write to tty
cargo run --release

In the above examples, we have set up a hello-world system with no more (surfaced) complexity than an async hello-world (i.e. the need to annotate the main function to bring in the required runtime), followed by running a simulation.

Idiomatic Rust

Rusts rich type-system, helpful compiler errors, lifetime management, and other toolings dramatically elevate the value of exposing an interface that conforms to rust idioms, take the for example:

new type pattern

// instead of
sel4::reply(42); // (valid where a CPtr is like `#define seL4_Word seL4_CPtr;`)

// use an interface based on:
pub struct ReplyCPtr(CPtr);

// With a reply interface like so:
sel4::reply(reply_cap_type);

Ergonomic fallible code

Consider the following code in C:

int get_and_use_foo_struct() {
    FooStruct *foo = malloc(sizeof(*foo));
    if foo == 0 {
        return 0;
    }
    let result = fallible_call_getter(foo);
    
    if result != 0 {
        return result;
     
    // Continue on happy path
    let extracted = extract_useful_non_zero(foo);
    free(foo);
    

    // and let's blow things up...
    FooStruct *null_foo = 0;
    
    // try to fill up with a null-pointer
    int forgotten_result = fallible_call_getter(null_foo);

    /* undefined behavior */
}

The rust equivilent might be:

// API use: 
// inside a function with a return type: 
//    Result<usize, E> where E: From<FooError>
let usize_from_foo_struct = FooStruct::try_get_foo()
    // Handle the happy-path with `.map`
    // Use the conversion trait to get the usize
    // Use `?` to early-return the error
    .map(Into::into)?;

// why not log it, eh?
println!("got {}", usize_from_foo_struct);

// return the value
Ok(usize_from_foo_struct)

To make this possible, you would build an interface that might look like:

// Rust equivilent of Cs result enum. note lack of `Nil`
enum FooError {
    GetError,
    SomeError,
    OtherError
}

// Use Rust result wrapping pattern
pub struct FooResult<T> = Result<T, FooError>;

// Make get-error handling a compiler-enforced requirement
impl FooStruct{
    fn try_get_foo() -> FooResult<Self> {
        Self::fallible_getter()
    }
}

impl From<FooStruct> for usize { /* snip */ }
impl From<FooError> for $MORE_GENERAL_ERROR { /* snip */ }

Guiding Questions

If the rust ecosystem was already mature when seL4 rust development started, what would the project look like if Rust was considered the primary ecosystem for development?

There is already prior work done, where it seems this question has been asked, and work done to realise the vision that comes from this question:

Does $STRATEGY method of improving seL4 development in the Rust ecosystem increase the mantenance burden long term?

E.g. Having to maintain two libsel4 implementations (one for C, one for Rust), vs just having a Rust interface that can be called from an auto-generated C library, via an FFI.

Reference-level explanation

All fallable functions/methods are to return a Result

// Private helper-function
fn do_cnode_copy(/*snip */) -> Result<(), SyscallError> {/* snip */}

// api usage:
let cnode = sel4::CNode::/* constructor method */(/*snip */)?;
let mut copied_node: CNode = cnode.copy(/* snip */)?;

Use #[cfg(...)] for conditional compilation/exporting

// in src/arch/mod.rs

#[cfg(target_arch = "aarch64")]
mod aarch64;
#[cfg(target_arch = "aarch64")]
pub use aarch64::*;

Use usize instead of seL4_Word

The compiler auto-magically fills the same requirements of seL4_Word definitions

Use type-wrapping to constain (safe rust) to correct usage of usize

Put public wrappers around private data, and use intenal implementations to ensure that invalid data will return an Err instead of on Ok

// in src/types.rs
pub struct CPtr(usize); // equivilent to seL4_CPtr

// in TODO: module design for capability file locations
pub struct TCB(CPtr);

impl TCB {
    // The only(?) way to provide a `usize` to the kernel interface when a TCB cability is required
    pub fn create(/* snip */) -> Result<Self, /* snip */> {/* snip */}
    
}

Stakeholders

  1. kernel developers who primarily interact with the c code, but may want to occasionally look at or interact with rust code.
  2. end-user developers who currently interact with c-based seL4 code, and may want to migrate or add some rust based components.
  3. end-user rust focused developers primarily coming to seL4 from rust for its rust support and want it to reflect normal rust development practices.
  4. proof engineers who primarily with the proofs, and c-implementation with the expectation that rust support is not impactful.
  5. proof engineers focusing on rust based verification tools, who don’t currently exist or have anything to prove.

Drawbacks

TODO: (RFC author not objective)

Prior art

A lot of work has already been done to make rust compatable with seL4, in many different projects.

IceCap

The IceCap Framework provides a Rust runtime, Rust libraries, system composition tools, and a build system for constructing Rust userspaces for seL4-based systems. IceCap self-describes as opinionated. According to the authors, many of the design decisions which compose the IceCap Framework, across varying facets and scopes, were made with the design and engineering process of the IceCap Hypervisor in mind. However, the IceCap Framework is successful as the basis for the IceCap Hypervisor, which serves as a concrete, open-source example of a seL4-based system with a userspace written almost entirely in Rust.

See the (IceCap Framework Tutorial)[https://gitlab.com/arm-research/security/icecap/icecap/-/tree/main/examples#tutorial] for an introduction to some of the facets of the framework which relate to this discussion.

fel4

Perhaps example closest in scope/features to what this RFC is about. Following initial setup in README instructions, the following shell cli runs a hello-world:




cargo fel4 new my-project
cd my-project
cargo fel4 simulate

Some key contributions of this project to bringing seL4 into the rust ecosystem:

  • Changes to the assembly code such that initial hand-over to the root server goes directly to a rust no_std function
  • Proving that seL4 development is compatible with the rust+cargo ecosystem
  • TODO: Add more.

ferros

TODO

oxidised documentation

Originally an effort to grok the seL4 API, it became a PR to discus what a Rusty version of the API might look like.

Redox OS

A microkernel based OS written in rust. Though the seL4 kernel is entirely implemented in C, the Redox project could be considered a reference point regarding what the upper-bound might look like when it comes to ease of developing an OS with seL4 and Rust.

Unresolved questions

Build system strategy

Project scope

Where on the spectrum to set our ambitions. From "low-hanging fruit only" to "wildly ambitious". Some thoughts about what might be involved between the two

Wildly ambitious:

  • Replace the use of cmake/ninja with cargo/rust.
  • All seL4 specific tools be wholely within the rust ecosystem.
  • Non-kernel be wholely rust, with C support provided through code-generators/FFI
  • API design to use Rust as a primary reference.

Low-hanging fruit:

  • Where rust-implemented tools are already working, upstream them
  • Upstream efforts by fel4 to allow the root-server to be pure-rust

Some where in between:

  • Code gen tools that emit rust slowly migrate to a more "Rusty" API

Gerwin Klein

The matter of threading dependencies between cmake/kernel and rust build(s):

I’m not saying it (low-level lib) shouldn’t end up as a crate on crates.io, I think that might make sense, it’s just that the seL4 build should not depend on a Rust build, but only the other way around (Rust build can depend on or invoke a seL4 build).

a build.rs file can handle that, perhaps. One question that might need answering,

Are we expecting cargo to invoke the seL4 build system and produce a seL4 binary to package with user space?

The answer to this question can vary. For the things that

how does that mesh with the crate structure Rust expects? Can seL4 releases + bottom-level (untyped) Rust libraries be generated and packaged as a crate other work can depend on? If yes, what would working on a seL4 dev version look like where maybe no crate is published yet? (This would be mostly for CI during seL4 development, not so much for people wanting to use seL4).

how does support for the different config options of seL4 work in Rust builds? Can everything be mapped to corresponding concepts in Rust builds?

For static/default configurations, you can use .cargo/config.toml

There is also the corrosion cmake is a tool that helps integrate rust into a cmake project

I presume target architecture, platform, etc would be selected in the cargo.toml file? What would an example look like?

// src/arch/mod.rs

#[cfg(target = "aarch64")]
mod aarch64;
#[cfg(target = "aarch64")]
pub use aarch64::*;

#[cfg(target = "x86_64")]
mod x86_64;
#[cfg(target = "x86_64")]
pub use x86_64::*;

Api design

Select a repo