Frequently Asked Questions on seL4

形式化验证是近年来安全操作系统发展的热门！seL4在其官网上打出的口号就是：安全不是表现不佳的借口！

什么是seL4？

seL4是L4微内核家族中最先进的成员，值得注意的是其全面的形式验证，这使它有别于其他任何操作系统。seL4达成这个目标同时不会影响性能。

什么是微内核？

微内核是操作系统（OS）的最小核心。它呈现的是今天通常被认为的操作系统的一个很小的子集。微内核的定义由利特克给出[SOSP'95]。 因此微内核不提供如大多数现代操作系统Linux或Windows所做的那样硬件上的高层次的抽象（文件，进程，套接字等）。相反，它提供了最少的机制用于控制物理地址空间访问，中断和处理器时间。 在L4微内核使用的模式中（seL4也不例外），一旦内核启动后，一个初始的用户级的任务（根任务），被赋予完全的权限来处理所有的资源（这通常包括物理内存，x86的IO端口和中断）。由根任务来设置其他任务，并给其他任务授予权限来构建一个完整的系统。在seL4中，像其他第三代微内核一样，这样的访问权限是按能力授予的（不可伪造的令牌代表特权），并是完全可委托的。

什么是L4微内核的家族？

L4家族是非常小的，高性能的微内核。由约亨·利特克在90年代初研制出的第一个L4微内核演化而业。参见《From L3 to seL4  What Have We Learnt in 20 Years of L4 Microkernels?》，这是2013年一篇比较系统的介绍微内核发展的论文。原文下载地址：http://sigops.org/sosp/sosp13/papers/p133-elphinstone.pdf。这虽然是一篇几年前旧文，但是可读性非常强。如下所示，L4微内核的家族树图

和其他微内核相比seL4的性能如何？

尽我们所知，seL4在通常的乒乓指标方面：跨地址空间的消息传递（IPC）的操作成本，在所支持的处理器上是世界上最快的微内核，欲了解更多信息，请查看关于L4HQ的性能页面：http://l4hq.org/docs/performance.php。

但是，请注意，在L4HQ记录的 IPC时间是微优化的结果，这是尚未包括在公开的版本中。发布的内核大约慢了10-20％速度（这仍然使得它快于其他任何我们已经知道的性能数据）。我们正计划一旦他们成熟，就推动这些优化。

seL4运行在在什么硬件上？它支持哪些处理器架构？

现在seL4运行在ARMv6（ARM11），ARMv7（Cortex A8，A9，A15）和x86核上。支持的ARM平台包括飞思卡尔的i.MX31，OMAP3的BeagleBoard，Exynos Arndale 5250, Odroid-X, Odroid-XU, Inforce IFC6410 和 Freescale i.MX6 Sabre Lite。也支持所有现代的x86机器。

seL4支持什么设备？

seL4，就像任何真正的微内核一样，在用户模式下执行所有的设备驱动程序，因此设备支持不是内核的问题。唯一的例外是一个时钟驱动程序，seL4需要它执行时间片抢占，还有seL4处理的中断控制器访问。当编译内核时使能了调试的话，内核还包含了一个串口驱动程序。 除此之外，设备支持是用户的问题。seL4提供了用户模式设备驱动程序的机制，尤其是映射设备内存到驱动和将IRQ做为（异步）消息传递的能力。

DMA怎么样？

ARM平台上的seL4的形式化验证假设MMU完全控制内存，这意味着证明假设DMA是关闭的。DMA设备理论上可以覆盖机器上的任何内核，包括内核数据和代码。 你仍然可以安全地使用DMA设备，但你必须单独确保它们动作良好，也就是说，他们不覆盖内核代码或数据结构，只写到按照系统策略分配给它们的帧上。在实践中，这意味着，驱动程序和DMA硬件设备必须是可靠的。 未经验证的seL4 x86版本在实验分支上支持VT-d扩展。VT-d扩展允许内核限制DMA，从而使DMA设备能与不受信任的用户级驱动程序交互。目前，我们正在为具备SystemMMU 的A15 ARM板提供类似的验证支持。

我可以在seL4上运行Linux吗？

是的，seL4可以在虚拟机上运行Linux。目前这是仅支持x86处理器，同时seL4要求机器支持英特尔 EPT VT-X。另外目前的VMM需要支持MSI delivery 的HPET。我们正在研究基于ARM处理器上的Linux的虚拟化扩展支持（目前是A15 / A7核心），发布应该不会太久。

为了支持虚拟机，seL4本身作为一个虚拟机管理程序运行（x86 Ring-0 根模式或ARM hyp模式）和转发虚拟化事件到虚拟机监视器（VMM），VMM执行必要的仿真。VMM运行在脱特权模式（x86 Ring-3 根模式或ARM supv模式）。

seL4支持多核吗？

在x86上，seL4可以配置为支持多个CPU。目前多核的支持是通过一个多核配置实现，每个启动CPU被分配一部分可用内存。然后，内核可以通过受限的共享内存和内核支持的IPI通信。

我可以在一个没有MMU的微控制器上运行seL4吗？

在没有一个完整的存储器管理单元（MMU）上使用seL4没有什么意义，因为它的资源管理基本上是基于虚拟内存的。对于只有一个内存保护单元（MPU）或完全没有内存保护的低端处理器可言，你应该看看NICTA的eChronos实时操作系统（RTOS），这是专为这样的处理器，也经过形式化验证。

seL4是为什么应用程序服务的？

seL4是一个通用的微内核，所以答案是所有的。主要目标是有安全性或可靠性要求的嵌入式系统，但是这不是唯一的。采用像seL4的微内核就能够提供虚拟内存保护平台，并应用于需要在软件的不同部分之间隔离的应用领域。直接的应用领域是在金融，医疗，汽车，航空电子设备和国防部门。

什么是形式验证？

形式软件验证是用数学证明来说明一款软件满足特定属性。传统上，形式验证已被广泛用于说明设计或一个软件的规范都有一定的属性，或者一个设计正确地实现了一个规范。在最近几年，已经可能直接应用形式验证到实现该软件的代码上，并表明该代码具有特定的性质。形式验证有两个方式：完全自动化的方法，如有限的系统和属性的模型检验工作，以及交互的数学证明，需要手动操作。 seL4验证使用了Isabelle/HOL定理证明的形式数学证明。该定理证明是交互的，但提供的自动化程度较高。它也提供了高度的保证来确保所产生的证明是正确的。

seL4的形式验证意味着什么？

seL4的独特之处是通过形式验证来实现前所未有程度的保证。具体来说，seL4的ARM版本是第一个（也是目前唯一）带有一个完整的代码级的功能正确性证明的通用操作系统内核，这意味着一个数学证明的实现（用编写C语言）支持其规格。简言之，实现被证明是无缺陷的（见下文）。这也意味着一些其他属性，如避免缓冲区溢出，空指针异常，释放后使用等等。更进一步，有在硬件上执行的二进制代码是C代码的正确转换的相关证明。这意味着，编译器不必被信任，并且扩展了二进制的功能正确性属性。 此外，也有证明来证实seL4的规格，如果使用得当，会强制完整性和保密性，核心安全属性。结合上面提到的证明，不仅在内核模型上（规范），也在执行的二进制的硬件上，这些属性都被保证强制实施。因此，seL4是世界上第一个（也是目前唯一）在一个极强的意义上被证明是安全的操作系统。 最后，seL4是第一个（也是目前唯一），保护模式的操作系统内核与健全完善的时间性分析。这意味着其有对中断延迟（以及任何其他的内核操作的延迟）的可证明的上限。因此，它是有内存保护的内核中唯一的可以给你硬实时保证的。

seL4是否具有了零错误？

功能正确性的证明指出，如果证明假设得到满足，seL4内核的实现它的规格相比就没有偏差。安全证明指出，如果内核是根据证据假设配置的，并进一步满足硬件的假设，本规范（和它的seL4内核实现）强制执行了一些强大的安全属性：完整性，保密性和可用性。 仍然有可能存在本规格中未意料到的功能，同时一种或多个的假设可能是不适用的。安全属性可能足够满足你的系统的需求，但也可能并非如此。例如，保密证明没有关于不存在的隐藏定时通道的保证。

因此，问题的答案取决于你对错误的理解。在形式软件验证（代码实现规范）的理解中，答案是肯定的。在一般的软件用户的理解中，答案是有可能，因为还有可能是硬件错误或未得到满足的证明假设。对于高保障系统来说，这不是一个问题，因为硬件的分析和证明的假设比分析具备相同的硬件，和测试假设的大型软件系统容易的多。

seL4证明是安全吗？

这取决于你所说安全的意思。在传统的操作系统的安全性的解释，答案是肯定的。特别是，seL4已被证明强制执行特定的安全性能，即在一定条件下的完整性和保密性。这些证明都是关于seL4的程序用于构建安全系统的非常有力的证据。 一些证据的假设可能有限制条件，例如DMA的使用被排除在外，或仅允许由正式由用户进行验证的受信任驱动程序。虽然这些限制对高保障系统是常见的，我们正在努力地以减少它们，例如通过在x86上使用IOMMU或在ARM上使用System MMU。

如果我运行了seL4，我的系统就是安全吗？

这并不是自动保证的。安全是一个跨越整个系统，包括与人交互那一部分的问题。OS内核，无论验证与否，并不会自动使系统安全。事实上，任何系统，无论多么安全的，都可能在不安全的方式下使用。

但是，如果被正确地使用，seL4通过具体的安全理论的支持，给系统架构师和用户提供了强大的机制来实现安全策略。

什么是证明假设？

简明的版本是：我们假设在内核的汇编代码是正确的，硬件表现是正常的，内核的硬件管理（TLB和高速缓存）是正确的，启动代码是正确的。硬件模型假设DMA将被关闭或者被信任。安全证明额外给出了一个系统配置的条件列表。

我该如何充分利用了seL4的形式证明？

seL4证明仅仅是在构建安全的系统的第一步。它们提供应用程序和系统开发人员需要的工具来提供证据证明他们的系统是安全的。

例如，可以使用功能的正确性证明来表明与内核的应用程序接口是正确的。我们可以使用完整属性来证明别人无法干扰私有数据，以及保密的证据来证明其他人将无法访问私有数据。可以将所有的整个（one-machine）系统绑定到一个证明中，而不需要验证整个系统的代码。

有之前未被验证的操作系统的内核吗？

操作系统验证至少可以追溯到40年前的20世纪70年代中期，所以关于操作系统内核的验证有大量的前期工作。还可以看一个关于2008年来的OS验证全面性概述的论文以及2014年来的seL4概述论文的相关工作部分。

seL4的新的和令人兴奋的事情是，

a）强大的属性，如功能正确性，完整性，保密性，

b）具有直接针对代码的正式验证属性 - 最开始是C，现在可以针对二进制。此外，seL4证明是机器检查，不只是基于笔和纸。

之前的验证要么没有完成其证明，或只针对更浅的属性，如没有未定义执行，或者它们验证代码的手动构造模型而不是代码本身。 先前的验证中有一部分是令人印象深刻的成就，它们奠定了基础，没有这些基础，seL4证明就不会被实现。只是在最近五到十年，代码验证和定理证明技术进步到足以使大量的代码级证明是可行的。

我可以用seL4做什么？

你可以将seL4用于研究，教育和商业。详情参见标准开放源代码规定的许可证附带的代码。不同的许可证适用于代码的不同部分，但这些条件都是为了方便代码的采用。

许可证条件是什么？

seL4内核是在GPL2许可证下发布。用户空间工具和库大多是在BSD。

我该如何给seL4做贡献？

简单地说，seL4是在拥有代码的合作伙伴之间的复杂协议下发布的。发布的条件是，我们跟踪的所有贡献，并从所有参与者那获取一个签名的协议许可。

我怎样才能构建seL4系统？

与Linux操作系统相比，在seL4系统上构建一个系统要求多的多。将你的系统分解为模块，你需要找出每个模块需要访问哪些硬件资源，你需要为你的平台构建设备驱动程序（在libplatsupport下有少量为支持的平台提供的驱动），你必须把它集成成某物来运行。 为了做到这一点，有两种推荐的方式。

• CAmKES是基于微内核的嵌入式系统的组件架构。它提供了一种语言用于描述组件的资源的分配和组件的地址空间的分配。
• 建立在libsel4utils上，它提供了如进程之类的有用的抽象，但一般级别比较低。

此外，新南威尔士大学的先进操作系统课程有一个扩展项目组件来在seL4之上创建一个OS。如果你有机会得到Sabre Lite开发板，你应该能够自己进行项目开发工作来做为熟悉seL4的一种方式。

哪里可以了解更多信息？

• 从L3到了seL4 - 20年内在微内核我们学到了什么？20年L4微内核的回顾; 

http://ts.data61.csiro.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml

• 原始的2009论文描述了seL4及其形式化验证;

http://ts.data61.csiro.au/publications/papers/Klein_EHACDEEKNSTW_09.abstract

• 更长的论文，详细说明了seL4的完整验证的故事，其中包括高层次的安全性证明，二进制校验和时间性分析。它还包含验证成本的分析，以及和传统设计系统的比较。

http://ts.data61.csiro.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml

本文来自：http://sel4.systems/FAQ/ 译者：网络整理，有删改

seL4代码托管地址: https://github.com/seL4/seL4  seL4项目主页:http://sel4.systems/