seL4 is an open source operating system kernel with a proof of implementation correctness and a cool capability system. A feL4 project is a Rust project that can be built to run in the seL4 context and make use of seL4 APIs.
The Robigalia project is the best example of prior art in this space. feL4 is distinguished largely by its aim to automate and simplify the development process.
Today we’re sharing cargo-fel4, an automation tool. With
cargo-fel4, you can write a seL4 task in Rust, expose it through a prescribed entry point, and then build it along with the kernel.
cargo-fel4 provides code generation that helps accelerate projects beyond the boilerplate of setting up a seL4 application. feL4 uses a toml-based configuration approach that helps wrap the relatively complex CMake build system for seL4, and
cargo-fel4 generates usable configuration files for multiple hardware targets.
For now, feL4 exposes only the system calls by way of Bindgen, as represented by the libsel4-sys library; however, we have plans to release more of our idiomatic and Rusty abstractions in the near future.
Dan, Jon, Zack, and Nathan @ PolySync