5 ms·

Question: under what circumstances would I ever want to use this OS, over Linux or MacOS or Windows?

mikewarot 2y ago
I've been waiting for a system like this for over a decade to use as my daily driver. An OS that runs with a capability model like this is immune to whole classes of security exploits that guarantee Linux, Windows, MacOS, etc. will never be secure. I was hoping Genode would get there sooner, and GNU Hurd should have gotten there years ago. Capabilities are the computing version of circuit breakers. They make it possible to run code without having to trust it. You can't do that with Linux, Windows, MacOS, et al. MULTICS could do it, but it was deemed too complex, at the time.
- progbits 2y ago
  Do you know if there is anything like that which can run OCI containers/lightweight VMs? I would love that as daily driver too for the same reasons, but realistically will have to run various Linux apps to be productive, so those could go into shortlived isolated sandboxes ala distrobox.
  - dmm 2y ago
    Have tried Qubes? It provides security through isolated VMs. https://qubes-os.org https://qubes-os.org
    - snvzz 2y ago
      For some definition of isolated. A replacement with a more serious architecture based on seL4 is in the works[0]. 0. https://trustworthy.systems/projects/makatea/ https://trustworthy.systems/projects/makatea/
- amluto 2y ago
  FWIW, I would not trust seL4 on x86. Last time I checked, seL4’s interaction with the x86 architecture was not formally verified and looked quite buggy. Even a microkernel has three things that form part of the TCB: the part that interfaces with the even-lower-level stuff (interrupt and exception handlers, paging, memory model, etc), the interface it provides to its clients (syscalls and whatever it provides via syscalls), and the code that glues the first two parts together and implements the microkernel’s internal logic. The latter two, in seL4, are straightforward and formally verified. The former, on x86, not so much. AIUI, the situation on ARM is likely better.
  - snvzz 2y ago
    >FWIW, I would not trust seL4 on x86. I would not trust any system on x86. >AIUI, the situation on ARM is likely better. Somewhat, but still not good. RISC-V is where it's at, when it comes to seL4. (seL4 participates in RISC-V)
- sillywalk 2y ago
  Have you tried Genode's Sculpt OS? "Sculpt is an open-source general-purpose OS. It combines Genode's microkernel architecture, capability-based security, sandboxed device drivers, and virtual machines in a novel operating system for commodity PC hardware and the PinePhone. Sculpt is used as day-to-day OS by the Genode developers." https://genode.org/download/sculpt https://genode.org/download/sculpt
  - mikewarot 2y ago
    I tried it a while ago, it seemed like there wasn't enough there, there. I couldn't find the "Hello World" example that made sense to me. I get the idea of composing resources, but until I've got a file system and compiler running, and a command line I can do something with, it doesn't help. 8( I'm hoping that Sculpt 24.04 does the job for me. If I can make sense of it enough to get Free Pascal running on it, or even just a C compiler, and "Hello, World" in a CLI, we're off to the races.
    - sillywalk 2y ago
      I never really got it to do anything. I gather that this[0] is the "tutorial", and it looks complicated. Just allocating hardware etc. I suppose that's part of the price for high-security. I don't have an x86 machine, and running it under a VM is too slow. https://genode.org/documentation/articles/sculpt-22-04 https://genode.org/documentation/articles/sculpt-22-04
subjectsigma 2y ago
Under no circumstances, it’s a microkernel for embedded systems. It’s like asking under what scenarios would you want to drive an ATV through New York. Technically possible, but that’s just not what it was made to do.
- blacklion 2y ago
  In practice, Linux is everywhere now, often in places where it should not be. Linux is truck/SUV of computer world if I can extend your analogy. It doesn't belong to center of big city, but it is here.
  - Affric 2y ago
    My conversations with people who have implemented Linux where it shouldn’t have been have essentially boiled down to it being easier to hire Linux developers than embedded systems developers
    - blacklion 2y ago
      Yes, it is "good enough" and familiar to everybody in industry. I understand that. But it doesn't mean we don't need to try harder.
    - ertian 2y ago
      It's easier to hire linux kernel devs, there's more documentation, tooling & examples, device drivers & filesystems are more widely available, etc. Every other OS has to play catch-up. They either need a killer app or lots of funding, or else they'll be stuck in a specific niche.
devit 2y ago
All circumstances where correctness and security are more important than maximum possible performance, once it's mature enough (which will probably never happen), since it provides a proper and secure architecture.
- RetroTechie 2y ago
  Which is basically everywhere. Well-designed microkernels have been proven to have only a minor impact on performance, afaik. Especially if said kernel is small enough to fit in a cpu's L1 or L2 cache entirely. With that in mind, I'd say there's few cases left where users would not want to take a minor performance hit, if that gets rid of entire classes of bugs & vulnerabilities. Reasons this isn't the norm these days are mostly historic. But going forward, a good midpoint would be popular OS kernels like Linux split into smaller components, while providing same user-space APIs. Along the lines of how XFree86 was modularized into a set of Xorg libraries. Maybe L4Linux could be an example? (dunno how modular that is though). On such a componentized system, components could be shared among multiple 'OS personalities'. Kinda like a multi-VM setup but finer grained with much more shared code, much reduced attack surface for individual components, while maintaining very strong isolation guarantees between components.
- snvzz 2y ago
  seL4 is not doing badly in the performance side. It is even seen beating Linux in the slides.

I've been waiting for a system like this for over a decade to use as my daily driver. An OS that runs with a capability model like this is immune to whole classes of security exploits that guarantee Linux, Windows, MacOS, etc. will never be secure. I was hoping Genode would get there sooner, and GNU Hurd should have gotten there years ago. Capabilities are the computing version of circuit breakers. They make it possible to run code without having to trust it. You can't do that with Linux, Windows, MacOS, et al. MULTICS could do it, but it was deemed too complex, at the time.

progbits 2y ago
Do you know if there is anything like that which can run OCI containers/lightweight VMs? I would love that as daily driver too for the same reasons, but realistically will have to run various Linux apps to be productive, so those could go into shortlived isolated sandboxes ala distrobox.
- dmm 2y ago
  Have tried Qubes? It provides security through isolated VMs. https://qubes-os.org https://qubes-os.org
  - snvzz 2y ago
    For some definition of isolated. A replacement with a more serious architecture based on seL4 is in the works[0]. 0. https://trustworthy.systems/projects/makatea/ https://trustworthy.systems/projects/makatea/
amluto 2y ago
FWIW, I would not trust seL4 on x86. Last time I checked, seL4’s interaction with the x86 architecture was not formally verified and looked quite buggy. Even a microkernel has three things that form part of the TCB: the part that interfaces with the even-lower-level stuff (interrupt and exception handlers, paging, memory model, etc), the interface it provides to its clients (syscalls and whatever it provides via syscalls), and the code that glues the first two parts together and implements the microkernel’s internal logic. The latter two, in seL4, are straightforward and formally verified. The former, on x86, not so much. AIUI, the situation on ARM is likely better.
- snvzz 2y ago
  >FWIW, I would not trust seL4 on x86. I would not trust any system on x86. >AIUI, the situation on ARM is likely better. Somewhat, but still not good. RISC-V is where it's at, when it comes to seL4. (seL4 participates in RISC-V)
sillywalk 2y ago
Have you tried Genode's Sculpt OS? "Sculpt is an open-source general-purpose OS. It combines Genode's microkernel architecture, capability-based security, sandboxed device drivers, and virtual machines in a novel operating system for commodity PC hardware and the PinePhone. Sculpt is used as day-to-day OS by the Genode developers." https://genode.org/download/sculpt https://genode.org/download/sculpt
- mikewarot 2y ago
  I tried it a while ago, it seemed like there wasn't enough there, there. I couldn't find the "Hello World" example that made sense to me. I get the idea of composing resources, but until I've got a file system and compiler running, and a command line I can do something with, it doesn't help. 8( I'm hoping that Sculpt 24.04 does the job for me. If I can make sense of it enough to get Free Pascal running on it, or even just a C compiler, and "Hello, World" in a CLI, we're off to the races.
  - sillywalk 2y ago
    I never really got it to do anything. I gather that this[0] is the "tutorial", and it looks complicated. Just allocating hardware etc. I suppose that's part of the price for high-security. I don't have an x86 machine, and running it under a VM is too slow. https://genode.org/documentation/articles/sculpt-22-04 https://genode.org/documentation/articles/sculpt-22-04

subjectsigma 2y ago

Under no circumstances, it’s a microkernel for embedded systems. It’s like asking under what scenarios would you want to drive an ATV through New York. Technically possible, but that’s just not what it was made to do.

blacklion 2y ago
In practice, Linux is everywhere now, often in places where it should not be. Linux is truck/SUV of computer world if I can extend your analogy. It doesn't belong to center of big city, but it is here.
- Affric 2y ago
  My conversations with people who have implemented Linux where it shouldn’t have been have essentially boiled down to it being easier to hire Linux developers than embedded systems developers
  - blacklion 2y ago
    Yes, it is "good enough" and familiar to everybody in industry. I understand that. But it doesn't mean we don't need to try harder.
  - ertian 2y ago
    It's easier to hire linux kernel devs, there's more documentation, tooling & examples, device drivers & filesystems are more widely available, etc. Every other OS has to play catch-up. They either need a killer app or lots of funding, or else they'll be stuck in a specific niche.

devit 2y ago

All circumstances where correctness and security are more important than maximum possible performance, once it's mature enough (which will probably never happen), since it provides a proper and secure architecture.

RetroTechie 2y ago
Which is basically everywhere. Well-designed microkernels have been proven to have only a minor impact on performance, afaik. Especially if said kernel is small enough to fit in a cpu's L1 or L2 cache entirely. With that in mind, I'd say there's few cases left where users would not want to take a minor performance hit, if that gets rid of entire classes of bugs & vulnerabilities. Reasons this isn't the norm these days are mostly historic. But going forward, a good midpoint would be popular OS kernels like Linux split into smaller components, while providing same user-space APIs. Along the lines of how XFree86 was modularized into a set of Xorg libraries. Maybe L4Linux could be an example? (dunno how modular that is though). On such a componentized system, components could be shared among multiple 'OS personalities'. Kinda like a multi-VM setup but finer grained with much more shared code, much reduced attack surface for individual components, while maintaining very strong isolation guarantees between components.
snvzz 2y ago
seL4 is not doing badly in the performance side. It is even seen beating Linux in the slides.