3 ms·
An active, long-running project, more than 20 years now, Genode is amazing outright. They actually managed to make a general-purpose OS (Sculpt) with an archit
by snvzz 9mo ago
An active, long-running project, more than 20 years now, Genode is amazing outright.
They actually managed to make a general-purpose OS (Sculpt) with an architecture centered around capabilities, and they can run such a system with seL4 as the microkernel, which guarantees capabilities cannot be forged.
- rurban 9mo agoThey can use most L4-based microkernels, mostly their own, or NOVA or Fiasco. Secure capabilities are a feature of all L4 kernels.
- snvzz 9mo ago>They can use most L4-based microkernels, mostly their own, or NOVA or Fiasco. Correct, Genode supports several kernels, including but not limited to those. >Secure capabilities are a feature of all L4 kernels. Not accurate. Liedtke's L4 does not do capabilities. It would be more accurate to say that most modern L4-like kernels do. The highlight is seL4, specifically because it offers those formal guarantees while also being the fastest.
- rurban 9mo agoWho cares about formal guarantees when the other kernels are much better and provide a much better infrastructure. The kernel itself is minimal. Fiasco can be real-time.
- snvzz 9mo ago>Who cares about formal guarantees Projection. You might not care, but extrapolating is a mistake. Public as well as private sector with high assurance needs have gathered around seL4 foundation due to its proofs and technical excellence. >are much better Subjective. What is your criteria? >Fiasco can be real-time. Depends on your definition of real-time. Hard realtime requires guarantees that the deadlines will always be met. The only non-toy kernel that offers proof of WCET is seL4. If soft realtime is all you need, then Linux with PREEMPT_RT suffices.