[HN Gopher] The SeL4 Microkernel: An Introduction [pdf]
___________________________________________________________________
The SeL4 Microkernel: An Introduction [pdf]
Author : snvzz
Score : 173 points
Date : 2025-03-23 11:09 UTC (11 hours ago)
(HTM) web link (sel4.systems)
(TXT) w3m dump (sel4.systems)
| coldblues wrote:
| https://genode.org/index
|
| An operating system with seL4 support
| Rochus wrote:
| Are there notable uses of Genode?
| hackpelican wrote:
| Does the OS that lies on top of this kernel need to be formally
| verified as well for the security guarantees to hold?
| Koshkin wrote:
| In absolute terms, sure. At the practical level, you can find a
| partial answer in the section 7.2 of the paper.
| snvzz wrote:
| The guarantees offered by the kernel cannot be subverted by
| unprivileged processes running on it.
|
| Of course, the kernel is not very useful on its own, thus the
| design of drivers, filesystem servers and other services
| running on top of the kernel is still relevant.
|
| Note that, unlike most other systems (including Linux) which
| are flawed at a fundamental level, seL4 actually enables the
| construction of a secure and reliable system.
| marcosdumay wrote:
| Well, as long as the hardware underneath it also enables the
| construction of a secure system.
|
| I don't think we have any such option right now.
| snvzz wrote:
| An example of this is timing side channels.
|
| Originating in an effort within seL4[0], there's ongoing
| work[1] in RISC-V to resolve this.
|
| 0. https://sel4.systems//Foundation/Summit/2022/slides/d1_1
| 1_fe...
|
| 1. https://lf-riscv.atlassian.net/browse/RVS-3569
| rubenbe wrote:
| No, that's the advantage is that the kernel/processes don't
| need to be trusted since your kernel guarantees the isolation.
| So you can have a Linux kernel running next to some high
| security process with the guarantee that they will be isolated
| (with the exception of allowed IPC)
| nabla9 wrote:
| No.
|
| But there are limitations. DMA off, only formally verified
| drivers
|
| It's also important to note that se4L multicore kernel is not
| yet verified.
| snvzz wrote:
| An IOMMU can help significantly with the driver problem,
| preventing a properly initialized driver from misbehaving and
| compromising the system.
| vacuity wrote:
| I want the magical IOMMUs that are maturely secure like
| MMUs are now. For now, I think various efforts in
| verifying/restricting/generating drivers are far better,
| although they fall particularly flat for proprietary
| drivers.
| snvzz wrote:
| >I want the magical IOMMUs that are maturely secure like
| MMUs are now.
|
| There's nothing magical about IOMMUs. They weren't
| invented last week either.
|
| Driver and hardware talk to each other using virtual
| memory instead of physical memory, preventing the
| scenario where a bug causes DMA to shit all over somebody
| else's memory.
|
| What holds is that systems that run drivers in supervisor
| mode have not been able to leverage an iommu to its full
| extent.
| vacuity wrote:
| My (admittedly limited) understanding is that IOMMUs
| still have practical roadblocks to being a solidly
| established part of the security of the computer. Of
| course they aren't bad in principle. Perhaps it's just
| that we aren't willing to eat the performance cost of
| making them more robust, but then performance is a
| tortured debate.
| nimish wrote:
| SeL4 is proof that microkernels are safe, efficient and scalable
| yet we are stuck with big honking Linux kernels in 2025. That
| said more and more drivers moving usermode anyway so it's a wash
| in the end.
| pjmlp wrote:
| I feel like containers and Kubernetes are microkernels revenge.
|
| They are for all practical purposes fulfilling the same role.
| bri3d wrote:
| Not at all? If anything they're filling the opposite role.
| Microkernels are about building interfaces which sandbox
| parts of the kernel. Namespaces are about giving sandboxed
| userlands full access to kernel interfaces.
| pjmlp wrote:
| Namespaces is one form of capabilities.
|
| Additionally a Linux kernel that exists for the sole
| purpose to keep KVM running, while everything that powers a
| cloud workload are Kubernetes pods, it is nothing more than
| a very fat microkernel, in terms of usefulness.
| bigstrat2003 wrote:
| Microkernel does not mean it uses capabilities. And "very
| fat microkernel" is an oxymoron. The _definition_ of a
| microkernel is that they do as little as possible in the
| kernel.
| pjmlp wrote:
| Of course it doesn't.
|
| The point is how Linux is being tamed to provide some of
| the concepts, in spite of its monolithic design.
|
| But naturally we can discuss minutiae instead.
| bri3d wrote:
| It's not "some of the concepts" nor minutae, though, it's
| literally the difference between a microkernel and a
| monolithic kernel.
|
| Presenting capabilities / namespaces to userland is a
| completely different and in the case of Linux, orthogonal
| thing to presenting capabilities/namespaces to kernel
| services. I guess you could argue that the concept of
| capabilities came from microkernels, but when it's
| applied to only user space, it's just not really related
| to a microkernel anymore at all.
|
| That's basically the whole problem with capabilities and
| especially their application in namespaces from a
| security standpoint in Linux: they try to firewall these
| little boxes from each other but the kernel they're all
| talking to is still one big blob. And this difference is
| meaningful in a security sense, not just some theory hand
| waving. https://www.crowdstrike.com/en-
| us/blog/cve-2022-0185-kuberne... is just one good
| example, but entire classes of mitigations are rendered
| meaningless by the ability to unshare into a box that
| lets an attacker touch exploitable kernel surface area
| which is not further isolated.
| afiori wrote:
| Imo the microness is not about size but about the
| architecture of running drivers/services in fault-
| resistant separation from the kernel
| vacuity wrote:
| The dose makes the poison; we're still a long way from
| fulling embracing microkernels and capabilities. Security
| is a holistic property and encompasses finer details too.
| I want a small TCB. I want capabilities pervasively. And
| in pursuit of modularity and abstraction, I want to be
| able to choose the components I want and take those
| burdens myself. It's a bit silly seeing the nth SIGOPS-
| SOSP paper on how Linux can be improved by integrating
| userspace scheduling.
| pjmlp wrote:
| It is the same in safer systems programming languages, we
| already have the concept since 1961, but apparently
| making the industry take the right decisions is a tenuous
| path until something finally makes good ideas stick and
| gain adoption.
| cedws wrote:
| I heard a joke somewhere that sel4 is even more successful than
| Linux because it is running below ring 0 in every Intel chip
| shipped in the past N decades, plus probably many others.
| CalChris wrote:
| Intel used a version of Minix rather than seL4 for its Intel
| Management Engine. [1] There was some controversy about this
| because they didn't give Andrew Tanenbaum proper credit. [2]
|
| [1] https://www.zdnet.com/article/minix-intels-hidden-in-
| chip-op...
|
| [2] https://www.cs.vu.nl/~ast/intel/
| mrkeen wrote:
| That is Minix, not SeL4.
| ianburrell wrote:
| Intel Management Engine is a separate microcontroller
| integrated into the chipsets. Recent ones are Intel Quark x86
| CPU and Minix 3 OS.
| ryao wrote:
| seL4 having a proof of correctness does not mean all
| microkernels do. In fact, seL4 is the only microkernel that has
| a proof of correctness. If you build on top of it in the
| microkernel way, you quickly find that it is not performant.
| That is why NT and XNU both abandoned their microkernel origins
| in favor of becoming monolithic kernels.
| mastax wrote:
| I've seen this argument play out many times. I believe the
| next line is: "QNX proved that micro kernels can be fast
| given clever message passing syscall design."
|
| "I remember running the QNX demo disc: an entire graphical
| operating system on a single 1.44MB floppy! Whatever happened
| to them?"
|
| "They got bought by blackberry, which ended as you'd expect.
| QNX had a lot of success in automotive though."
|
| "Nowadays Linux and Android are dominant in new cars, though,
| proving once and for all that _worse is better._ "
|
| _exeunt_. End Scene
| ryao wrote:
| Nice use of Latin. mihi placet.
| nine_k wrote:
| Also an illustration how an open-source solution, even if
| technically inferior, would displace a closed-source
| solution, even if technically superior, unless there is a
| huge moat. And huge moats usually exist only in relatively
| narrow niches.
| vacuity wrote:
| It turns out that success is composed of 90% luck, 10%
| marketing, and 5% talent/technical advantage. A
| rhetorical question: how do you entice people to turn a
| movement into a revolution when it isn't likely the
| movement will succeed?
| necovek wrote:
| Another rhetorical question: out of
| luck/marketing/technical advantage, which one is
| contributing the most to the extra 5% out of 105% of all
| the components success can be attributed to?
| pjmlp wrote:
| NT in Windows 11 has very little to do with the monolithic
| kernel story that keeps being repeated.
|
| Not only did the graphics stack moved again back into
| userspace, there is now a complete userspace drivers stack,
| and VBS (Virtualization-based security) for several kernel
| components that run on their mini Hyper-V island, talking via
| IPC with the rest of the kernel.
|
| Likewise on XNU land, Apple has started a crusade already a
| few years ago, to move all kexts into userspace, no more
| drivers in the kernel beyond the ones Apple considers
| critical.
|
| In both cases, they never were a pure monolithic kernel, due
| to the way walls were introduced with kernel level IPC to
| talk across modules, instead of straight function calls.
| netbsdusers wrote:
| NT and XNU never had microkernel origins - Cutler explicitly
| refuted this at a conference in the early 1990s (if anyone
| remembers which, kindly share) and NeXTSTEP forked Mach at
| version 2.5, which was not a microkernel (see https://cseweb.
| ucsd.edu/classes/wi11/cse221/papers/accetta86...). XNU
| retained this monolithic architecture (as did Tru64 and other
| systems that trace their heritage to Mach prior to its
| version 3).
| danieldk wrote:
| _NeXTSTEP forked Mach at version 2.5_
|
| Various sources state that they rebased to OSF Mach Kernel
| 7.3, which was based on Mach 3 and parts of Mach 4. The OSF
| MK ancestry of macOS XNU can still be seen in paths:
|
| https://github.com/apple-oss-
| distributions/xnu/tree/main/osf...
| rhet0rica wrote:
| This is quite a ship-of-Theseus problem. Steve Jobs hired
| Avi Tevanian to work at NeXT on the Mach kernel, and
| later brought Tevanian to Apple; he was still working on
| the Mach/Darwin kernel as late as the first iPhone
| release. There is a reasonable argument to be made that
| the OSF kernel is actually the derivative, by default.
| p_ing wrote:
| There are a few references to the OSF Mach kernel from
| '98 in a few files, such as https://github.com/apple-oss-
| distributions/xnu/blob/main/osf...
|
| EDIT: Apple calls out Mach 3.0.
|
| https://developer.apple.com/library/archive/documentation
| /Da...
|
| https://developer.apple.com/library/archive/documentation
| /Da...
|
| Apple took Mach 3.0 and collapsed it into a single
| address space for performance purposes. Certainly
| reasonable.
| netbsdusers wrote:
| As far as I can tell (this isn't gospel, just something
| I've inferred as the only reasonable explanation from
| comparing the codebases), Apple reconstructed a Mach 2.5
| style kernel, like NeXTSTEP had, from fresh codebases
| (OSF Mach and 4.4BSD-Lite2), perhaps because 4.3BSD was
| still encumbered at the time.
|
| The Darwin 0.1 and 0.3 releases contain the old kernel,
| derived directly from NeXTSTEP, and that's the direct
| derivative of Mach 2.5. The later XNU appears to be a
| reconstruction of that kernel with unencumbered code and
| that's also when IOKit replaced DriverKit.
| rhet0rica wrote:
| In more recent interviews Cutler has been firm that the NT
| kernel was designed pragmatically, a view that Tevanian
| also evidently later adopted, as evident with the great
| wheel of incarnation that Darwin went through on the road
| to XNU, although I'm not sure Tevanian ever stated his
| perspectives on this matter publicly. Neither of these
| systems were ever true monolithic kernels in the Linux or
| Unix sense--at all times they both had some measure of
| sandboxing between e.g. driver code and the scheduler--
| rather sitting somewhere between.
|
| True microkernels are, alas, more of an ideology than a
| practical reality, as the long-suffering GNU/HURD team
| discovered; Tanenbaum has been clear that the MINIX/NetBSD
| experiment was more about principles than performance. That
| said, certainly many hypervisors have attained success with
| configurations that coincidentally happen to be the same
| footprint as a microkernel.
| vacuity wrote:
| The hypervisor/microkernel boundary has blurred, and
| commercial success for microkernels is more or less as
| hypervisors, e.g. OKL4 is widely used in mobile
| devices[0]. And Tanenbaum's Minix is used for the Intel
| Management Engine. I don't know the details with HURD,
| but I don't think it is mainly suffering from "inherent"
| or "nearly-inherent" (strongly associated) problems of
| microkernels. The main cost of microkernels is developer
| effort and likely performance overhead.
|
| [0] https://vita.militaryembedded.com/5159-open-
| virtualization-a...
| ryao wrote:
| NT and XNU never had microkernel origins - Cutler
| explicitly refuted this at a conference in the early 1990s
|
| Interestingly, the Tanenbaum-Torvalds debate had Tanenbaum
| claim otherwise at the very start: The
| alternative is a microkernel-based system, in which most of
| the OS runs as separate processes, mostly outside the
| kernel. They communicate by message passing. The kernel's
| job is to handle the message passing, interrupt handling,
| low-level process management, and possibly the I/O.
| Examples of this design are the RC4000, Amoeba, Chorus,
| Mach, and the not-yet-released Windows/NT.
|
| https://groups.google.com/g/comp.os.minix/c/wlhw16QWltI
|
| That is why I thought Windows NT had originally been
| intended to be a microkernel.
| vacuity wrote:
| I will caution that IPC microbenchmarks should not be taken as
| confirmation that the "academic microkernel" is viable: OS
| services all in userspace and with fine granularity as is
| appropriate. Often microkernel-like designs like
| VMMs/hypervisors and exokernels make use of unikernels/library
| OSes on top, which reduces the burden of fast IPC somewhat. Or
| developers intentionally lump protection domains to reduce IPC
| burden. Of particular note: even seL4 did not evict its
| scheduler to userspace. Since the scheduler is the basis behind
| time management, it's quite a blow to performance if the
| scheduler eats up time constantly. My own thoughts there are
| that, with care, a userspace scheduler can efficiently
| communicate with the kernel with a shared memory scheme, but
| that is not ideal. But for desktop and mobile, a microkernel
| design would be delightful and the performance impact is
| negligible. We need far more investment on QoS there.
|
| Edit: That being said, we should be building microkernel-based
| OSes, and if for some cases performance really is a restricting
| factor, they will be exceptions. The security, robustness,
| flexibility, etc. of microkernels is not to be understated.
| indolering wrote:
| They verified that the scheduler doesn't interfere with
| integrity, confidentiality, and authenticity requirements of
| the kernel so it's a moot point.
| vacuity wrote:
| Rather, although I believe the seL4 scheduler is
| sufficiently general, I want a userspace scheduler to
| minimize policy. The seL4 team recognizes that a
| kernelspace scheduler violates Liedtke's minimality
| principle for microkernels, since the only motivating
| reason is performance. If an efficient userspace scheduler
| implementation exists, the minimality principle dictates no
| kernelspace scheduler. Otherwise there's pointless
| performance overhead and possibly policy inflexibility.
| netbsdusers wrote:
| Drivers in userspace is not particularly microkernelly - most
| of the major monolithic kernels have supported this to some
| degree or another for years (it is easy in principle, just
| transmit I/O requests to userspace servers over some channel)
| while many historic microkernels (see e.g. Mach 3) did not do
| it. It hardly changes the architecture of the system at all.
|
| It is moving the higher-level things into userland that is the
| harder problem, and the one that has been challenging for
| microkernels to do well.
| vacuity wrote:
| People should stop bringing up Mach so much. It should never
| have been the poster child for microkernels. It's poisoned
| the discourse when there are plenty of alternative examples.
| Granted, Mach also did some good work in the space, but its
| shortcomings are emphasized as if they reflect the whole
| field.
|
| More to the point, drivers in userspace is an important
| distinction between "pure" monolithic kernels and
| microkernels: the former is optimizing for performance and
| the latter is optimizing for robustness. It's not about ease
| of implementation for either. It's quite meaningful to shift
| on the axis nowadays: it represents a critical pragmatic
| decision (notice purity is irrelevant). You're right that
| "higher-level things" such as the networking stack or
| filesystem are also crucial to the discussion. I think here,
| too, ease of implementation is not relevant, though.
| torginus wrote:
| Isn't it common to run OSes on desktop/server environment
| inside hypervisors? That means the OS itself can be
| transparently virtualized or preempted, and access to
| physical hardware can be transparently passed to the
| virtualized OSes. This can be accomplished today with minimal
| impact to performance on user experience.
|
| The fact that this can be done with OS code not explicitly
| designed for this signals to me that there are no roadblocks
| to having a high-performing general purpose microkernel
| running our computers.
| vacuity wrote:
| This leads to big units of code, namely multiple OSes,
| whereas the ideal is being able to use as finely granular
| units as developers are able to stomach. For example, Xen
| can work around the issue of device drivers by hosting a
| minimal OS instance that has drivers, but it is better to
| be able to run drivers as individual processes. This
| reduces code duplication and performance overhead.
| phendrenad2 wrote:
| Yes and there's a very good reason: Linux is safe enough, more
| efficient, and more scalable.
| vacuity wrote:
| I suppose I should ask the other side too, though I am biased
| to favor microkernels, and am better read on them, but how
| so?
|
| "Safe enough" measured by the standards of this upside-down
| industry...I'll let everyone decide that for themselves.
|
| "More efficient": while monolithic kernels have a higher
| ceiling, currently there's plenty of OS research papers and
| industry work demonstrating that more integration with
| userspace brings performance benefits, such as in the
| scheduler, storage, or memory management. Microkernels
| encourage/enforce userspace integration.
|
| "More scalable": I think this has less to do with kernelspace
| scale and more with how nodes are connected. See
| Barrelfish[0] for eschewing shared memory in favor of message
| passing entirely, running separate kernels on each core.
| Meanwhile Linux has gradually discovered a "big lock"
| approach is not scalable and reduced coarse-grained locks,
| added RCU, etc.. So I think we will go moreso towards
| Barrelfish. But on a single core, for what goes into the
| kernel, that's covered by everything but scalability.
|
| [0] https://people.inf.ethz.ch/troscoe/pubs/sosp09-barrelfish
| .pd...
| sparkie wrote:
| To the best of my knowledge, seL4 is not AVX-512 aware. The
| AVX-512 state is not saved or restored on a context switch,
| which is clearly going to impact efficiency.
|
| At present there's 16x64-bits of register state saved (128B),
| but if we were to have full support for the vectors, you need
| to potentially add 32x512-bits to the state (plus another 16 GP
| registers when APX arrives). Total state that needs moving from
| registers to memory/cache would jump to 2304B - a 1800%
| increase.
|
| Give that memory is still the bottleneck, and cache is of
| limited size, a full context switch is going to have a big hit
| - and the main issue with microkernels is that a service you
| want to communicate with lives in another thread and address
| space. You have: app->kernel->service->kernel->app for a round-
| trip. If both app and service use the AVX-512 registers then
| you're going to have to save/restore more than half a page of
| CPU state up to 4 times, compared with up to 2 on the
| monolithic kernel which just does app->kernel->app.
|
| The amount of CPU state only seems to be growing, and
| microkernels pay twice the cost.
| nickpsecurity wrote:
| High-assurance security requires kernels clear or overwrite
| all shared state. That could become a covert, storage channel
| if one partition can write it and another read it. If so, it
| should be overwritten.
| Veserv wrote:
| The cost of moving 4 KB is miniscule. Assume a anemic basic
| desktop with a 2 GHz clock and 2 instructions per clock. You
| would be able to issue 4 billion 8-byte stores per second
| resulting 32 GB/s or 32 bytes per nanosecond. Memory
| bandwidth is going to be on the order of 40-60 GB/s for a
| basic desktop, so you will not run into memory bandwidth
| bottlenecks with the aforementioned instruction sequence. So,
| 4 KB of extra stores is a grand total of 128 additional
| nanoseconds.
|
| In comparison, the average context switch time of Linux is
| already on the order of ~1,000 nanoseconds [1]. We can also
| see additional confirmation of the store overhead I computed
| as that page measures ~3 us for a 64 KB memcpy (load + store)
| which would be ~187 nanoseconds for 4 KB (load + store) where
| as the context saving operation is a 2 KB register -> store
| and a 2 KB load -> register.
|
| So, your system call overhead only increases by 10 percentage
| points. Assuming you have a reasonably designed system that
| does not kill itself with system call overhead, spending the
| majority of the time actually handling the service request,
| then it constitutes a miniscule performance cost. For
| example, if you spend 90% of the time executing the service
| code, with only 10% in the actual overhead, then you only
| incur a 1% performance hit.
|
| [1] https://eli.thegreenplace.net/2018/measuring-context-
| switchi...
| arakageeta wrote:
| I'm not sure that seL4 even supports NUMA, so there are other
| tradeoffs to consider.
| vacuity wrote:
| I think NUMA management is high level enough that in a
| microkernel it would be comfortably managed in userspace,
| unlike things relevant to performance-critical context
| switches. And seL4 is currently intended only for
| individual cores anyways.
| mmooss wrote:
| SeL4 is old news - not a criticism, but has anyone added another
| formally proven layer or component? (Edit: I mean new components
| beyond the microkernel, not improvements to the microkernel.)
|
| Also, I suspect some people - maybe some on HN :) - get emotional
| overload when they see the word 'proof' and their intellectual
| functions stop. It's not a panacea for the infinite problem of
| secure IT; it isn't a way to create or discover a perfect and
| flawless diamond of software. IIUC it means it's proven to meet
| specific requirements in specific conditions, and those
| requirements and conditions can be quite narrow; and it says
| nothing about other functions and conditions that are out of
| spec. Is that roughly correct?
|
| What does it mean in practical terms? What does a security
| professional see when they see 'formally proven software'?
|
| What are the specs that SeL4 meet (no, I haven't looked at the OP
| in a long time)? Isn't that the essential information here?
| saithound wrote:
| Has anyone added another formally proven layer or component?
| Yes, they're being added all the time. Recently added features:
|
| - Support for a bunch of new architectures, including RISC-V. -
| Mixed criticality scheduling, which provides capability-based
| access to CPU time, mechanisms to limit the upper bound of
| execution of a thread, ensuring that high-criticality tasks
| have priority and access to necessary resources, and allowing
| "passive servers" which run on scheduling time donated by the
| caller. - Microkit, a new verified abstraction layer which made
| it much much easier to build actual systems using seL4. - Very
| recently, the Device Driver Framework, a device-driver
| template, control and data plane implementation, and tools for
| writing device drivers and providing device virtualisation for
| high-performance I/O on seL4.
|
| Formal verification can guarantee that specific requirements
| hold in specific conditions. It's true that in general such
| requirements and conditions can be quite narrow. But seL4
| itself has a whole lot of proofs about it, covering a wide
| range of properties that one would want in a kernel, and these
| guarantees hold under very weak assumptions. Even the
| correctness of the C compiler is not assumed, they have a
| separate tool which looks at the compiler output and proves
| that the compiled binary behaves correctly with respect to the
| required C semantics.
|
| The requirements that seL4 meets include the following: the
| binary code of the seL4 kernel correctly implements the
| behaviour described in the abstract specification and nothing
| more. There are no buffer overflows, no memory leaks, no
| pointer errors or null pointer dereferences, no undefined
| behavior in the C code, no termination of the kernel apart from
| the explicit ways enumerated in the spec, etc. The
| specification and therefore the seL4 binary satisfy the
| security properties of integrity and confidentiality: the
| former means that there is absolutely no way for a process to
| change data that the process has no explicit permission to
| change, and the latter means that a process cannot, in any way,
| read data it has no explicit permission to read. It even shows
| that a process without permission cannot indirectly infer the
| data through certain side channels. Beyond security, the
| expected worst-case execution-time guarantees and scheduling
| properties are also met.
| dloss wrote:
| For example: No buffer overflows, null pointer exceptions, use-
| after-free, etc. On ARM and RISCV64 not even the C compiler has
| to be trusted, because functional correctness has been proven
| for the binary. And there are more proofs besides functional
| correctness.
| https://docs.sel4.systems/projects/sel4/frequently-asked-que...
| im_down_w_otp wrote:
| https://github.com/auxoncorp/ferros
|
| Lots of type-level programming for tracking resources, hardware
| access, and capabilities at compile-time and trying to bring
| some of the underlying kernel guarantees up to the compiler
| because finding out about and debugging issues at runtime was
| just the absolute worst.
| snvzz wrote:
| The document was updated in January.
|
| A lot has happened in the last few years, such as the founding
| of seL4 foundation, the maturation of mixed criticality
| scheduling, the celebration of multiple seL4 summits, and the
| deployment in practical use by multiple companies and
| countries, in several scenarios.
| ryao wrote:
| Being "formally proven" to be free of various flaws did not
| make seL4 immune to memory corruption flaws. Despite the formal
| proof, a memory corruption flaw was found a few years ago. The
| PRs for the commits fixing it and amending seL4's proof are
| public:
|
| https://github.com/seL4/seL4/pull/243
|
| https://github.com/seL4/l4v/pull/453
|
| You will find a number of other memory related bugs in its
| issue tracker:
|
| https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
|
| Interestingly, the PR fixing "register clobbering" in memory
| was not labelled bug, so it is not listed when you filter by
| "bug".
|
| I used to think seL4 was immune to these issues given its proof
| allegedly saying it is, but upon seeing this, I have come to
| think that the proof is not as comprehensive as the wider
| community has been lead to believe. That said, seL4 is still a
| very impressive piece of software.
|
| Finally, to answer your question. The specification that seL4
| meets is published on github:
|
| https://github.com/seL4/l4v
| isubasinghe wrote:
| I believe only certain versions and on certain architectures
| is seL4 verified for. There are no bugs found at the C source
| code level for these builds of seL4.
| vacuity wrote:
| Even if it's not exactly seL4, there's good value in taking
| inspiration for design elements. It would still be a lot
| more robust than commodity operating systems.
| hannob wrote:
| L4 was popular at my university (Karlsruhe). While I never really
| looked into it in any detail, it always appeared to me like a
| project that is primarily interested in testing some theoretical
| ideas, but not in building anything that would be practically
| useful.
|
| That was 20 years ago. As far as I can tell, this has not
| changed. (Quick googling tells me there appear to be some efforts
| to build an OS on it, but they all look more like proof of
| concepts, not like something with real-world use.)
| yjftsjthsd-h wrote:
| https://en.wikipedia.org/wiki/L4_microkernel_family seems to
| describe it having been used all over the place, though mostly
| in embedded contexts.
|
| > OKL4 shipments exceeded 1.5 billion in early 2012,[4] mostly
| on Qualcomm wireless modem chips. Other deployments include
| automotive infotainment systems.[13]
|
| > Apple A series processors beginning with the A7 contain a
| Secure Enclave coprocessor running an L4 operating system[14]
| called sepOS (Secure Enclave Processor OS) based on the
| L4-embedded kernel developed at NICTA in 2006.[15] As a result,
| L4 ships on all modern Apple devices including Macs with Apple
| silicon.
| ryao wrote:
| I feel like the two of you are talking past each other as the
| other poster is talking about time sharing systems like UNIX
| while you are pointing at embedded applications that are OS
| optional and if there is any semblance of an OS, it is really
| minimal. People deploying L4 there is not very surprising and
| does not apply to his remarks. Seeing this is like watching
| one person discuss an absence of apples and seeing another
| reply saying that there are oranges.
| hannob wrote:
| Ok, admittedly, that's more than I expected. And hey, if they
| found some use cases in the embedded world, fine.
|
| Nevertheless, it's not exactly how it was pitched. This
| Microkernel thing always had a "Linux is doing it wrong,
| we're doing it better" story behind it. They wanted to be a
| replacement for a general-purpose OS. That cetainly hasn't
| happened.
| ryao wrote:
| OSF/1 is the closest that microkernels ever came to being
| used in general purpose operating systems:
|
| https://en.wikipedia.org/wiki/OSF/1
|
| The only still living variant is AIX. Some of the code is
| in the XNU kernel, although that is a monolithic kernel
| rather than a microkernel. Apple converted it to a
| monolithic design for performance reasons.
|
| That said, this article suggests that AIX is not using a
| microkernel either:
|
| https://tedium.co/2019/02/28/ibm-workplace-os-taligent-
| histo...
| dloss wrote:
| Well, an L4 variant is used in iPhones: "The Secure Enclave
| Processor runs an Apple-customized version of the L4
| microkernel." https://support.apple.com/de-
| at/guide/security/sec59b0b31ff/...
| nabla9 wrote:
| L4, L4Ka developed in Karlsruhe is not the same as seL4.
| xxmarkuski wrote:
| Jochen Liedtke became a professor in 1999 in Karlsruhe, sadly
| he passed away only shortly after in 2001. I don't know if his
| successor Bellosa still does research on L4. There was the L4Ka
| project which appears to be completed. In the bachelor lecture
| on OS by him it's not part of the curriculum.
|
| Rittinghaus, alumni of Bellosa, is involved with Unikraft [0],
| which was featured a couple of times on hn, and is using
| unikernel technology.
|
| [0] https://unikraft.org/
| senko wrote:
| I love the work (and the direction) the Karlsruhe team did on
| L4Ka, especially with Pistachio - the design was clean, simple,
| easy to grasp.
|
| I did a Pistachio-based OS for my diploma thesis (not at
| Karlsruhe). I always thought that if I'd been studying there,
| I'd probably go into OS research.
| TheAmazingRace wrote:
| I gave a presentation on SeL4 for my local OWASP chapter. I'll
| have to see if I can dig it up.
|
| The project truly is a nice piece of kit, but I would hesitate to
| consider it as a replacement for Linux, especially for general
| purpose computing. Though that isn't to say microkernels are
| terrible for it in general. RedoxOS seems to be making some
| inroads lately and it uses a microkernel written in Rust.
| vacuity wrote:
| The question is always "how big of a replacement are we
| talking?" Redox seems to be committed to interoperate well with
| POSIX, which naturally informs its design decisions. And
| there's a huge difference between having technical capabilities
| and succeeding. Although if Redox does succeed, it would
| already be a good step. seL4 is even more extreme in these
| qualities: its technical advantages are superb, but so far (and
| I think this will continue) it does not have what it takes,
| whatever that encompasses, to be the Next Big Thing. Ignoring
| political considerations, I think microkernels will be
| successful, and rightfully so.
| alphazard wrote:
| Also worth checking out Drew DeVault's Helios Microkernel, which
| is based on SeL4.
|
| https://ares-os.org/docs/helios/
| kevinherron wrote:
| I think there's a meaningful difference between "based on" and
| "inspired by", Helios being the latter.
| HeavyRain266 wrote:
| I'm a fan of microkernel hosts for guest monoliths, thus our
| servers are running seL4 as safety layer and backups for FreeBSD
| VMs with jails for renderfarm, BEAM clusters and Jenkins.
|
| All I'm missing is an ARM port of DragonflyBSD for its threading
| and in-process kernels (hybrid kernel design). My dream is to run
| it on 128 cores Ampere Altra to run OpenMoonRay more effectively.
| russellbeattie wrote:
| I think at this point the argument for or against microkernels is
| becoming moot. The only way to provide fast, efficient and safe
| access to privileged services is via hardware mitigations.
| Software can only do so much.
|
| It's like the difference between a 80286 and a 80386: The latter
| added the hardware support for true multitasking that the former
| lacked. Since then there's been an ever increasing number of
| hardware-level protection mechanisms added, like those which
| enabled hypervisors.
|
| Apple in particular has been adding a bunch of stuff to their
| SOCs to protect the kernel, drivers and components at the chip
| level, as well as enforce privileges on running threads and when
| using pointers. [1] This doesn't mean the OS is impenetrable, but
| it's a lot more effective than a software only strategy of
| managing privileges.
|
| Seems to me that utilizing this stuff (or similar), the
| architecture of the kernel really isn't that important any more.
|
| Am I off base?
|
| 1. https://support.apple.com/guide/security/operating-system-
| in...
| vacuity wrote:
| That doesn't seem right. Even with strong hardware protections,
| how is Linux's TCB comparable to a microkernel? Unless it just
| recreates the exact same protection domains, there will be more
| vulnerability in Linux. Rather, the thing about hardware is
| primarily that it makes things more efficient. For example,
| microkernels nowadays are already quite robust because they
| make good use of certain hardware: the MMU. Then the small TCB
| of a microkernel gives the kernel credibiity, so the kernel and
| hardware together make for a solid infrastructure. So really
| it's a matter of how much "cheating" we're allowed to do with
| hardware, but microkernels overall utilize the protection
| better. Or see exokernels.
___________________________________________________________________
(page generated 2025-03-23 23:00 UTC)