Significant raise of reports (on the Linux Kernel Mailing List) https://lwn.net/Articles/1065620/
-
@cwebber@social.coop we need microkernel based operating systems with capability-based security enforcement, isolation of components from each other as a baseline assumption, and formal verification of the whole thing at both the code and spec level, and we need all of this quite urgently(se)L4 I think fits such criteria? It is already widely deployed (e.g. Apple's Secure Enclave).
Problematically? I don't think any of the L4 kernels were "self hosting" last I checked? Maybe that has changed.
BS such as that, would have received failing grades in the 1980s.
Alas, we live in a different era now, where cross compiling is de rigueur even if it is awful in practice.
If I had a wish granting fairy or whatever? I would totally task someone(s) to make the L4 microkernel family self-hosting, so it doesn't need a Linux to boot strap.
CC: @cwebber@social.coop
-
(se)L4 I think fits such criteria? It is already widely deployed (e.g. Apple's Secure Enclave).
Problematically? I don't think any of the L4 kernels were "self hosting" last I checked? Maybe that has changed.
BS such as that, would have received failing grades in the 1980s.
Alas, we live in a different era now, where cross compiling is de rigueur even if it is awful in practice.
If I had a wish granting fairy or whatever? I would totally task someone(s) to make the L4 microkernel family self-hosting, so it doesn't need a Linux to boot strap.
CC: @cwebber@social.coop@teajaygrey@snac.bsd.cafe @cwebber@social.coop yes, see further downthread -
@teajaygrey@snac.bsd.cafe @cwebber@social.coop yes, see further downthread@teajaygrey@snac.bsd.cafe @cwebber@social.coop and go learn about Genode / SculptOS
-
Sculpt/Genode seems really cool. I have long wanted to be able to hack OS components by working in userspace with languages like Scheme/LISP or Julia or Erlang or whatever. We have enough speed that we could let say firewalling / bridging / Routing be done in slightly less close-to-the-metal languages and gain tremendous flexibility. We can already see this kind of happening with eBPF and nftables and whatnot.
-
I'd set aside the formal verification requirement to get the rest of it. I really do think microkernels were the right way to go, it's just that in 1992 or whatever the consumer hardware wasn't up to the task. I think probably around 2005 or so the hardware started to be able to afford to do that. But that's approximately the time that VMs and containers took off. Now we have this giant mess.
"I really do think microkernels were the right way to go, it's just that in 1992 or whatever the consumer hardware wasn't up to the task."
100% microkernels were the right way to go!
They still are.
Alas, something threw a very angry GURU MEDIATION at the "in 1992 or whatever the consumer hardware wasn't up to the task" part of your statement. Amiga Workbench (a microkernel derived from the TripOS provenance) was absolutely the bees' knees on economical consumer hardware in the 1980s, and Commodore hadn't yet declared bankruptcy in 1992.
Heck, it's 2026 and I am pretty sure that there will probably still be Amiga related entries at @revisionparty@icosahedron.website
this weekend (wish I were there, alas $12,000ish USD in debt and it was going to cost around $2k USD just to fly there and have lodgings, so not this year).
Admittedly, the Amigas were pretty awesome insomuch as you could bypass the OS entirely. Kickstart was hella fast. Still is! Pretty sure my Amiga 2000 booted faster decades ago, with a SCSI hard drive (and my A1200 with IDE) than any contemporary "consumer" grade hardware shipping today, despite the Ghz in CPU clockspeeds these days (my Amigas' CPUs were measured in MHz and still sooooo speedy and usable).
CC: @linear@nya.social @cwebber@social.coop
-
M mttaggart@infosec.exchange shared this topic
