For the last year, Nick Spinale, funded by the seL4 Foundation, has been developing support for the Rust programming language in seL4 userspace.
Nick has created a comprehensive language support infrastructure that integrates well with the rest of the seL4 ecosystem (capDL, Microkit, sel4test) and also integrates well with what Rust programmers would expect from the language side. This work has now been accepted by the seL4 Foundation Technical Steering Committee and can be found on GitHub. Nick’s talk at the recent seL4 summit is on seL4’s Youtube channel. A demo system that uses the device driver framework, asynchronous programming in Rust and library support from the Rust ecosystem to implement a small web server is available on GitHub.
The overall outcome will be to allow people to write safer user-level code on top of seL4 without needing full formal verification, with a language that is receiving increasing interest and that aligns extremely well with security and safety critical embedded systems programming.
