7 ms·

There's already a high performance, formally verified, "FLOSS" microkernel: http://sel4.systems/ http://sel4.systems/ As it turns out, very few people are inte

There's already a high performance, formally verified, "FLOSS" microkernel: http://sel4.systems/ http://sel4.systems/ As it turns out, very few people are interested in having software that works.

Hypx 12y ago
I've only briefly heard of that kernel, and I suspect the same is true for many people at HN. It's also been open sourced pretty recently so maybe it needs more time for people to become aware of it. It may catch on if we give it more time. But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have. I was thinking of a kernel written entirely in Rust, and that would be not only much more reliable, because it would have far fewer segfaults and the like, plus be more immune to the types of highly publicized security flaws lately (Heartbleed, etc.). Of course, the whole OS might have to be written in Rust + memory safe languages. So we might be a ways off from the ideal goal, but clear I was thinking that we can start with a Rust kernel and build on top of that.
- nullc 12y ago
  SEL4 is provably free of segfaults, without any runtime overhead at all. Unlike Rust. Though it took considerable development time overhead to achieve that. (Moreover, rust itself may have bugs, or there could be bugs in unsafe code in the standard library. The amount of trusted infrastructure is much smaller for SEL4, I suppose if you compile it with compcert, I imagine it's quite small) The worst case latency is also part of the proof for SEL4-- which is a kind of correctness you cannot achieve via rust (even ignoring overhead). There are many elements of program correctness beyond memory safety. The developers of rust generally eschewed concerns about other kinds of correctness. For example, your integer types may overflow and your algorithms could fail to work as a result. SEL4's proofs show the operation of the software match its specifications completely (given some assumptions), it's really far far beyond the memory safety promises of rust.
  - TheHydroImpulse 12y ago
    > there could be bugs in unsafe code in the standard library For any embedded work or kernels, you wouldn't be pulling in the standard library via a `#![no_std]` attribute. But you're right that bugs in the compiler could produce safety issues.
    - nullc 12y ago
      > any embedded work or kernels Perhaps not, but in a kernel you'd have plenty of your own unsafe code. SEL4 doesn't. There are, of course, people thinking about bridging the worlds of formally provable correctness and Rust, e.g. https://github.com/rust-lang/rust/issues/18496 https://github.com/rust-lang/rust/issues/18496 though extraction based is likely to not produce the most elegant or efficient code... and I assume the along-the-side proofs like SEL4 uses would be harder for Rust because the language is more complex than C.
  - Havvy 12y ago
    Rust is able to be almost (unsafe blocks) free of segfaults without runtime overhead. That's the core feature that Rust provides with lifetimes. The Rust compiler can (and does) have bugs, but they get weeded out over time. But so can whatever proof system or proof checker is used on SEL4. As for integer overflow, yeah...that's a hard problem with Rust, and unfortunately, unlikely to be fixed.
    - MichaelGG 12y ago
      Aren't bounds checks and unwinding examples of non-free safety code in Rust?
      - kibwen 12y ago
        Unwinding is only potentially unsafe if you're already using `unsafe` blocks. If you're sticking to safe Rust, unwinding can't cause memory unsafety.
      - steveklabnik 12y ago
- tptacek 12y ago
  Hasn't code for L4 been available for, like, a very long time? SEL4 is a variant of L4, and not (IIRC) the best-known. L4 is fantastic, by the way.
- imanaccount247 12y ago
  >But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have No it won't, that's the point. It is a much stronger guarantee of being without those bugs than using rust would provide. >because it would have far fewer segfaults and the like SEL4 can not segfault, that's the point. It isn't fewer, it is zero. >but clear I was thinking that we can start with a Rust kernel and build on top of that. Yes, and I am saying if people actually wanted that, they could start with a formally verified kernel that already exists and build on top of that. But they don't.
nullc 12y ago
Or perhaps very few people are in a position to use a very recently Open Sourced OS that has no file system or network stack, or write these things for it? Presumably you'd want formally verified versions of at least the network device driver... otherwise process isolation might be violated.
- imanaccount247 12y ago
  Tons of people use L4 for their systems, there's billions of devices running some L4 kernel. The question is why are they not switching to SEL4 given that it provides the same thing they are already using, but faster and proven correct.
coldtea 12y ago
I call BS. The reason very few people care is that "works" is not a binary, but obviously a continium -- and people inherently understand diminishing returns... Especially when the "works" they care about is getting shit done, by having access to software (including proprietary), drivers, a community, vendors, etc. The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied...
- Animats 12y ago
  That L4 kernel is in the air link CPU of most cell phones.
  - coldtea 12y ago
    Nice that it found a niche there. That's however orthogonal to what I wrote, I think. It's not like it has a software ecosystem, community, drivers, etc, to be adopted over any major OSes as something that "all others being equal" is also "formally verified".
- imanaccount247 12y ago
  >I call BS. And yet your post can be summarized as "I am not aware of the usage of L4 microkernels". >The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied... Except their "other demands" are satisfied. It implements L4, just like every other L4 implementation does. It also happens to be the fastest L4 implementation ever tested. So rather than vague dismissive "calling BS", how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead?
  - coldtea 12y ago
    >how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead? I'm talking about people in general, prefaring their mainstream OS of choice over some platform based on L4. Not about L4 users opting for this or that implementation. The parent talked about people in general not caring for software quality, while those L4 users are highly specialized enteprises and businesses making a choice.

There's already a high performance, formally verified, "FLOSS" microkernel: http://sel4.systems/ http://sel4.systems/ As it turns out, very few people are interested in having software that works.

Hypx 12y ago

I've only briefly heard of that kernel, and I suspect the same is true for many people at HN. It's also been open sourced pretty recently so maybe it needs more time for people to become aware of it. It may catch on if we give it more time. But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have. I was thinking of a kernel written entirely in Rust, and that would be not only much more reliable, because it would have far fewer segfaults and the like, plus be more immune to the types of highly publicized security flaws lately (Heartbleed, etc.). Of course, the whole OS might have to be written in Rust + memory safe languages. So we might be a ways off from the ideal goal, but clear I was thinking that we can start with a Rust kernel and build on top of that.

nullc 12y ago
SEL4 is provably free of segfaults, without any runtime overhead at all. Unlike Rust. Though it took considerable development time overhead to achieve that. (Moreover, rust itself may have bugs, or there could be bugs in unsafe code in the standard library. The amount of trusted infrastructure is much smaller for SEL4, I suppose if you compile it with compcert, I imagine it's quite small) The worst case latency is also part of the proof for SEL4-- which is a kind of correctness you cannot achieve via rust (even ignoring overhead). There are many elements of program correctness beyond memory safety. The developers of rust generally eschewed concerns about other kinds of correctness. For example, your integer types may overflow and your algorithms could fail to work as a result. SEL4's proofs show the operation of the software match its specifications completely (given some assumptions), it's really far far beyond the memory safety promises of rust.
- TheHydroImpulse 12y ago
  > there could be bugs in unsafe code in the standard library For any embedded work or kernels, you wouldn't be pulling in the standard library via a `#![no_std]` attribute. But you're right that bugs in the compiler could produce safety issues.
  - nullc 12y ago
    > any embedded work or kernels Perhaps not, but in a kernel you'd have plenty of your own unsafe code. SEL4 doesn't. There are, of course, people thinking about bridging the worlds of formally provable correctness and Rust, e.g. https://github.com/rust-lang/rust/issues/18496 https://github.com/rust-lang/rust/issues/18496 though extraction based is likely to not produce the most elegant or efficient code... and I assume the along-the-side proofs like SEL4 uses would be harder for Rust because the language is more complex than C.
- Havvy 12y ago
  Rust is able to be almost (unsafe blocks) free of segfaults without runtime overhead. That's the core feature that Rust provides with lifetimes. The Rust compiler can (and does) have bugs, but they get weeded out over time. But so can whatever proof system or proof checker is used on SEL4. As for integer overflow, yeah...that's a hard problem with Rust, and unfortunately, unlikely to be fixed.
  - MichaelGG 12y ago
    Aren't bounds checks and unwinding examples of non-free safety code in Rust?
    - kibwen 12y ago
      Unwinding is only potentially unsafe if you're already using `unsafe` blocks. If you're sticking to safe Rust, unwinding can't cause memory unsafety.
    - steveklabnik 12y ago
tptacek 12y ago
Hasn't code for L4 been available for, like, a very long time? SEL4 is a variant of L4, and not (IIRC) the best-known. L4 is fantastic, by the way.
imanaccount247 12y ago
>But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have No it won't, that's the point. It is a much stronger guarantee of being without those bugs than using rust would provide. >because it would have far fewer segfaults and the like SEL4 can not segfault, that's the point. It isn't fewer, it is zero. >but clear I was thinking that we can start with a Rust kernel and build on top of that. Yes, and I am saying if people actually wanted that, they could start with a formally verified kernel that already exists and build on top of that. But they don't.

nullc 12y ago

Or perhaps very few people are in a position to use a very recently Open Sourced OS that has no file system or network stack, or write these things for it? Presumably you'd want formally verified versions of at least the network device driver... otherwise process isolation might be violated.

imanaccount247 12y ago
Tons of people use L4 for their systems, there's billions of devices running some L4 kernel. The question is why are they not switching to SEL4 given that it provides the same thing they are already using, but faster and proven correct.

coldtea 12y ago

I call BS. The reason very few people care is that "works" is not a binary, but obviously a continium -- and people inherently understand diminishing returns... Especially when the "works" they care about is getting shit done, by having access to software (including proprietary), drivers, a community, vendors, etc. The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied...

Animats 12y ago
That L4 kernel is in the air link CPU of most cell phones.
- coldtea 12y ago
  Nice that it found a niche there. That's however orthogonal to what I wrote, I think. It's not like it has a software ecosystem, community, drivers, etc, to be adopted over any major OSes as something that "all others being equal" is also "formally verified".
imanaccount247 12y ago
>I call BS. And yet your post can be summarized as "I am not aware of the usage of L4 microkernels". >The "is formally verified" they could not care less, and rightly so, if their other demands are not satisfied... Except their "other demands" are satisfied. It implements L4, just like every other L4 implementation does. It also happens to be the fastest L4 implementation ever tested. So rather than vague dismissive "calling BS", how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead?
- coldtea 12y ago
  >how about you point out the specific fault in SEL4 that causes people to need to use other L4 implementations instead? I'm talking about people in general, prefaring their mainstream OS of choice over some platform based on L4. Not about L4 users opting for this or that implementation. The parent talked about people in general not caring for software quality, while those L4 users are highly specialized enteprises and businesses making a choice.