6 ms·

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

• pjmlp 2y ago
  I feel like containers and Kubernetes are microkernels revenge. They are for all practical purposes fulfilling the same role.
  • bri3d 2y ago
    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 2y ago
      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 2y ago
        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 2y ago
          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 2y ago
            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-kubernetes-container-escape-using-linux-kernel-exploit/ 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.
            • indolering 2y ago
              I don't think containers, namespaces, and the like failing to provide the same benefits of a true microkernel negate the OPs point. They are ways of segmenting userspace in a more finely grained manner and they do make attacks harder. Linux security being a shit show and undermining these efforts is kinda besides the point: they are still attempts provide a runtime closer to what microkernels would naturally provide in a backwards compatible way. Indeed, these containers could be turned into fully fleged VMs if there were the resources to make it happen.
              • bri3d 2y ago
                I don't really get this argument: "you're saying that one thing, namespaces, isn't implemented in any way resembling a microkernel, but what if we replaced it with another completely different thing, a hypervisor? Then it would be similar!" Yes? Sure? To me the word "microkernel" expresses how the kernel is structured, not what userspace interface it presents. A microkernel is built by separating kernel services into discrete processes which communicate using a defined IPC mechanism. Ideally, a microkernel offers memory boundary guarantees for each service, either by using hardware memory protection/MMU and running each service as a true "process" with its own address space, or by proving the memory safety of each kernel service using some form of ahead-of-time guarantee. Of course, doing this lends itself to also segmenting user-space processes by offering a unique set of kernel service processes for each user-space segment (jail, namespace, etc.), but there's no reason this needs to be the case, and it's by and large orthogonal. I do agree with what I eventually understand the grandparent poster was trying to express, which is that running a bunch of KVMs looks like a microkernel. Because then, you've moved the kernel services into a protected boundary and made them communicate across a common interface (hypercalls). But that's not how Kubernetes works by default and in the case of containers and namespaces, I think this is entirely false and a dangerous thing to believe from a security standpoint. > They are ways of segmenting userspace in a more finely grained manner and they do make attacks harder. From a _kernel_ security standpoint (because we are talking about micro_kernels_ here), I actually think namespaces make attacks much easier and the surface area much greater. Which is basically the entire point I was trying to make: rather than exposing fragile kernel interfaces to exclusively system services with CAP_SYS_ADMIN, you now have provided an ability (unshare) for less-trusted runtimes to touch parts of the host kernel (firewall, filesystem drivers, etc.) which they would normally not have access to, and you have to go back and use fiddly rules engines (seccomp, apparmor, selinux) to fix the problem you created with namespaces. To be clear, I think from a big picture standpoint, it's a tradeoff, and I'm nowhere near as anti-container/anti-namespace as it may seem. I just get annoyed when I see people express namespaces as a kernel security boundary when they are basically the exact opposite: they are a kernel security un-boundary, and Linux's monolithic nature makes this a problem.
        • afiori 2y ago
          Imo the microness is not about size but about the architecture of running drivers/services in fault-resistant separation from the kernel
      • vacuity 2y ago
        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 2y ago
          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 2y ago
  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 2y ago
    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-operating-system/ https://www.zdnet.com/article/minix-intels-hidden-in-chip-op... [2] https://www.cs.vu.nl/~ast/intel/ https://www.cs.vu.nl/~ast/intel/
    • indolering 2y ago
      Such a dumb technical choice driven by stupid managerial considerations. They do this ring -1 shit because hardware companies view this as a cheap way to add value. But they don't open source it or contribute back because they view it as secret sauce. Minix as a result didn't get the investments that GPL software receives. Now the project is in hard legacy mode.
  • mrkeen 2y ago
    That is Minix, not SeL4.
  • ianburrell 2y ago
    Intel Management Engine is a separate microcontroller integrated into the chipsets. Recent ones are Intel Quark x86 CPU and Minix 3 OS.
  • naasking 2y ago
    seL4 is used in a lot of cellular phone firmwares I believe.
• ryao 2y ago
  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 2y ago
    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 2y ago
      Nice use of Latin. mihi placet.
    • nine_k 2y ago
      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 2y ago
        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 2y ago
          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?
• vacuity 2y ago
  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 2y ago
    They verified that the scheduler doesn't interfere with the integrity, confidentiality, and authenticity requirements of the kernel so it's a moot point.
    • vacuity 2y ago
      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.
      • indolering 2y ago
        I understand the minimality principle but one should not be afraid to violate layers of abstraction when justified. The whole point of the minimality principle is to improve modularity and remove the need to worry about the correctness of various OS components. What would you be able to do in a userspace scheduler that couldn't be done safely in an in-kernel scheduler? Why couldn't it be configured or given a safe API to interact with userspace at runtime? But I guess your shared memory bit is an API to a userspace scheduler?
• netbsdusers 2y ago
  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 2y ago
    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 2y ago
    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 2y ago
      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 2y ago
  Yes and there's a very good reason: Linux is safe enough, more efficient, and more scalable.
  • vacuity 2y ago
    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.pdf https://people.inf.ethz.ch/troscoe/pubs/sosp09-barrelfish.pd...
  • naasking 2y ago
    "Safe enough" means "actually unsafe".
    • phendrenad2 2y ago
      Yes, and bank vaults have doors.
• sparkie 2y ago
  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 2y ago
    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.
    • deleted 2y ago
      [deleted]
  • Veserv 2y ago
    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-switching-and-memory-overheads-for-linux-threads/ https://eli.thegreenplace.net/2018/measuring-context-switchi...
• deleted 2y ago
  [deleted]