This is good work. I enjoyed reading it. I wonder, though, why Muen separation kernel wasn't mentioned in related work on kernels in safe languages. It uses the SPARK language so that it's provably immune to a number of defects. The Ada compilers can also give you as little or much runtime as you want with several "profiles" available. Muen uses the "minimal, Zero-Runtime" profile. Rust improves on Ada and SPARK with the affine types giving temporal safety plus more flexible model for safe concurrency than Ravenscar. CompSci work shows one can probably do that and info-flow security with contracts but that would be extra, specialist work for Ada/SPARK versus what's built-in to Rust already. Verbose, too.
When I about the Rust kernels, I assumed there would be some trusted components in there which could screw them up on assurance side. Aside from full formal verification, one thing someone might want to try is writing those pieces in SPARK like Muen does. Make a direct port from any proven SPARK to Rust source. Alternatively, compile the SPARK into executable code that Rust calls with its FFI since C code can call SPARK code. Then, those untrusted portions are shown safe with one set of rules while the rest is shown safe with Rust's compiler. Optionally, convert those to an intermediate language of CompCert or CakeML compilers for certified compilation. This is how my Brute-Force Assurance model would attempt to handle each's limitations in a kernel project.
Note: Only problem with using SPARK for that is the person doing it probably has to buy a license if the Rust kernel in question isn't GPL. SPARK is only free for use with GPL code. Frama-C is another option one might use to avoid that but SPARK is stronger offering.
If you see from my discussions, many in the community (not the Rust designers) seem to be unaware, willing or not, of all the great work that came before Rust.
Rust is making a great progress infecting other languages with the idea of having affine types for resource management and concurrency is possible, just that the ergonomics still need some fine tuning.
No need to glace over the ideas of other strong type systems programming languages.
Oh well, not being a native speaker only now I realized that the last sentence is the complete opposite of what I intended to say, and the edit is button is gone now.
What I actually wanted to say, is that it would be worthwhile for the community to learn what has been done before, like the examples referred by nicksecurity.
Heh… that approach is probably workable, but it sounds like such a hack to use two completely unrelated programming languages to get two different levels of safety. It would be so cool if someone wrote a language/compiler which is to Rust as SPARK is to Ada.
It definitely is a hack. I've encouraged others with expertise to create SPARK-like tech for a Rust subset among other things. The problem is such experts are hard to find and it took SPARK 10-20 years to get to thus point. There's also a lot of verification tooling for C and Java especially that would have to be ported.
So, I came up with a concept called Brute Force Assurance that tries to reduce verification from an expensive, expert problem to a pile of cheap labor problem. The idea is a language like Scheme or Nim expresses the algorithms in lowest-common denominator form that’s automatically converted to at least equivalent C, Rust, Ada, and SPARK. Their tools… esp static analyzers or test generators in C, borrow-checker in Rust, and SPARK’s prover… all run on the generated code. Errors found there are compared against the original program with it changed for valid errors. Iterate until no errors and then move on to next work item. Eventually, one might use certified compiler on one of these forms (probably C).
Hey, this is an extension of what I'm planning to work on, which is a translator from Scheme enriched with lifetime and type information to Rust. See my comment here: https://news.ycombinator.com/item?id=15286945
For what it's worth I hear work on porting some of rust's memory-ownership concepts to Spark are going well at AdaCore. This should allow pointers to be integrated in the Spark subset of proveable Ada.
I do hope you're right with them figuring it out. It's a killer feature Ada and/or SPARK need. The alternative is basically separation logic. That isn't going mainstream or significant commercial haha. For me, I prefer both to adopt each others' strengths to increase diversity in batteries-included, safe/secure, systems space.
https://muen.codelabs.ch/
When I about the Rust kernels, I assumed there would be some trusted components in there which could screw them up on assurance side. Aside from full formal verification, one thing someone might want to try is writing those pieces in SPARK like Muen does. Make a direct port from any proven SPARK to Rust source. Alternatively, compile the SPARK into executable code that Rust calls with its FFI since C code can call SPARK code. Then, those untrusted portions are shown safe with one set of rules while the rest is shown safe with Rust's compiler. Optionally, convert those to an intermediate language of CompCert or CakeML compilers for certified compilation. This is how my Brute-Force Assurance model would attempt to handle each's limitations in a kernel project.
Note: Only problem with using SPARK for that is the person doing it probably has to buy a license if the Rust kernel in question isn't GPL. SPARK is only free for use with GPL code. Frama-C is another option one might use to avoid that but SPARK is stronger offering.