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.
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:
cargo to invoke the seL4 build system and produce a seL4 binary to package with user space?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):
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
Should this PoC go well, I see the following being a feasible reality:
libsel4 library as a rust cratefn 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.
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
One thing this discussion seems to be circling back to consistently, is the build system. Some key points raised so far:
cargo to invoke the seL4 build system and produce a seL4 binary to package with user space?" - GKcargo like how fel4 does it, does not appear sustainableI 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?
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:
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.