Pre-RFC: To effortlessly develop seL4 systems in rust

There are a number of project out there that involve developing on seL4 using Rust. This RFC is an exploration of what can/needs to be done within the seL4 project itself to allow full advantage of rust tooling and language for building on seL4, with minimal extra friction.

The ongoing draft of the RFC is here: To effortlessly develop seL4 systems in rust - HackMD

Look forward to your feedback.

Hi, have you taken a look at Ferros? GitHub - auxoncorp/ferros: A Rust-based userland which also adds compile-time assurances to seL4 development.

I havenā€™t used it and Iā€™m not sure that it works for dynamic systems, but Iā€™d expect a discussion of seL4 development in Rust to include it.

1 Like

That one slipped under my radar. Thanks!

but Iā€™d expect a discussion of seL4 development in Rust to include it.

Hard-agree on that.

I like the spirit of the RFC, and personally Iā€™m on board with providing a proper typed libsel4 layer for Rust. Iā€™d consider that the fun and easy part and would be happy to contribute time to that. As pointed out in the draft RFC and discussion here there are multiple developments out there that would already be good candidates for that layer, at least as inspiration/for adaption. In addition to the ones mentioned so far, I also like the Icecap libraries.

What Iā€™m less clear on is how to achieve the goal of an easy/effortless dev + build experience. This may mostly be because I donā€™t know too much about cargo and the Rust build tools. Some concrete questions:

  • are we expecting cargo to invoke the seL4 build system and produce a seL4 binary to package with user space?
  • 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?
  • I presume target architecture, platform, etc would be selected in the cargo.toml file? What would an example look like?

While supporting and maintaining a Rust library layer seems doable in terms of effort, extending cargo like the fel4 project does not look like a sustainable option to me.

Related work for a looser coupling to the cmake build system for seL4 would be the Core Platform work. Not sure how directly applicable that is, but ideas from there might translate over.

In addition to a typed library layer, it would make sense to build up a few further libraries, in particular for resource management and common primitives, in terms of functionality along the lines of what currently exists in GitHub - seL4/seL4_libs: No-assurance libraries for rapid-prototyping of seL4 apps. for C. Iā€™d keep that separate from this RFC discussion though build that up over time.

One approach that could be considered is trying to focus requirements by first picking a seL4 framework like CAmkES or the seL4 Core Platform and focus on what it would take to write rust as first class apps in one of those environments. By starting from something that already defines a process abstraction and a runtime environment, itā€™s easier to build a rust foundation on top.

From this approach, itā€™s easier to motivate whatā€™s missing from the core seL4 libraries and tooling to support rust in these settings. Otherwise, itā€™s harder to argue the requirements for the libraries when theyā€™re trying to be the foundational rust support for all rust app runtime environments.

Yes, all of seL4_libs might be a bit much. Letā€™s focus on the the base libsel4 layer (typed) and general build first.

I suspect integrating with CAmkES and CP will be one step harder, because you also have to configure components and connections etc and it draws in more dependencies. Itā€™d be great to have that, but Iā€™d be fine with a more bare-bones environment first as well.

My personal interest in this would actually be experimenting with something more dynamic than either of CAmkES/CP (without verification, but at least with type safety), thatā€™s why Iā€™m keen on at least the bottom layer library + build capability without a component framework. E.g. longer term, itā€™d be nice to have something like Thread::spawn just work on seL4 or even an async framework that can use seL4 threads. These would all be within the same address space, and could be running inside a component framework or not (if it supports multi-threading).

One of my biggest issues with using seL4 effortlessly is the build system. Repo isā€¦ interesting, but can largely be ignored once sync is run. CMake is a fairly standard build tool for C/C++ but the way itā€™s used in seL4 is more complicated than the average and it also doesnā€™t follow some of the best practices (CMake makes this hard). The biggest issue I see is that the build system assumes that the kernel and libsel4 are compiled at the same time, with the same settings.

I understand why the ABI isnā€™t stable and I donā€™t think it needs to be. That would seemingly suggest stability across versions which I think is unnecessary. I am curious which things currently impact the ABI and why. I know that architecture/platform do (reasonable), MCS or not also does (reasonable).

For example, if Iā€™m building for riscv64, how do I know whether KernelCtzNoBuiltin changes the ABI? I donā€™t know why it would but Iā€™ve read a lot about seL4 lately and none of it suggests otherwise.

How does this relate to Rust (or other languages). All of the Rust attempts at seL4 that Iā€™ve seen have a separate tool that takes a set of configuration options like KernelCtzNoBuiltin and turns them into a kernel and custom libsel4 to be used. This makes using seL4 with Rust unlike most libraries.

Ideally, Iā€™d want to get to the point where the options that impact the ABI is documented, at least in a comment in the script that generates libsel4.

Edit:

Rust/Cargo currently supports conditional compilation using an extensible key-value system, though there are builtin configuration pairs that are always available/standard.

The standard ones are (from: Conditional compilation - The Rust Reference):

  • target_arch - e.g. x86_64
  • target_feature - e.g. avx
  • target_os - e.g. linux
  • target_family - e.g. unix/windows
  • target_env - e.g. musl/msvc/gnu
  • target_endian - e.g. big/little
  • target_pointer_width - e.g. 32/64
  • target_vendor - e.g. unknown/apple
  • debug_assertions - enabled by default for debug builds.

Adding custom options is possible but has implications when those options have to be exposed through the dependency management of cargo. If seL4ā€™s ABI only relied on these (and MCS ā€˜takes overā€™), then building a Rust crate and publishing it for a specific version of seL4 would allow anyone to program against the kernel without any additional effort.

Obviously, this ignores the question of bundling the kernel along with rootserver/elfloader/etc. but I think we can consider that out of scope for the current discussion.

My draft PR is in line with that, I feel, but is strictly a documentation effort. I would be happy to put some time into implementing something more concrete.

As a PoC, Iā€™m re-implementing some of the inline assembly in Rust. Idea being, is to be able to put it in a stand-alone repo, perhaps published to crates.io, and adapt the current seL4 build system to link that in. These are some of the things that Iā€™m aiming for

  • Identical to the C functions at the binary level
  • Compilation handled by the rust ecosystem
  • integrates seamlessly into current cmake system
  • Possibility of reducing the complexity of cmake.

Should this PoC go well, I see the following being a feasible reality:

  • There exists a libsel4 library as a rust crate
  • This crate is fetched, built, and linked-in by the cmake system
  • You could write a rust server with code as follows:
fn called_straight_away_by_c_root_server(/* snip */) {
    sel4::$KERNEL_OBJ_INTERFACE::$METHOD(/* snip */);

    // compile failure if not built with kernel debug printing: macro doesn't exist
    sel4::debug_println!("Hello, World");
}

Rust handles that in a very nice way. Below is an example. To the library user, the path to an arch-specific interface would be sel4::arch;, and

// 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::*;

This is a common pattern. Hereā€™s one example of how Rusts core library uses it to make simd portable between architectures (Though that area goes into some pretty advanced usage)

For target selection, itā€™s done as so:

# Add the target to the rust toolchain. Only needs doing once
rustup target add aarch64-unknown-none
cargo build --target aarch64-unknown-none

You can set up custom target triples. Goes into some detail here, but in brief:

cargo build --target target_tripple_file.json

There exists a CMakeLists library that aims to make the invocation and linkage of rust into a cmake built C/CPP project seemless. Working out what to do there is part of my work on the PoC

This is problematic, because the seL4 build is already too complex and should definitely not depend on crates.io. For developing the inline asm functions, it might make sense to start in a separate repo, but for maintenance they should eventually end up where the C inlines asm functions are and the rest of the low-level (untyped) Rust libsel4 is generated, because that is extremely tightly coupled with the kernel implementation.

The typed Rust libsel4 on top of that would make sense as a separate repo and should probably also stay that way.

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).

This looks quite nice.

1 Like

Iā€™d agree, though I do think fel4 has done some interesting work that can be referred to.

One possible way of going about things, is to have the (for example) inline asm functions sitting in a dedicated crate, and use cargos vendoring infrastructure.

At my work, we have some crates vendored into our mono-repo for modification. We are also going to be experimenting with open-sourcing some internal libraries. These libraries have a degree of coupling with our core code. One idea being is that we ā€œinlineā€ the crate into our mono-repo with vendoring, keeping our local code in-sync with our core code, and periodically up-streaming the the changes.

What it should mean (in theory), for seL4 rust-dependancies , is that as far as the mono-repo code-base is concerned, everything is organised as if it is integrated into the mono-repo as you describe.

Keeping the XY problem in mind: The key-stone issue here is maintainability/stability in the context of this code being very tightly coupled to the kernel. Anything upstreamed into mainline is conditional on these two qualities not being compromised in any way.

Others might be ahead of me with this, and have experience using this method. I can share our experience as we acquire it.

Will make sure this is encapsulated in the RFC before it gets submitted

1 Like

One thing this discussion seems to be circling back to consistently, is the build system. Some key points raised so far:

  • " are we expecting cargo to invoke the seL4 build system and produce a seL4 binary to package with user space?" - GK
  • Extending cargo like how fel4 does it, does not appear sustainable
  • Some ideas from Core Platform might translate over
  • seL4 CMake system isā€¦ interesting: ā€œThe biggest issue I see is that the build system assumes that the kernel and libsel4 are compiled at the same time, with the same settings.ā€ - Ahmed Charles
  • ā€œthe seL4 build should not depend on a Rust build, but only the other way aroundā€ GK

I have a project (currently in a private repository) that successfully integrated selfe-sys and a rootserver (mostly in Rust, compiled in staticlib mode) into a regular seL4 CMake build, using the Corrosion extension to CMake for doing cargo builds.

I think the most important question from my post is: Which configuration options impact the kernel/user ABI?

1 Like

If you only check out GitHub - seL4/seL4: The seL4 microkernel, you can use just itā€™s CMakeLists.txt to build a kernel + libsel4 for a particular configuration:

git clone https://github.com/sel4/sel4.git
cmake -G Ninja -C sel4/configs/ARM_verified.cmake -DCMAKE_INSTALL_PREFIX=$PWD/stage sel4/
ninja install

ls stage/
# bin  libsel4
$ ls stage/libsel4/
# include  src
$ ls stage/libsel4/include/
# api  autoconf.h  interfaces  kernel  sel4

The kernel can be built independently of libsel4, but it does use some of the headers that are in the libsel4 tree. libsel4 does require the kernel build has been processed by CMake before libsel4 can be built due to a large number of configuration dependencies they share, but you can build it independently, provided you use the same configuration options that were used for the kernel.

I didnā€™t know that, is it documented somewhere?

I knew this before, it was the intent of my post, so sorry if I communicated that poorly. The core question is, which configuration options impact the ABI and therefore have to be the same?

The previously mentioned KernelCtzNoBuiltinhopefully doesnā€™t impact the ABI, but thatā€™s not documented anywhere that Iā€™ve seen.

I think this would be easier to answer for specific definitions of impact and ABI. But I agree it makes sense to make it easier for people to know which options are safe to change without breaking their user level programs. Iā€™ve written up a few different scenarios from different interpretations of impact and ABI:

  • Thereā€™s probably only a few options that affect the syscall ABI - the actual ABI for performing the actual syscall machine instructions and argument register allocation layout: MCS/non-MCS and the KernelSel4Arch options.
  • Thereā€™s more options that affect whether certain debug system call numbers exist such as KernelPrinting or KernelBenchmarks, but this list could probably be enumerated.
  • If you consider the kernel object sizes are part of the ABI, then there are various options that change the size of different kernel objects. Some CMake options change the size of the TCB object which affects the seL4_Untyped_Retype interface. For the same sized untyped object you can create a different number of TCB objects depending on certain kernel configuration options. This may be not considered ABI breaking for some dynamic systems that implement their object creation code dynamically, but it may be considered ABI breaking for static systems that rely on performing all object allocation offline and compiling an allocation spec into their root loader.
  • The seL4_Bootinfo_t object is part of the ABI between the kernel and roottasks, but all other user programs arenā€™t affected. Essentially any kernel config option can change the contents of this object. Dynamic systems can likely handle a wider range of config changes without requiring recompilation, but extremely static systems may require recompilation for any config change. Any kernel config option that changes the size of itā€™s binary image will result in a different layout of initial untyped objects being described in the seL4_Bootinfo_t. There are experiments with the capDL language to verify full system properties from a system spec that depends on knowing an exact initial Untyped layout and would also treat that as part of the ABI.

This is what I wouldā€™ve expected and I would consider this the baseline. I hope we can get to a point where these options are documented for a given release.

I think this is fine, as long as executing those system calls when they do not exist results in a well defined error. Iā€™m not sure whether this currently results in a fault to the TCBā€™s exception endpoint or in an error result, but either one should be fine from the perspective of independently compiling a Rust libsel4.

Can one currently ask the kernel what those sizes are dynamically? Is that something that could be added? That would allow the current libsel4 to ignore that API and continue to hardcode the values based on configuration but allow a Rust libsel4 to dynamically determine the values.

Iā€™m fine with some users deciding to take on the burden of managing more configuration options if they get some benefit, like verification, in return. I think the current interface here is sufficient for everything to be determined dynamically, if one decides that is sufficient, right?

As a concrete example:

tagged_union seL4_Fault seL4_FaultType {
    -- generic faults
    tag NullFault 0
    tag CapFault 1
    tag UnknownSyscall 2
    tag UserException 3
#ifdef CONFIG_HARDWARE_DEBUG_API
    tag DebugException 4
#endif
#ifdef CONFIG_KERNEL_MCS
    tag Timeout 5

    -- arch specific faults
    tag VMFault 6

#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
    tag VGICMaintenance 7
    tag VCPUFault 8
    tag VPPIEvent 9
#endif
#else
    -- arch specific faults
    tag VMFault 5

#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
    tag VGICMaintenance 6
    tag VCPUFault 7
    tag VPPIEvent 8
#endif
#endif

}

The CONFIG_HARDWARE_DEBUG_API configuration doesnā€™t change the number which comes after it, but CONFIG_KERNEL_MCS does. This seems like an unnecessary ABI break, though in this case, MCS obviously breaks the ABI in many other ways.

In general, I think a reasonable goal would be to have a Rust libsel4 which can be published to crates.io and used without having to determine all of the configuration options that were used to build your kernel.