3 ms·

I'm fuzzy on what it would take for there to be a mainstream formally-verified micro-kernel capability-based OS. Is it probable for Linux to be gradually refact

by dmos62 5y ago

I'm fuzzy on what it would take for there to be a mainstream formally-verified micro-kernel capability-based OS. Is it probable for Linux to be gradually refactored into that, or are will it take a fundamentally new OS?

CameronNemo 5y ago
I think it would be possible to adapt some Linux drivers to run in a sandboxed capacity within a capability/microkernel system. IIRC there was once an L4 based project that integrated with Linux. https://en.wikipedia.org/wiki/L4Linux https://en.wikipedia.org/wiki/L4Linux
- shandor 5y ago
  L4Linux is just the usual Linux paravirtualized on top of one the L4 microkernels. We previously ran two instances of it on top of L4/Fiasco The problem with that is that you don't actually get that much benefits from the underlying microkernel. Linux is just the same old monolith, just better isolated from the other resources not exposed to this particular (para)virtualized kernel instance, so you end up isolating more or less complete systems from each other rather than getting the normal benefits of capability based microkernel architecture inside a single system. Now that's not nothing of course, but not usually what people are after when they're hoping for a usable, modern microkernel system.
darksaints 5y ago
There are already some attempts at creating new operating systems off of seL4. The most complete at the moment is Genode. There are also attempts to port existing OSes to seL4, such as qubes. None of these are particularly mature. In terms of creating a Linux replacement, drivers are the biggest hurdle. There are some attempts to programmatically port the netbsd suite of drivers, which seems to be the most promising. Apart from that, drivers will likely need to be ported manually. The GNU userland is also unlikely to be ported easily en-masse due to the capabilities-oriented security model, although some projects would definitely be easier than others. Things like SystemD would be a monstrous task. I personally think that apart from drivers, which can use traditional microkernel approaches, it's probably time to start implementing some of the better OS ideas that have come out in the last 30 years, as opposed to just trying to replicate a posix environment. For example, NuShell has a ton of promise, but isn't particularly posix-y.
- deleted 5y ago
  [deleted]

by dmos62 5y ago

CameronNemo 5y ago

I think it would be possible to adapt some Linux drivers to run in a sandboxed capacity within a capability/microkernel system. IIRC there was once an L4 based project that integrated with Linux. https://en.wikipedia.org/wiki/L4Linux https://en.wikipedia.org/wiki/L4Linux

shandor 5y ago
L4Linux is just the usual Linux paravirtualized on top of one the L4 microkernels. We previously ran two instances of it on top of L4/Fiasco The problem with that is that you don't actually get that much benefits from the underlying microkernel. Linux is just the same old monolith, just better isolated from the other resources not exposed to this particular (para)virtualized kernel instance, so you end up isolating more or less complete systems from each other rather than getting the normal benefits of capability based microkernel architecture inside a single system. Now that's not nothing of course, but not usually what people are after when they're hoping for a usable, modern microkernel system.

darksaints 5y ago

There are already some attempts at creating new operating systems off of seL4. The most complete at the moment is Genode. There are also attempts to port existing OSes to seL4, such as qubes. None of these are particularly mature. In terms of creating a Linux replacement, drivers are the biggest hurdle. There are some attempts to programmatically port the netbsd suite of drivers, which seems to be the most promising. Apart from that, drivers will likely need to be ported manually. The GNU userland is also unlikely to be ported easily en-masse due to the capabilities-oriented security model, although some projects would definitely be easier than others. Things like SystemD would be a monstrous task. I personally think that apart from drivers, which can use traditional microkernel approaches, it's probably time to start implementing some of the better OS ideas that have come out in the last 30 years, as opposed to just trying to replicate a posix environment. For example, NuShell has a ton of promise, but isn't particularly posix-y.

deleted 5y ago
[deleted]