3 ms·

what about https://github.com/seL4/seL4 https://github.com/seL4/seL4?

• deleted 5y ago
  [deleted]
• Animats 5y ago
  It doesn't do enough. It's so low level that you have to run another OS on top of it. So all it does is provide a virtual machine. Typically people load Linux on top, which means you have all the security holes of Linux. You just get to run a few copies of Linux, possibly at different security levels. I would have liked to see a secure QNX as a mainstream OS. The microkernel is about 60Kb, and it offers a POSIX API. All drivers, file systems, networking, etc. are in user space. You pay about 10%-20% overhead for message passing. You get some of that back because you have good message passing available, instead of using HTTP for interprocess communication.
  • kobebrookskC3 5y ago
    i was responding to the claim "It is sheer ego that would cause anybody to say that they can feasibly write a safe program in C or C++". of course, the feasibility part is questionable.
    • kaba0 5y ago
      It was written by top experts of the field through multiple years and is formally verified. It could have been written in brainfuck as well, since at that point the language is not important.
    • UncleMeat 5y ago
      "on their first attempt" is part of that sentence.