seL4和紫红色的内核在概念上有什么区别?

Fuchsia是一个基于功能的操作系统,它建立在Google的锆石微内核之上,而锆石微内核本身就是基于 little kernel .

比较起来更有意义 Zircon 到seL4,或类似的操作系统框架 Genode (在seL4上运行)到紫红色。我将简单比较seL4和锆石。

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

例如,虽然seL4提供了构建流程抽象的机制,但它根本没有定义流程。相对而言,锆石在微内核中内置了很多策略,包括过程。当为特定平台配置时,seL4有许多属性(功能正确性、完整性、隔离性)的证明,而zron没有。