News for hackers. Stuff that matters.
Re:SeL4 Device Driver Framework 0.4.0 by snapplebobapple on Tuesday April 09, 2024 @09:15AM (#39979106)
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?
Re:SeL4 Device Driver Framework 0.4.0 by n3v3r3v3r on Tuesday April 09, 2024 @09:56AM (#39979483)
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

[2] https://genode.org/about/2020-09-16-sculpt.png

Re:SeL4 Device Driver Framework 0.4.0 by snvzz on Tuesday April 09, 2024 @10:43PM (#39986465)
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.

Re:SeL4 Device Driver Framework 0.4.0 by thatguy27 on Tuesday April 09, 2024 @09:25AM (#39979203)
>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/

[1] https://opensource.googleblog.com/2022/10/announcing-kataos-...

[2] https://l4re.org/

[3] https://www.youtube.com/watch?v=x8jxINR-q40

Re:SeL4 Device Driver Framework 0.4.0 by transpute on Tuesday April 09, 2024 @10:14AM (#39979653)
Google Research, 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

Re:SeL4 Device Driver Framework 0.4.0 by pjmlp on Tuesday April 09, 2024 @11:41AM (#39980625)
Apparently they moved out of Github, https://github.com/AmbiML/we-moved
Re:SeL4 Device Driver Framework 0.4.0 by transpute on Wednesday April 10, 2024 @05:05PM (#39995709)
Thank you.
Re:SeL4 Device Driver Framework 0.4.0 by thatguy27 on Tuesday April 09, 2024 @09:37AM (#39979299)
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

Re:SeL4 Device Driver Framework 0.4.0 by snvzz on Tuesday April 09, 2024 @10:22AM (#39979741)
>QubesOS

Look into Makatea[0], a seL4-based QubesOS-like system.

0. https://trustworthy.systems/projects/makatea/

Re:SeL4 Device Driver Framework 0.4.0 by katehikes88 on Tuesday April 16, 2024 @04:33PM (#40056820)
vaporware
Re:SeL4 Device Driver Framework 0.4.0 by marcosdumay on Tuesday April 09, 2024 @09:49AM (#39979410)
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.

Re:SeL4 Device Driver Framework 0.4.0 by yjftsjthsd-h on Tuesday April 09, 2024 @11:36AM (#39980567)
My impression, corroborated by https://www.gnu.org/software/hurd/microkernel/l4.html , is that HURD looked at L4 but never actually jumped from mach.
Re:SeL4 Device Driver Framework 0.4.0 by anthk on Tuesday April 09, 2024 @01:08PM (#39981529)
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.

Re:SeL4 Device Driver Framework 0.4.0 by marcosdumay on Tuesday April 09, 2024 @01:12PM (#39981581)
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.

Re:SeL4 Device Driver Framework 0.4.0 by snvzz on Tuesday April 09, 2024 @10:36AM (#39979906)
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/

Re:SeL4 Device Driver Framework 0.4.0 by naasking on Tuesday April 09, 2024 @12:53PM (#39981352)
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.
Re:SeL4 Device Driver Framework 0.4.0 by snvzz on Wednesday April 10, 2024 @06:48PM (#39996498)
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

Re:SeL4 Device Driver Framework 0.4.0 by naasking on Friday April 12, 2024 @09:20AM (#40012413)
This was the best I found: 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

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.

Re:SeL4 Device Driver Framework 0.4.0 by snvzz on Friday April 12, 2024 @12:06PM (#40014444)
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".

Re:SeL4 Device Driver Framework 0.4.0 by dark-star on Tuesday April 09, 2024 @01:25PM (#39981779)
There's an early version of the Win32 personality atop SeL4 called NeptuneOS (https://github.com/cl91/NeptuneOS)
Re:SeL4 Device Driver Framework 0.4.0 by darksaints on Tuesday April 09, 2024 @02:29PM (#39982529)
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.

Re:SeL4 Device Driver Framework 0.4.0 by forty on Tuesday April 09, 2024 @03:13PM (#39983069)
> 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.

Re:SeL4 Device Driver Framework 0.4.0 by naasking on Tuesday April 09, 2024 @09:04PM (#39985946)
Mac OS clearly has more polish and deeper integration, but these days the difference isn't the huge chasm that most think.
Re:SeL4 Device Driver Framework 0.4.0 by DEADMINCE on Tuesday April 09, 2024 @09:16PM (#39986003)
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...
Re:SeL4 Device Driver Framework 0.4.0 by naasking on Wednesday April 10, 2024 @12:45AM (#39987037)
"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.

Re:SeL4 Device Driver Framework 0.4.0 by DEADMINCE on Wednesday April 10, 2024 @03:14AM (#39987842)
> "Intuitive" is not an objective property, it's too polluted by habits you've learned from other systems.

To an extent, but then the test is seeing how people who have never used any system interact. I maintain the MacOS paradigm is objectively less intuitive than alternatives.

> 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

Sure, that's clumsy. Not really relevant though.

> In any kind of match up, MacOS will win on simplicity and intuitiveness hands down simply because every other option is just much worse.

Strongly disagree. MacOS comes in behind Windows for certain, and likely behind a couple of FOSS DEs as well. Windows has issues, but usability isn't one of them.