形式化验证在安全操作系统的发展中成为了热门话题！sel4在其官方网站上宣称：安全绝不应成为表现不佳的借口！
seL4是什么？seL4是L4微内核家族中最先进的成员，以其全面的形式验证而著称，这使其与其他操作系统截然不同。seL4在实现这一目标的同时，性能并未受损。
什么是微内核？微内核是操作系统（OS）的核心最小部分。它通常被视为今天的操作系统的一个小型子集。微内核的定义由利特克在[SOSP’95]中提出。因此，微内核不提供如linux或windows等现代操作系统那样在硬件上实现的高层次抽象（如文件、进程、套接字等）。相反，它提供了最基本的机制来控制物理地址空间访问、中断和处理器时间。在L4微内核使用的模式中（seL4亦是如此），一旦内核启动，一个初始的用户级任务（根任务）将获得完全权限来管理所有资源（通常包括物理内存、x86的IO端口和中断）。根任务负责设置其他任务，并向其他任务授予权限以构建完整的系统。在seL4中，像其他第三代微内核一样，这样的访问权限是通过能力授予的（不可伪造的令牌代表特权），且是完全可委托的。
L4微内核家族是什么？L4家族是一系列非常小型且高性能的微内核。第一个L4微内核由约亨·利特克在90年代初研制，并不断演化。参见《From L3 to seL4 What Have We Learnt in 20 Years of L4 Microkernels?》，这是一篇2013年关于微内核发展的系统性介绍论文。原文下载地址：https://www.php.cn/link/0c5bcd68aebc9060a7f2e5047bb962de：
seL4的性能与其他微内核相比如何？据我们所知，seL4在常见的乒乓指标上，即跨地址空间的消息传递（IPC）的操作成本，是世界上最快的微内核之一，欲了解更多信息，请查看L4HQ的性能页面：https://www.php.cn/link/78106a0fa774284d86ec3585a5112ca5。
需要注意的是，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微内核的回顾; https://www.php.cn/link/95ef1128340226d8325ba751bfac05eb
原始的2009论文描述了seL4及其形式化验证;https://www.php.cn/link/4cb4a0aadcf427341c1fe9ae93a5cf31
更长的论文，详细说明了seL4的完整验证的故事，其中包括高层次的安全性证明，二进制校验和时间性分析。它还包含验证成本的分析，以及和传统设计系统的比较。https://www.php.cn/link/b61be50f3f8a606a09d3614e09937e3a
本文来自：https://www.php.cn/link/6b387ebbcb8020ce186644d4a4669c6a 译者：网络整理，有删改
seL4代码托管地址: https://www.php.cn/link/3b81467c62f5cdcc01fdebe09a88faa0 seL4项目主页:https://www.php.cn/link/b32016b92746d5f303795b24402950e5
