3 ms·

I haven’t fully given up on the hope that a fully verified kernel eventually catches on. It would be basically impossible to verify all of Linux at this point,

I haven’t fully given up on the hope that a fully verified kernel eventually catches on. It would be basically impossible to verify all of Linux at this point, but I could see seL4 eventually getting traction in something like the smartphone market. A guy can dream, at least.

meling 1y ago
It has been used for a while in the Secure Enclave operating system: https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=Apple%20A%20series,at%20310%20million https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=... But to my knowledge, not for the more general user facing OSes.
- tombert 1y ago
  Yeah that's what I was getting at. I know seL4 is used in a bunch of places, but outside of a few hobbyist projects I have never heard of anyone using is at a "full" OS. It would be nearly impossible to have the support for the extremely diverse set of hardware that desktop Linux has while staying formally verified, but for something a bit more constrained like a smartphone, I think something like seL4 could work as a base and the manufacturer could write their own drivers for whatever hardware is needed. I mean, how cool would it be if every single part of the stack that is even possible to verify was fully verified. I know about the halting problem, I know there are things that would be basically impossible to verify fully, but I still think it would be cool to live in a world where software engineers actually had a little assurance what they were doing actually worked before unleashing into the world.
  - AlotOfReading 1y ago
    I know at least one autonomous vehicle company is using it as their base OS in the autonomy stack, with efforts at extending some form of verification up to the high level code.
    - tombert 1y ago
      That's cool as hell! I didn't know that but it makes me happy to see it getting a bit more love.
snvzz 1y ago
seL4 is being used in many places that we know about[0] and then there's those we don't or are still in the future, where we can only guess based on e.g. seL4 membership[1]. 0. https://sel4.systems/use.html https://sel4.systems/use.html 1. https://sel4.systems/Foundation/Membership/ https://sel4.systems/Foundation/Membership/

meling 1y ago

It has been used for a while in the Secure Enclave operating system: https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=Apple%20A%20series,at%20310%20million https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=... But to my knowledge, not for the more general user facing OSes.

tombert 1y ago
Yeah that's what I was getting at. I know seL4 is used in a bunch of places, but outside of a few hobbyist projects I have never heard of anyone using is at a "full" OS. It would be nearly impossible to have the support for the extremely diverse set of hardware that desktop Linux has while staying formally verified, but for something a bit more constrained like a smartphone, I think something like seL4 could work as a base and the manufacturer could write their own drivers for whatever hardware is needed. I mean, how cool would it be if every single part of the stack that is even possible to verify was fully verified. I know about the halting problem, I know there are things that would be basically impossible to verify fully, but I still think it would be cool to live in a world where software engineers actually had a little assurance what they were doing actually worked before unleashing into the world.
- AlotOfReading 1y ago
  I know at least one autonomous vehicle company is using it as their base OS in the autonomy stack, with efforts at extending some form of verification up to the high level code.
  - tombert 1y ago
    That's cool as hell! I didn't know that but it makes me happy to see it getting a bit more love.

snvzz 1y ago

seL4 is being used in many places that we know about[0] and then there's those we don't or are still in the future, where we can only guess based on e.g. seL4 membership[1]. 0. https://sel4.systems/use.html https://sel4.systems/use.html 1. https://sel4.systems/Foundation/Membership/ https://sel4.systems/Foundation/Membership/