[HN Gopher] From L3 to seL4: 20 years of L4 microkernels (2013) ...
___________________________________________________________________
From L3 to seL4: 20 years of L4 microkernels (2013) [video]
Author : tambourine_man
Score : 65 points
Date : 2024-04-15 05:27 UTC (17 hours ago)
(HTM) web link (www.youtube.com)
(TXT) w3m dump (www.youtube.com)
| defrost wrote:
| SOSP 2013
|
| Proceedings of the Twenty-Fourth ACM Symposium on Operating
| Systems Principles November 2013
|
| https://dl.acm.org/doi/10.1145/2517349.2522720
| BSDobelix wrote:
| Question, and please don't get mad at me if I'm fundamentally
| wrong.
|
| Are there any projects trying to make a universal UNIX operating
| system with sel4?
|
| I know of Genode, but is there anything more simple/traditional?
|
| PS: Helios is also there but not based directly on seL4
| hresvelgr wrote:
| Not Unix but Lions OS[1]. Also, why would you want to build
| Unix on top of seL4? I think we can have better ideas than that
| in today's state of the art.
|
| [1] https://trustworthy.systems/projects/LionsOS/
| BSDobelix wrote:
| >Also, why would you want to build Unix on top of seL4?
|
| Thank you very much for the link, and yes you are absolutely
| right. I should have wrote unix'i or plan9'i or better just a
| universal operating-system, i meant with that not just a
| hypervisor but a "real/full" os on top of seL4.
| TacticalCoder wrote:
| > I think we can have better ideas than that in today's state
| of the art.
|
| And yet Unix is powering all the supercomputers, six of the
| seven magnificent seven, the AI revolution, nearly every
| single computer in all the datacenters around the world,
| billions of "small" devices, etc.
|
| Can we _really_ do that much better or is it just hubris?
|
| At what point another approach, like the one Windows used,
| would be considered a failure? Once it's only powering the
| corporate world and not much else?
|
| And at what point another approach would be considered a
| success? Once it has replaced Unix on all the supercomputers
| and in all the datacenters?
|
| People like to snob Unix but the fact is: the world runs on
| Unix.
|
| P.S: I wrote "Unix" with an 'i' and not a star because I have
| no clue how to write a star in HN's powerful text editor ; )
| onjectic wrote:
| The world runs on Unix and as a consequence, computer
| viruses, malware, spyware and ransomware are all common
| vocabulary terms. We traded this security away for nothing.
|
| Linus Torvalds would have told you its system call
| performance, but Linux is also forced to solve these
| problems with things like futexes and io_uring, which carry
| over just as easily to microkernels.
|
| Nowadays the excuse is side-channel attacks make any
| attempts at security pointless anyways so the kernel has
| exploded in size and complexity. This is insane logic, not
| least of all because side-channel attacks are read-only and
| can't embed themselves into your system permanently through
| a bug in a browser JIT.
|
| Linux is used purely because of all of its drivers and
| familiarity. Not on technical merits.
| 4ad wrote:
| The problem with Unix is the abstractions it provides, not its
| implementation. Basing Unix off seL4 changes nothing of what
| makes Unix inadequate in 2024.
| tremon wrote:
| The problem with Unix is that the abstractions don't match
| today's adversarial computing environment. If seL4 can
| provide kernel-level process (tree) isolation, which part of
| Unix is inadequate for 2024?
| onjectic wrote:
| It's fundamentally full of concepts incompatible with
| capability based security principles, which are provably
| secure. Access control lists are provably insecure. POSIX
| resource management is archaic. It's not possible to define
| "ownership" clearly on a Unix system.
|
| You could certainly write a Unix abstraction layer on top
| of seL4, or more commonly treat seL4 as a hypervisor, but
| you would not be able simply use a Unix interface to
| interact with seL4 and get all of it's benefits.
|
| Capability based systems don't magically carry their
| desired properties up the abstraction ladder, they have to
| be maintained and the designer has to be vigilant to avoid
| introducing ambient authority by using capability based
| design themselves.
|
| Genode is an example of a layer over seL4 that follows
| these principles.
| anthk wrote:
| GNU Hurd.
|
| Also, why it's inadequate?
|
| "Unix 2.0" which is basically plan9/9front, uses namespaces,
| cpu, auth and so on 'servers' to authenticate users and even
| shared devices over the network.
| jacobgorm wrote:
| I think one problem is that SEL4 lacks proper multi-core
| support. According to the FAQ it has not been formally
| verified, and it relies on a big lock for everything. This is
| fine when powering a security chip like T2, but not so fine if
| you are trying to replace UNIX.
| adamretter wrote:
| That video is from 2013. Is anyone aware of an update for the
| last ten years which covers 2013 to 2023? I would like to
| understand if seL4 is still considered "current" or there have
| been newer developments since then that are worth considering. I
| have searched around a bit, and apart from Google's Fuscia
| Zircon, or Unikernel's like UniKraft, other L4 spin-offs and XNU
| I am not finding too much about newer modern microkernels.
| mike_hearn wrote:
| There was an seL4 summit last year:
|
| https://www.youtube.com/@seL4/videos
|
| Anyway the trend has been that regular mainstream kernels
| steadily adopt more microkernel-like features when it can be
| shown to not harm performance too much. MacOS/iOS aren't
| technically microkernels, but they incorporate Mach into the
| core and a typical system will have thousands of possible
| servers that can be reached via Mach. Those servers are all
| sandboxed pretty heavily too, so you get the security benefits.
| The core filesystem and networking stack do still run in kernel
| mode because there aren't many benefits there (moving them to
| user space doesn't remove them from the TCB and) but over time
| more and more stuff has been kicked out to user space. The same
| can be seen in Windows where over time more subsystems get
| extracted to user space servers.
|
| Linux has a less well defined architecture than Apple's
| platforms and there are way fewer services reachable via DBUS
| than on macOS, but the same trends can be seen there too with
| support for direct user space access to devices, FUSE, user
| space schedulers, eBPF and so on.
|
| So there isn't I think much interest in pure microkernels now.
| Linux has got flexible enough that you can make it as micro-
| kernelly as you want, but the current balance seems about right
| for nearly all use cases. The stuff that remains in-kernel
| generally isn't a big source of vulnerabilities, moving stuff
| to userspace wouldn't help anyway but would reduce performance
| a lot.
| bewo001 wrote:
| For high-speed networking, exokernel concepts are now being
| used in the form of DPDK (user space) and eBPF/XDP (user code
| dynamically verified and loaded into kernel space).
| Exokernels aimed to move kernel functionalities not into a
| bunch of separate processes like microkernels, but into
| libraries. In the late 1990s, I worked on such a system which
| unfortunately fell victim to the dotcom crash.
|
| https://en.wikipedia.org/wiki/Exokernel
| vbezhenar wrote:
| I don't see this trend with Linux. FUSE is very old and does
| not seem to get much traction. User space schedulers: where
| are they used? eBPF is like the other way around: people want
| to run more stuff inside kernel.
|
| Honestly I feel that Linux server users are performance
| freaks and will kill for 0.1% performance. So it's very
| unlikely that they'll trade anything for it. They don't need
| stability, they'll just recreate server if necessary. They
| need absolute minimum of security (otherwise they would use
| VMs instead of containers).
| mike_hearn wrote:
| On Linux it's more about what can be done. Agree that
| server users don't care about microkernels.
| bregma wrote:
| QNX 8.0 was just released. The version bump represents a
| rewritten microkernel.
| speed_spread wrote:
| Is QNX 8 seL4 based?
| DoingIsLearning wrote:
| QNX predates the first L4 release by at least 10 years.
| Unless they had a major rewrite I wouldn't assume so.
| speed_spread wrote:
| The comment I was replying to seemed to imply that QNX
| 8.0 is a full rewrite. I'm not sure how relevant that
| statement was here, unless the rewrite is seL4 based.
| ahartmetz wrote:
| Interestingly, QNX designers have learned and applied one
| of the same lessons as L4 designers: asynchronous
| messaging is messy regarding resource management and
| slower than well-executed synchronous messaging. QNX and
| L4 both use synchronous messaging for the vast majority
| of tasks.
| panick21_ wrote:
| seL4 is still being worked on. There are recent changes to the
| wat time is tracked. I would say in terms of research seL4 is
| still up there. The current trend is very much on verification
| of user space and also verification chains down to RISC-V.
| wittystick wrote:
| Probably the biggest development in seL4 since this is the
| MCS (mixed criticality systems) addition, which provides
| capabilities for budgeting CPU usage to give guarantees for
| components that need higher priority. There's some videos by
| Gernot Heiser on YouTube covering it.
| riedel wrote:
| I just thought if L4 pistachio was a thing in the days (C++
| rewrite, the new thing when I did my masters in Karlsruhe),
| someone must have written a microkernel OS in Rust by now and
| here it is: https://www.redox-os.org/ . So sad that Liedke died
| so early, I really wonder what L5 would have looked like.
| gnufx wrote:
| I don't know how complete it is -- it doesn't list DeVault's
| Helios -- but various projects are listed at
| http://www.microkernel.info/
| lasiotus wrote:
| Moturus OS (https://github.com/moturus/motor-os) has a newer
| microkernel.
___________________________________________________________________
(page generated 2024-04-15 23:02 UTC)