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

【问题标题】：What is a conceptual difference between seL4 and Fuchsia's kernel?seL4 和 Fuchsia 的内核在概念上有什么区别？
【发布时间】：2019-02-25 10:00:34
【问题描述】：

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

【问题讨论】：

有 1500+ 声望的人可以创建一个标签“seL4”，所以可以在这里添加吗？似乎在 seL4 特定的 Q/A 站点中有一些针对堆栈溢出的工作：area51.stackexchange.com/proposals/120611/sel4
你能澄清一下这个问题吗？你想知道第一个基于能力的内核吗？还是 Fuchsia 和 seL4 的区别？
@AnnaLyons 后者，但前提是它们是概念与实现细节。
@Lost 好的，我已经根据这个回答了。很高兴回答任何后续问题！
创建标签sel4

【解决方案1】：

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

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

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

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

【讨论】：