seL4
Don't reimplement libmicrokit in Rust?
Turns out Microkit 2.0.0 has some internal changes that affect the Rust Microkit support due to rust-sel4 re-implimenting libmicrokit which means I've broken rust-sel4 despite not introducing any libmicrokit breaking changes. The specific issue is from this PR https://github.com/seL4/microkit/pull/282 where I introduce more Microkit specific globals that are patched by the tool.
I don't think it makes sense to have two versions of the same library and instead rust-sel4 should wrap over libmicrokit since it means that internal changes to libmicrokit don't affect Rust users. Also, libmicrokit is intended to be formally verified and so if we continue with having another implementation of libmicrokit it means that Rust users wouldn't have the verified version or we would have to verify two libmicrokits.
In previous discussions I thought it would be fine to have another version of libmicrokit but it looks like I was wrong, I think the maintenance burden is too high, apologies.
I plan on implementing https://github.com/seL4/microkit/issues/128 which should make using libmicrokit via FFI easier.
One of nice things about Microkit is its simple, minimal ABI. From my perspective, the ABI is so simple that implementing the sel4-microkit crate at the ABI level incurs a lower maintenance burden than implementing it at the API level using bindgen would. I personally don't consider the maintenance burden for sel4-microkit to be high at all. This is all it took to update to 2.0.0:
ad237f08:crates/sel4-microkit/base/src/symbols.rs and https://github.com/seL4/rust-sel4/pull/247/commits/a2059811abd07eb533875c5a6f2820bf8b806158
Once libmicrokit is verified, the cost-benefit equation will change, of course, but for now, I believe that implementing sel4-microkit at the ABI level not only is at least as low-maintenance as implementing it at the API level, but also makes it easier to much implement correctly and with an idiomatic Rust API.
It may also turn out that verifying the rust version of libmicrokit is easier than verifying the C version. Would certainly be interesting to compare.
Once libmicrokit is verified, the cost-benefit equation will change, of course, but for now, I believe that implementing sel4-microkit at the ABI level not only is at least as low-maintenance as implementing it at the API level, but also makes it easier to much implement correctly and with an idiomatic Rust API.
Sure. I'm mainly just worried about subtle behaviour differences between the libraries.
I'm not sure if I should be taking ABI changes into account for semantic versioning, so far I have not.
It may also turn out that verifying the rust version of libmicrokit is easier than verifying the C version. Would certainly be interesting to compare.
The C version has already been verified in the past, but it hasn't been updated for the current version of libmicrokit. I believe the verification people at TS are looking at better tooling for doing C verification or potentially re-implementing libmicrokit in Pancake and then verifying that. I think people looked into verifying Rust but didn't pursue it, can't remember why.
Anyways, too early to say anything really.
The reason we aren't pursuing Rust is that we won't get a full story, given the lack of an agreed formal semantics and no hope of removing the compiler from the TCB – both possible with CompCert or Pancake
Yes, of course -- I didn't mean that TS should do Rust verification of libmicrokit. Given that the implementation is so small, there might be others who want to give it a shot. The complexity is modelling what happens in kernel calls, not so much with what the library does itself.
NB: it's all a bit more complicated. I doubt that libmicrokit with seL4 kernel calls and C runtime setup that is necessarily outside the standard satisfies the preconditions of the CompCert theorem, so CompCert won't give you a formal correctness story for this. And of course there is no agreed formal semantics of C either, everyone just does various reasonable subsets. There is compilation validation for C that doesn't exist for Rust, and the aspects of C semantics that are needed here are much simpler than the ones of Rust. So overall I agree that there still is much better verification infrastructure for C than for Rust, but it'd still be interesting to see how far things have been pushed.