5 ms·

is SeL4 anywhere near usability by regular humans? is that even it's design purpose? Are we going to see the equivalent of Arch Sel4 that I can install, run way

is SeL4 anywhere near usability by regular humans? is that even it's design purpose? Are we going to see the equivalent of Arch Sel4 that I can install, run wayland to get a gui, and replace my linux stuff?

thatguy27 3y ago
>is that even it's design purpose? It is not. The closest thing you'll get to it that has the features you mention, is Qubes OS [0]. When it comes to the L4 family, Google's adoption of seL4 [1] might be interesting to you, and possibly L4Re [2] [3], which is open source (not their tooling, though) with commercial support. Edit: there's a bunch more open source activity in this field, but I'm not familiar with it. [0] https://www.qubes-os.org/ https://www.qubes-os.org/ [1] https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html https://opensource.googleblog.com/2022/10/announcing-kataos-... [2] https://l4re.org/ https://l4re.org/ [3] https://www.youtube.com/watch?v=x8jxINR-q40 https://www.youtube.com/watch?v=x8jxINR-q40
- thatguy27 3y ago
  A few completely uncurated L4Re links: https://github.com/kernkonzept/manifest/wiki#tutorials https://github.com/kernkonzept/manifest/wiki#tutorials https://l4re.org/rpi.html https://l4re.org/rpi.html https://l4re.org/doc/ https://l4re.org/doc/ https://www.youtube.com/watch?v=oqm6GOniQ_k https://www.youtube.com/watch?v=oqm6GOniQ_k https://www.youtube.com/watch?v=WGjAxsEAWRI https://www.youtube.com/watch?v=WGjAxsEAWRI
- thatguy27 3y ago
  A pretty cool video on seL4 where they give the red team root access on a Linux VM running inside of seL4, which controls a helicopter. https://www.youtube.com/watch?v=6s5FDX5PkZI https://www.youtube.com/watch?v=6s5FDX5PkZI
- transpute 3y ago
  Google Research, https://github.com/AmbiML/sparrow-manifest https://github.com/AmbiML/sparrow-manifest > Sparrow is a project to build a low-power secure embeded platform for Ambient ML applications. The target platform leverages RISC-V and OpenTitan. The Sparrow software includes a home-grown operating system named CantripOS, that runs on top of seL4 and (ignoring the seL4 kernel) is written almost entirely in Rust. > Archived on Jan 4 2024
  - pjmlp 3y ago
    Apparently they moved out of Github, https://github.com/AmbiML/we-moved https://github.com/AmbiML/we-moved
    - transpute 3y ago
      Thank you.
- snvzz 3y ago
  >QubesOS Look into Makatea[0], a seL4-based QubesOS-like system. 0. https://trustworthy.systems/projects/makatea/ https://trustworthy.systems/projects/makatea/
  - katehikes88 3y ago
    vaporware
marcosdumay 3y ago
Just to add an interesting information, the famous GNU Hurd project had the goal of making a system like L4 usable by regular humans. (Later on, they changed it to work literally with L4.) That doesn't mean any project to do that will have the fate of Hurd. But it is a huge and complicated task.
- yjftsjthsd-h 3y ago
  My impression, corroborated by https://www.gnu.org/software/hurd/microkernel/l4.html https://www.gnu.org/software/hurd/microkernel/l4.html , is that HURD looked at L4 but never actually jumped from mach.
  - anthk 3y ago
    This is interesting. GNU inherits a lot from ITS, DDT and Emacs openness, where they had no security at all and you could edit the files from the whole system and import processes locally and over the network.The security there was to behave like a lady/gentelman and help/get helped. Also, crackers weren't interested as everyone could see everything users where doing at any moment. Data security? Restoring from tapes. By setting up an open system on top of a permissions bound system (Unix) having limitations as an user looks really weird and with full of rough edges everywhere, with limited permissions even to mount a hard disk image. Namespaces in Hurd (+ maybe guix) solve that by giving the user lots of freedom to install and share whatever it wants without breaking a system.
  - marcosdumay 3y ago
    That would explain why it never seemed to move forward. TBF, that makes it quite explicit that the problem of Hurd never getting ready was due to the project governance (as in "this is not a goal"). A project that uses Mach could never get big.
n3v3r3v3r 3y ago
Kind of actually, just depends how much you mean by "regular human"--it's not super popular but the Sculpt OS[1] release of Genode is a pretty solid system runnable on top of SeL4 that supports emulation for the features it's otherwise missing (a la wifibox). Have not personally used it yet but I believe the developers dogfood it on some decently modern hardware (think Framework). It has a very specific design ethos and aesthetic[2] that I find super compelling. [1] https://genode.org/download/sculpt https://genode.org/download/sculpt [2] https://genode.org/about/2020-09-16-sculpt.png https://genode.org/about/2020-09-16-sculpt.png
- snvzz 3y ago
  Running Linux in VMs covered the gap and allowed them to dogfood Genode for years. But today, they have native modern webbrowser with native 3d acceleration and native audio. Genode has gone very far.
snvzz 3y ago
Managarm[0] is a microkernel-based but unrelated to seL4 system that aims at being a drop-in replacement for Linux. 0. https://managarm.org/ https://managarm.org/
- naasking 3y ago
  Very interesting. I couldn't find a high-level overview of how they're approaching this though. It seems like they might be re-implementing some Linux APIs, but I have the impression that it runs all those APIs in a single process, like hosting a UNIX or Linux kernel as a guest OS, which would be a fairly large TCB. Is there a reference document that describes the system architecture in more detail? Their handbook is a little thin on details.
  - snvzz 3y ago
    I agree such a document would be helpful. However, there's a talk[0] from three years ago. I would imagine the architecture has changed since then. 0. https://www.youtube.com/watch?v=BzwpdOpNFpQ https://www.youtube.com/watch?v=BzwpdOpNFpQ
    - naasking 3y ago
      This was the best I found: https://docs.managarm.org/handbook/sys-arch/thoreir/index.html https://docs.managarm.org/handbook/sys-arch/thoreir/index.ht... So as I suspected, posix-subsystem is a single process that provides the POSIX support for all other process, so it's a single point of failure: https://docs.managarm.org/handbook/sys-arch/posix/index.html https://docs.managarm.org/handbook/sys-arch/posix/index.html It's interesting that they have some kind of subsystem to run code in kernel space too, very against typical microkernel thinking for isolation/safety reasons.
      - snvzz 3y ago
        from the documentation, it is not clear to me what shape the posix subsystem has. It might be a library. thor seems to be an actual "bottleneck".
dark-star 3y ago
There's an early version of the Win32 personality atop SeL4 called NeptuneOS (https://github.com/cl91/NeptuneOS https://github.com/cl91/NeptuneOS)
darksaints 3y ago
Nowhere near the usability of Linux, let alone something like MacOS. I'd be really happy if I could easily deploy small self-contained embedded applications using general purpose ARMv8 processors. Like one would do with an infotainment system for a car, which is currently done primarily with QNX.
- forty 3y ago
  > Nowhere near the usability of Linux, let alone something like MacOS. Like if there was a clear order of usability between Linux and MacOS :) it's more a matter of habits and preferences (and religion maybe for some ^^) than anything else.
  - naasking 3y ago
    Mac OS clearly has more polish and deeper integration, but these days the difference isn't the huge chasm that most think.
    - DEADMINCE 3y ago
      MacOS seemed downright rough the few times I've had to use it. It's not intuitive and stuff often seems buggy until you get that dreaded spinning pinwheel...
      - naasking 3y ago
        "Intuitive" is not an objective property, it's too polluted by habits you've learned from other systems. But we can say this: there's nothing intuitive about Windows' incomplete transition to the new settings app that still sometimes requires you to jump to the old control panel system; there's nothing intuitive about Linux' 50 desktop environments, each with their own incomplete configuration systems. In any kind of match up, MacOS will win on simplicity and intuitiveness hands down simply because every other option is just much worse.
        DEADMINCE 3y ago

thatguy27 3y ago

>is that even it's design purpose? It is not. The closest thing you'll get to it that has the features you mention, is Qubes OS [0]. When it comes to the L4 family, Google's adoption of seL4 [1] might be interesting to you, and possibly L4Re [2] [3], which is open source (not their tooling, though) with commercial support. Edit: there's a bunch more open source activity in this field, but I'm not familiar with it. [0] https://www.qubes-os.org/ https://www.qubes-os.org/ [1] https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html https://opensource.googleblog.com/2022/10/announcing-kataos-... [2] https://l4re.org/ https://l4re.org/ [3] https://www.youtube.com/watch?v=x8jxINR-q40 https://www.youtube.com/watch?v=x8jxINR-q40

thatguy27 3y ago
A few completely uncurated L4Re links: https://github.com/kernkonzept/manifest/wiki#tutorials https://github.com/kernkonzept/manifest/wiki#tutorials https://l4re.org/rpi.html https://l4re.org/rpi.html https://l4re.org/doc/ https://l4re.org/doc/ https://www.youtube.com/watch?v=oqm6GOniQ_k https://www.youtube.com/watch?v=oqm6GOniQ_k https://www.youtube.com/watch?v=WGjAxsEAWRI https://www.youtube.com/watch?v=WGjAxsEAWRI
thatguy27 3y ago
A pretty cool video on seL4 where they give the red team root access on a Linux VM running inside of seL4, which controls a helicopter. https://www.youtube.com/watch?v=6s5FDX5PkZI https://www.youtube.com/watch?v=6s5FDX5PkZI
transpute 3y ago
Google Research, https://github.com/AmbiML/sparrow-manifest https://github.com/AmbiML/sparrow-manifest > Sparrow is a project to build a low-power secure embeded platform for Ambient ML applications. The target platform leverages RISC-V and OpenTitan. The Sparrow software includes a home-grown operating system named CantripOS, that runs on top of seL4 and (ignoring the seL4 kernel) is written almost entirely in Rust. > Archived on Jan 4 2024
- pjmlp 3y ago
  Apparently they moved out of Github, https://github.com/AmbiML/we-moved https://github.com/AmbiML/we-moved
  - transpute 3y ago
    Thank you.
snvzz 3y ago
>QubesOS Look into Makatea[0], a seL4-based QubesOS-like system. 0. https://trustworthy.systems/projects/makatea/ https://trustworthy.systems/projects/makatea/
- katehikes88 3y ago
  vaporware

marcosdumay 3y ago

Just to add an interesting information, the famous GNU Hurd project had the goal of making a system like L4 usable by regular humans. (Later on, they changed it to work literally with L4.) That doesn't mean any project to do that will have the fate of Hurd. But it is a huge and complicated task.

yjftsjthsd-h 3y ago
My impression, corroborated by https://www.gnu.org/software/hurd/microkernel/l4.html https://www.gnu.org/software/hurd/microkernel/l4.html , is that HURD looked at L4 but never actually jumped from mach.
- anthk 3y ago
  This is interesting. GNU inherits a lot from ITS, DDT and Emacs openness, where they had no security at all and you could edit the files from the whole system and import processes locally and over the network.The security there was to behave like a lady/gentelman and help/get helped. Also, crackers weren't interested as everyone could see everything users where doing at any moment. Data security? Restoring from tapes. By setting up an open system on top of a permissions bound system (Unix) having limitations as an user looks really weird and with full of rough edges everywhere, with limited permissions even to mount a hard disk image. Namespaces in Hurd (+ maybe guix) solve that by giving the user lots of freedom to install and share whatever it wants without breaking a system.
- marcosdumay 3y ago
  That would explain why it never seemed to move forward. TBF, that makes it quite explicit that the problem of Hurd never getting ready was due to the project governance (as in "this is not a goal"). A project that uses Mach could never get big.

n3v3r3v3r 3y ago

Kind of actually, just depends how much you mean by "regular human"--it's not super popular but the Sculpt OS[1] release of Genode is a pretty solid system runnable on top of SeL4 that supports emulation for the features it's otherwise missing (a la wifibox). Have not personally used it yet but I believe the developers dogfood it on some decently modern hardware (think Framework). It has a very specific design ethos and aesthetic[2] that I find super compelling. [1] https://genode.org/download/sculpt https://genode.org/download/sculpt [2] https://genode.org/about/2020-09-16-sculpt.png https://genode.org/about/2020-09-16-sculpt.png

snvzz 3y ago
Running Linux in VMs covered the gap and allowed them to dogfood Genode for years. But today, they have native modern webbrowser with native 3d acceleration and native audio. Genode has gone very far.

snvzz 3y ago

Managarm[0] is a microkernel-based but unrelated to seL4 system that aims at being a drop-in replacement for Linux. 0. https://managarm.org/ https://managarm.org/

naasking 3y ago
Very interesting. I couldn't find a high-level overview of how they're approaching this though. It seems like they might be re-implementing some Linux APIs, but I have the impression that it runs all those APIs in a single process, like hosting a UNIX or Linux kernel as a guest OS, which would be a fairly large TCB. Is there a reference document that describes the system architecture in more detail? Their handbook is a little thin on details.
- snvzz 3y ago
  I agree such a document would be helpful. However, there's a talk[0] from three years ago. I would imagine the architecture has changed since then. 0. https://www.youtube.com/watch?v=BzwpdOpNFpQ https://www.youtube.com/watch?v=BzwpdOpNFpQ
  - naasking 3y ago
    This was the best I found: https://docs.managarm.org/handbook/sys-arch/thoreir/index.html https://docs.managarm.org/handbook/sys-arch/thoreir/index.ht... So as I suspected, posix-subsystem is a single process that provides the POSIX support for all other process, so it's a single point of failure: https://docs.managarm.org/handbook/sys-arch/posix/index.html https://docs.managarm.org/handbook/sys-arch/posix/index.html It's interesting that they have some kind of subsystem to run code in kernel space too, very against typical microkernel thinking for isolation/safety reasons.
    - snvzz 3y ago
      from the documentation, it is not clear to me what shape the posix subsystem has. It might be a library. thor seems to be an actual "bottleneck".

dark-star 3y ago

There's an early version of the Win32 personality atop SeL4 called NeptuneOS (https://github.com/cl91/NeptuneOS https://github.com/cl91/NeptuneOS)

darksaints 3y ago

Nowhere near the usability of Linux, let alone something like MacOS. I'd be really happy if I could easily deploy small self-contained embedded applications using general purpose ARMv8 processors. Like one would do with an infotainment system for a car, which is currently done primarily with QNX.

forty 3y ago
> Nowhere near the usability of Linux, let alone something like MacOS. Like if there was a clear order of usability between Linux and MacOS :) it's more a matter of habits and preferences (and religion maybe for some ^^) than anything else.
- naasking 3y ago
  Mac OS clearly has more polish and deeper integration, but these days the difference isn't the huge chasm that most think.
  - DEADMINCE 3y ago
    MacOS seemed downright rough the few times I've had to use it. It's not intuitive and stuff often seems buggy until you get that dreaded spinning pinwheel...
    - naasking 3y ago
      "Intuitive" is not an objective property, it's too polluted by habits you've learned from other systems. But we can say this: there's nothing intuitive about Windows' incomplete transition to the new settings app that still sometimes requires you to jump to the old control panel system; there's nothing intuitive about Linux' 50 desktop environments, each with their own incomplete configuration systems. In any kind of match up, MacOS will win on simplicity and intuitiveness hands down simply because every other option is just much worse.
      - DEADMINCE 3y ago