Hi My name is Nirnai Rai and currently, I am pursuing Masters in CS from NIT Jaipur, India.I wanted to ask about the need for formal verification of RIOT code modules. I read about RIOT-fp and saw that they were using HACL* for their crypto library. I want to know if any work on formal verification of RIOT code modules is being done or how beneficial is it for the OS? Or are there any topics in RIOT which I could explore and work further on? Any advice would be appreciated.
Hi Nirnai Rai,
as far as I know, nobody is currently working on formal verification of any sorts. The current projects to improve security are:
- Improving Rust support in RIOT
- Rust support is actually pretty mature at the moment, but not every board supports Rust as of now and not every feature implemented in C in RIOT is wrapped as Rust API yet
- A number of core developers are aiming to implement more and more features in Rust. Once Rust support is mature enough that this would become practical, I expect some formal proposal to actually do this
- A number of modern MCU have features like MPUs that do a allow a meaningful distinction between userspace threads and kernel threads
- with that, it would be possible to limit a thread to only access its own memory and only access hardware via syscalls, very similar to what e.g. Linux does
- multiple options to run code in a VM
It would be interesting to see work on formal verification 
1 Like
Actually, in the RIOT-fp project that Nirnai pointed out, we’re working on formal verification of (parts) of RIOT. It’s non-trivial given the chaotic nature of the close-to-the-metal C codebase we’re starting with. The approach there is to rewrite parts of RIOT in Rust and Hacspec, a subset of Rust that can be automatically transformed into F*, which in turn allows doing formal proofs on it.
So far there is:
- HACL* for crypto
- a rewrite of riotboot in Hacspec
- an implementation of the runqueue of RIOT-rs’ scheduler in Hacspec
- a verified version of eBPF (paper preprint)
- and a lot of work on figuring out how to do any meaningful formal verification of a general purpose OS like RIOT, or parts of it, to enhance trust in the codebase as much as possible.
Check out the RIOT-fp project!
1 Like