Kani for unsafe rust

[podhrmic]

Hi @nspin !

As we talked, I had a brief look at the unsafe code in rust-sel4 and whether Kani could be helpful here:

1. the unsafe logic is already fairly limited, e.g. a pointer dereference, memory transmutation or external function call. That is good (less unsafe code the better), but also there is not that much that Kani can test (not counting trivial properties, such as any usize ptr that is not null can be dereferenced)
2. we would usually start with converting unit tests to symbolic Kani tests - given there are (almost?) no tests in rust-sel4 crates, maybe we should start by adding tests/fuzzing? Don't get me wrong - your code looks really good, currently it is just hard to say why should we trust it works (maybe you have some ideas?)
3. depending on the properties we want to proof, maybe other tools than Kani could be more applicable - e.g. Prusti or Flux.

[nspin]

Thanks for bringing this up!

the unsafe logic is already fairly limited, e.g. a pointer dereference, memory transmutation or external function call. That is good (less unsafe code the better), but also there is not that much that Kani can test (not counting trivial properties, such as any usize ptr that is not null can be dereferenced)

Yes, much of the unsafe code in this project is outside of the scope of what Kani can analyze. That said, there is, of course, plenty of analysis to be done towards increasing confidence in this project's use of unsafe! This includes finding ways to further minimizing its use, documenting assumptions and safety conditions, informal reasoning, and perhaps even applying tools which enable more rigorous analysis, including Kani and possibly others.

we would usually start with converting unit tests to symbolic Kani tests - given there are (almost?) no tests in rust-sel4 crates, maybe we should start by adding tests/fuzzing? Don't get me wrong - your code looks really good, currently it is just hard to say why should we trust it works (maybe you have some ideas?)

I agree that this project needs more tests with limited scope (including unit tests), and fuzzing! Some crates will require additional code infrastructure like mocking. I've been thinking about this, and I believe that certain mocking utilities may be useful for application developers using these crates as well, allowing them to develop and debug their application code on their development system, without emulation, instead of on seL4. So we might get extra bang for our buck there.

I've had a go at introducing Kani into this project (#30). I chose the sel4-bitfield-ops crate because it is both important (used heavily for object invocations and ABI-defined bitfield manipulation by the sel4-sys crate) and also easy to apply these techniques to.

I will report progress on all of these fronts in this issue.

[nspin]

I've introduced Verus into the project with this PR:

#143

For now, Verus feels like a heavyweight dependency for the core crates in this repo, but I plan to experiment with applying Verus to other areas of the code.

[podhrmic]

Very cool! I would be curious how your experience with Verus compares with Kani.