5 ms·

Google's Fuchsia OS uses a microkernel: https://fuchsia.dev/fuchsia-src/concepts/kernel https://fuchsia.dev/fuchsia-src/concepts/kernel

junon 3y ago
Microkernels by themselves are not special; SeL4 is because it's proven to be secure.
- senko 3y ago
  SeL4 is a very interesting kernel even without taking the proof into account (eg in platforms/builds that the proof doesn't cover). I wish someone would build a beyond-posix desktop OS on top of it...
  - mycall 3y ago
    Take a look at Genode.
  - langfan 3y ago
    Why is it interesting?
    - snvzz 3y ago
      Not the parent, but seL4 has very high performance (they claim the best), and the IPC latency is bound by Worst Case Execution Time proof.
    - saithound 3y ago
      Some interesting aspects, in no particular order. Pure capability-based access control, where capabilities are communicable, but not forgeable "references with rights" to objects. While this is interesting, it's not really unique: other L4 kernels also have it, and Capsicum (but not POSIX capabilities) implements something like it on Unix. But even here, seL4 has some unique twists, such as the way IPC replies are handled, which allows policies that prevent "unsolicited" replies. A unique approach to memory management, where after boot-time, the kernel does no memory management, and even kernel memory is managed completely by user-level code. In fact, the kernel has no heap. Instead, when the user requests an operation that requires kernel memory (e.g. creating an address space, which requires memory for page tables) the user provides the memory explicitly to the kernel. This sets seL4 apart not just from monokernels, but from other L4 kernels as well. Support for passive servers: one of the most exciting recent features, these are server processes that run on scheduler time "donated" by the client. Among other things, this can be used to make sure that non-critical clients will not monopolize services needed by critical clients. IIRC seL4 is also the fastest L4 kernel for most use cases - and its worst-case execution time is bounded, at least on older CPUs which have published timing data.
    - senko 3y ago
      It's at the same time pure microkernel and performant and usable in real world (not just a research project). The memory management, scheduling and IPC are implemented in an interesting and novel way (compared to your typical mainstream OS) and allow for quite different OS design. In particular, capability-based IPC and memory management could provide a robust base for a secure OS from the ground up, instead playing whackamole in an aging POSIXish design. Sadly (tho I understand the rationale), most approaches to building a full OS on top of (L4 in general) are "run userspace Linux in an isolated container", which kind of ignores all the power underneath.
    - langfan 3y ago
      Thanks to all who replied.
- kjs3 3y ago
  It's proven correct against specification. That's not the same thing as 'secure' (although it helps).
  - hedora 3y ago
    The specification includes the semantics of the hardware it runs on, and shows security properties. Having said that, it is surprisingly easy to get hardware to violate its specifications.
    - kjs3 3y ago
      Which...is not the same thing as 'secure' (although it helps).

junon 3y ago

Microkernels by themselves are not special; SeL4 is because it's proven to be secure.

senko 3y ago
SeL4 is a very interesting kernel even without taking the proof into account (eg in platforms/builds that the proof doesn't cover). I wish someone would build a beyond-posix desktop OS on top of it...
- mycall 3y ago
  Take a look at Genode.
- langfan 3y ago
  Why is it interesting?
  - snvzz 3y ago
    Not the parent, but seL4 has very high performance (they claim the best), and the IPC latency is bound by Worst Case Execution Time proof.
  - saithound 3y ago
    Some interesting aspects, in no particular order. Pure capability-based access control, where capabilities are communicable, but not forgeable "references with rights" to objects. While this is interesting, it's not really unique: other L4 kernels also have it, and Capsicum (but not POSIX capabilities) implements something like it on Unix. But even here, seL4 has some unique twists, such as the way IPC replies are handled, which allows policies that prevent "unsolicited" replies. A unique approach to memory management, where after boot-time, the kernel does no memory management, and even kernel memory is managed completely by user-level code. In fact, the kernel has no heap. Instead, when the user requests an operation that requires kernel memory (e.g. creating an address space, which requires memory for page tables) the user provides the memory explicitly to the kernel. This sets seL4 apart not just from monokernels, but from other L4 kernels as well. Support for passive servers: one of the most exciting recent features, these are server processes that run on scheduler time "donated" by the client. Among other things, this can be used to make sure that non-critical clients will not monopolize services needed by critical clients. IIRC seL4 is also the fastest L4 kernel for most use cases - and its worst-case execution time is bounded, at least on older CPUs which have published timing data.
  - senko 3y ago
    It's at the same time pure microkernel and performant and usable in real world (not just a research project). The memory management, scheduling and IPC are implemented in an interesting and novel way (compared to your typical mainstream OS) and allow for quite different OS design. In particular, capability-based IPC and memory management could provide a robust base for a secure OS from the ground up, instead playing whackamole in an aging POSIXish design. Sadly (tho I understand the rationale), most approaches to building a full OS on top of (L4 in general) are "run userspace Linux in an isolated container", which kind of ignores all the power underneath.
  - langfan 3y ago
    Thanks to all who replied.
kjs3 3y ago
It's proven correct against specification. That's not the same thing as 'secure' (although it helps).
- hedora 3y ago
  The specification includes the semantics of the hardware it runs on, and shows security properties. Having said that, it is surprisingly easy to get hardware to violate its specifications.
  - kjs3 3y ago
    Which...is not the same thing as 'secure' (although it helps).