microkernel - seL4 和 Fuchsia 的内核在概念上有什么区别？

Question

最初我认为 Fuchsia 是第一个广泛使用基于能力的安全性的内核，但看起来在 seL4 中它们也是主要的安全原语。

Answer 1

Fuchsia 是建立在 Google 的 Zircon 微内核之上的基于能力的操作系统，它本身就是基于little kernel的。

将Zircon与 seL4 或像Genode（在 seL4 上运行）这样的操作系统框架与Fuchsia进行比较更有意义。我将简要比较 seL4 和 Zircon。

seL4 提供最少的机制，专为高保证系统而设计。锆石提供了很多政策，并不是为高保证而设计的，重点是实用性。我相信两者都以高性能为目标。简而言之，与 Zircon 相比，seL4 是一个非常小的微内核。

例如，虽然 seL4 提供了构建流程抽象的机制，但它根本没有定义流程。相比之下，Zircon 在微内核本身中内置了很多策略，包括进程。seL4 在为特定平台配置时具有许多属性（功能正确性、完整性、隔离性）的证明，而 Zircon 没有。