SeL4已在RISC-V上验证

seL4(发音为ess-e-ell-4)可以说是世界上最安全的操作系统(OS)内核。

操作系统内核是计算机系统上运行的最低级别的软件。它是在特权模式下执行的代码(RISC-V中的S模式；M模式是为微码/固件保留的)。内核最终负责计算机系统的安全。

seL4是一个微内核。微内核的想法是最大限度地减少可信计算基础--这是系统的一部分，如果它失败了，就没有B计划了。Linux和Windows内核由数千万行代码组成，包含数以千计(更有可能是数万)的错误--这是一个巨大的攻击面。一个设计良好的微内核，比如seL4，大约有10,000行--本质上更可靠。

seL4与所有其他操作系统内核(包括其他微内核)的不同之处在于它的验证故事。它是世界上第一个通过机器检查的、对其C实现的功能正确性进行数学证明的操作系统内核(结果为我们赢得了名人堂奖)。这意味着相对于用数理逻辑表示的规范而言，它被证明是无bug的。到目前为止，它已经证明了进一步的安全属性(这表明规范具有正确的属性)和向下延伸到二进制代码的功能正确性。并且它拥有对硬实时系统的最先进的支持。它是世界上最快的微内核。不管怎么定义，它都是课堂上最棒的。

我们最初为32位ARM处理器验证了seL4。然后我们将其扩展到64位x86处理器。现在到RISC-V RV64处理器。现在涵盖了所有重要的国际会计准则。

RISC-V是一种开放式指令集体系结构(ISA)。seL4是一个开源操作系统微内核。这是天作之合。特别是在安全方面。

当我们验证seL4时，我们必须假设硬件运行正常(即按照规定)。这假设首先有一个明确的规范，但并不是所有的硬件都是这样。但是，即使有这样的规范，并且它是正式的(意思是用支持关于其属性的数学推理的数学形式主义编写的)，我们如何知道它实际上捕获了硬件的行为呢？现实情况是，我们可以相当肯定的是，情况并非如此。硬件和软件没有什么不同，因为它们都有缺陷。

但是，拥有一个开放的ISA的好处不仅仅是免版税。其一是它允许开放源码的硬件实现。苏黎世理工大学开发的CV64(前身为阿丽亚娜)核心就是一个例子。使用开放源码实现，您可以看到您得到了什么，并且可以自己检查它是否存在安全关键错误。这就是德国公司HENSOLDT Cyber GmbH所做的：他们生产了一款基于阿丽亚娜的芯片，具有强大的供应链安全故事。此外，为了用安全操作系统来补充这一点，为在RISC-V上验证seL4提供了资金。[免责声明：我在HENSOLDT Cyber有权益。]

使用开源硬件实现的开放ISA最令人兴奋的方面是验证实现的前景。这听起来是一个很大的要求，但很难实现。但同样的话也适用于经过验证的操作系统内核-直到我们这么做了。我知道有多个团体朝着这个目标努力，迟早会有一个团体成功。这将是实现真正的安全的革命性的一步，我打赌只有几年的时间了！

具有经过验证的开源操作系统的开源硬件对于安全性来说是一件很棒的事情，但还有更多的东西。

开放ISA、开放源码操作系统和开放源码硬件的结合使得以前为硬件制造商保留的硬件-软件接口实现了创新(因此发生得非常缓慢)。这对安全来说真的很重要。

我们都知道幽灵攻击，它利用投机性处决的副作用来窃取机密。人们不太了解的是，仅靠投机性执行是不够的。幽灵需要一个隐蔽的定时通道才能把信息传出去。没有隐蔽的定时通道，就没有幽灵攻击。

防止这些隐蔽的计时通道恰好是我们几年来一直在研究的事情。我们开发了操作系统机制来预防它们，但后来才意识到它们并不完全起作用。更深入地挖掘，我们发现这是因为硬件没有给我们提供正确的机制。换句话说，大多数现有硬件在安全性方面都出现了问题！潜在的原因是ISA，这是我们的硬件-软件合同。ISA指定硬件的功能，但有意抽象出与时间有关的任何内容。但计时可以用来泄露信息，而ISA并没有提供阻止这种情况的手段。因此，ISA不足以确保安全，必须加以改进。

这通常是无望的努力：试图说服硬件制造商同意一份对他们能做的事情施加额外限制的新合同。(相信我，我试过了！)。或者甚至给操作系统提供一个额外的指令，它可以用来击败秘密通道-只要房子没有着火，它们就不太可能听。而且幽灵之火显然还没有燃烧到足够热的程度。

开放式硬件改变了这一点。它使我们无需等待制造商就能进行创新。它使我们能够控制围栏的两边。为了安全起见，它实现了真正的协同设计。

与苏黎世理工大学的Ariane的创建者合作，我们做到了这一点：我们探索了如何只需稍微修改一下硬件-软件合同，就可以给操作系统提供正确的方法来击败秘密通道。我们可以证明，它只需要很少的时间就可以达到高度有效的效果。

RISC-V基金会的相关工作组目前正在讨论这些机制。敬请关注RISC-V在处理器安全性方面的基准设置，与世界上最安全的操作系统内核-seL4相辅相成。

sel4网站解释了sel4，并有一份为非专家编写的白皮书，详细解释了sel4及其验证故事。