11 ms·

The SeL4 Microkernel: An Introduction [pdf]

264 points by snvzz 2y ago

coldblues 2y ago
https://genode.org/index https://genode.org/index An operating system with seL4 support
- Rochus 2y ago
  Are there notable uses of Genode?
hackpelican 2y ago
Does the OS that lies on top of this kernel need to be formally verified as well for the security guarantees to hold?
- Koshkin 2y ago
  In absolute terms, sure. At the practical level, you can find a partial answer in the section 7.2 of the paper.
- snvzz 2y ago
  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 2y ago
    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 2y ago
      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_11_fence.t_hardware_support_for_preventing_microarchitectural_timing_channels_Nils_Wistoff.pdf https://sel4.systems//Foundation/Summit/2022/slides/d1_11_fe... 1. https://lf-riscv.atlassian.net/browse/RVS-3569 https://lf-riscv.atlassian.net/browse/RVS-3569
- rubenbe 2y ago
  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 2y ago
  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 2y ago
    An IOMMU can help significantly with the driver problem, preventing a properly initialized driver from misbehaving and compromising the system.
    - vacuity 2y ago
      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 2y ago
        >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 2y ago
        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.
        surajrmal 2y ago
        The primary roadblock is cost and complexity. The technology itself is sound and doesn't have major performance problems.
nimish 2y ago
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 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.
mmooss 2y ago
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 2y ago
  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.
hannob 2y ago
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 2y ago
  https://en.wikipedia.org/wiki/L4_microkernel_family 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 2y ago
    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 2y ago
    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.
TheAmazingRace 2y ago
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 2y ago
  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.
- snvzz 2y ago
  >I would hesitate to consider it as a replacement for Linux It would depend on the scenario. Of course, Linux is easier to work with but OTOH there are requirements which only seL4 can satisfy. There's a lot required on top of seL4 for it to be actually useful. Fortunately, there has been a lot of Open Source work there as well. This is where seL4 is in a much better position than just a few years ago. For static scenarios, there's LionsOS[0], quite usable already. For dynamic scenarios, there's the Provably Secure, General-Purpose Operating System[1], which is still early stages. Both can be found in the Projects page[2] at trustworthy systems, which is linked in the seL4 website. 0. https://trustworthy.systems/projects/LionsOS/ https://trustworthy.systems/projects/LionsOS/ 1. https://trustworthy.systems/projects/smos/ https://trustworthy.systems/projects/smos/ 2. https://trustworthy.systems/projects/ https://trustworthy.systems/projects/
  - TheAmazingRace 2y ago
    Thank you kindly for providing these links. I do hope that microkernels take off in a big way for general purpose computing someday.
alphazard 2y ago
Also worth checking out Drew DeVault's Helios Microkernel, which is based on SeL4. https://ares-os.org/docs/helios/ https://ares-os.org/docs/helios/
- kevinherron 2y ago
  I think there's a meaningful difference between "based on" and "inspired by", Helios being the latter.
HeavyRain266 2y ago
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.
- nickpsecurity 2y ago
  Could you elaborate on how your servers use seL4? And are these production, commercial servers?
  - HeavyRain266 2y ago
    Yes, commercial production servers. Similar to some other systems and certain consoles, microkernel is used as hypervisor that protect bare metal hardware from potential hazards when guest monoliths like mentioned FreeBSD becomes compromised. Guest components are running our software and services inside jails on two 128 core, two 64 core and one 32 core Ampere processors where first two machines run heavy workloads like offline rendering and Erlang VM clusters, while others are used to provide a few VPS servers, and internal services.
    - nickpsecurity 2y ago
      Thanks. That's similar to prior uses. Makes sense. I think some readers next question might be: are you all hiring?
      - HeavyRain266 2y ago
        We're not hiring at the moment.
        nickpsecurity 2y ago
        Thank you anyway.
russellbeattie 2y ago
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-integrity-sec8b776536b/web https://support.apple.com/guide/security/operating-system-in...
- vacuity 2y ago
  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.
- MisterTea 2y ago
  > Am I off base? Yes. There is still plenty of work to be done in the OS research space. There has to be software interfaces and API's to all this new hardware. I also think there is a lot to be learned from using micro/hybrid systems which are much more composable. e.g. Plan 9 is a great example of a hybrid system which makes use of a singular protocol, 9P, to serve all objects in the system to userspace. It is hybrid because some parts are in-kernel to avoid the overhead of system calls such as IP, and TLS. Another interesting design aspect is how the in-kernel drivers are minimal mostly acting as a 9P interface to the hardware logic. This way you A. turn a machine object like a pointer or record into a seekable file and B. secured that file using standard unix permissions and C. can easily distribute the components across machines via a network. Now you can securely push the driver logic into a userspace program. And 9p is network and architecture transparent meaning you can work across multiple machines running on Arm, x86, mips, etc. All this come out of the box. When I go back to Linux/Unix or Windows from Plan 9 its a sad and frustrating time. They're about as flexible as igneous rock. All the features are ad-hoc bolted on in mutually incompatible ways using a myriad of protocols that all do the same thing - serve files/objects. Ugh.
zzo38computer 2y ago
I also had ideas of an operating system design and the capabilities I had considered uses the same features of interposition and delegation as seL4 does. There are other advantages than just what they list there; for example, you can apply a filter to audio, or you can use proxy capabilities for implementing network transparency. The real-time stuff is something I had considered as allowing as an optional implementation; my idea was for a specification rather than only a single implementation. Another feature I wanted though, is that all programs operate deterministic except for I/O. Without I/O, you can't determine the date/time or how long a program takes, can't check for processor features (if you use something that the hardware does not support though, the operating system may emulate it), etc. I had thought to use a mixture of hardware support and software support to implement it, though. (There is a note in the document about attacks with capability implemented in hardware, but I do not have the referenced document and I don't know if that attack applies to what I am thinking of doing.)
aurelien 2y ago
The point about security is that it seems to present the same failure as kvm is for Linux kernel. If the hypervisor is in the ring 0 you have the risk of VM escape from one to another or the host itself. How do you mitigate that risk?
- snvzz 2y ago
  In seL4's virtualization support, VM exceptions are turned into messages and handled by VMM, a task running in unprivileged mode. VMM has no more capabilities than the VM itself, thus a VM escape would be, outside of academics, of no value. Refer to pages 8 to 10 in the OP PDF.
curtisszmania 2y ago
[dead]

264 points by snvzz 2y ago

coldblues 2y ago

https://genode.org/index https://genode.org/index An operating system with seL4 support

Rochus 2y ago
Are there notable uses of Genode?

hackpelican 2y ago

Does the OS that lies on top of this kernel need to be formally verified as well for the security guarantees to hold?

Koshkin 2y ago
In absolute terms, sure. At the practical level, you can find a partial answer in the section 7.2 of the paper.
snvzz 2y ago
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 2y ago
  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 2y ago
    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_11_fence.t_hardware_support_for_preventing_microarchitectural_timing_channels_Nils_Wistoff.pdf https://sel4.systems//Foundation/Summit/2022/slides/d1_11_fe... 1. https://lf-riscv.atlassian.net/browse/RVS-3569 https://lf-riscv.atlassian.net/browse/RVS-3569
rubenbe 2y ago
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 2y ago
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 2y ago
  An IOMMU can help significantly with the driver problem, preventing a properly initialized driver from misbehaving and compromising the system.
  - vacuity 2y ago
    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 2y ago
      >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 2y ago
        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.
        surajrmal 2y ago
        The primary roadblock is cost and complexity. The technology itself is sound and doesn't have major performance problems.

nimish 2y ago

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 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.

mmooss 2y ago

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 2y ago
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.

hannob 2y ago

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 2y ago
https://en.wikipedia.org/wiki/L4_microkernel_family 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 2y ago
  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 2y ago
  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.

TheAmazingRace 2y ago

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 2y ago
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.
snvzz 2y ago
>I would hesitate to consider it as a replacement for Linux It would depend on the scenario. Of course, Linux is easier to work with but OTOH there are requirements which only seL4 can satisfy. There's a lot required on top of seL4 for it to be actually useful. Fortunately, there has been a lot of Open Source work there as well. This is where seL4 is in a much better position than just a few years ago. For static scenarios, there's LionsOS[0], quite usable already. For dynamic scenarios, there's the Provably Secure, General-Purpose Operating System[1], which is still early stages. Both can be found in the Projects page[2] at trustworthy systems, which is linked in the seL4 website. 0. https://trustworthy.systems/projects/LionsOS/ https://trustworthy.systems/projects/LionsOS/ 1. https://trustworthy.systems/projects/smos/ https://trustworthy.systems/projects/smos/ 2. https://trustworthy.systems/projects/ https://trustworthy.systems/projects/
- TheAmazingRace 2y ago
  Thank you kindly for providing these links. I do hope that microkernels take off in a big way for general purpose computing someday.

alphazard 2y ago

Also worth checking out Drew DeVault's Helios Microkernel, which is based on SeL4. https://ares-os.org/docs/helios/ https://ares-os.org/docs/helios/

kevinherron 2y ago
I think there's a meaningful difference between "based on" and "inspired by", Helios being the latter.

HeavyRain266 2y ago

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.

nickpsecurity 2y ago
Could you elaborate on how your servers use seL4? And are these production, commercial servers?
- HeavyRain266 2y ago
  Yes, commercial production servers. Similar to some other systems and certain consoles, microkernel is used as hypervisor that protect bare metal hardware from potential hazards when guest monoliths like mentioned FreeBSD becomes compromised. Guest components are running our software and services inside jails on two 128 core, two 64 core and one 32 core Ampere processors where first two machines run heavy workloads like offline rendering and Erlang VM clusters, while others are used to provide a few VPS servers, and internal services.
  - nickpsecurity 2y ago
    Thanks. That's similar to prior uses. Makes sense. I think some readers next question might be: are you all hiring?
    - HeavyRain266 2y ago
      We're not hiring at the moment.
      - nickpsecurity 2y ago
        Thank you anyway.

russellbeattie 2y ago

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-integrity-sec8b776536b/web https://support.apple.com/guide/security/operating-system-in...

vacuity 2y ago
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.
MisterTea 2y ago
> Am I off base? Yes. There is still plenty of work to be done in the OS research space. There has to be software interfaces and API's to all this new hardware. I also think there is a lot to be learned from using micro/hybrid systems which are much more composable. e.g. Plan 9 is a great example of a hybrid system which makes use of a singular protocol, 9P, to serve all objects in the system to userspace. It is hybrid because some parts are in-kernel to avoid the overhead of system calls such as IP, and TLS. Another interesting design aspect is how the in-kernel drivers are minimal mostly acting as a 9P interface to the hardware logic. This way you A. turn a machine object like a pointer or record into a seekable file and B. secured that file using standard unix permissions and C. can easily distribute the components across machines via a network. Now you can securely push the driver logic into a userspace program. And 9p is network and architecture transparent meaning you can work across multiple machines running on Arm, x86, mips, etc. All this come out of the box. When I go back to Linux/Unix or Windows from Plan 9 its a sad and frustrating time. They're about as flexible as igneous rock. All the features are ad-hoc bolted on in mutually incompatible ways using a myriad of protocols that all do the same thing - serve files/objects. Ugh.

zzo38computer 2y ago

I also had ideas of an operating system design and the capabilities I had considered uses the same features of interposition and delegation as seL4 does. There are other advantages than just what they list there; for example, you can apply a filter to audio, or you can use proxy capabilities for implementing network transparency. The real-time stuff is something I had considered as allowing as an optional implementation; my idea was for a specification rather than only a single implementation. Another feature I wanted though, is that all programs operate deterministic except for I/O. Without I/O, you can't determine the date/time or how long a program takes, can't check for processor features (if you use something that the hardware does not support though, the operating system may emulate it), etc. I had thought to use a mixture of hardware support and software support to implement it, though. (There is a note in the document about attacks with capability implemented in hardware, but I do not have the referenced document and I don't know if that attack applies to what I am thinking of doing.)

aurelien 2y ago

The point about security is that it seems to present the same failure as kvm is for Linux kernel. If the hypervisor is in the ring 0 you have the risk of VM escape from one to another or the host itself. How do you mitigate that risk?

snvzz 2y ago
In seL4's virtualization support, VM exceptions are turned into messages and handled by VMM, a task running in unprivileged mode. VMM has no more capabilities than the VM itself, thus a VM escape would be, outside of academics, of no value. Refer to pages 8 to 10 in the OP PDF.

curtisszmania 2y ago

[dead]