5 ms·

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 class

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 3y 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 3y ago
  Have tried Qubes? It provides security through isolated VMs. https://qubes-os.org https://qubes-os.org
  - snvzz 3y 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 3y 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 3y 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 3y 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 3y 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 3y 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

progbits 3y 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 3y ago
Have tried Qubes? It provides security through isolated VMs. https://qubes-os.org https://qubes-os.org
- snvzz 3y 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 3y 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 3y 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 3y 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 3y 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 3y 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