RISC-V在其RV4处理器上验证了seL64微内核

RISC-V基金会宣布已验证 微内核如何工作 seL4在具有 指令集架构 RISC-V。 其中，验证过程简化为seL4可靠性的数学证明，这表明它完全符合正式语言中指定的规范。

可靠性测试使seL4可在基于RISC-V处理器的关键任务系统中使用 RV64，这需要更高的可靠性，并且不能保证会出现故障。

运行在seL4内核之上的软件开发人员可以完全确定，如果系统某一部分发生故障，则该故障不会扩散到系统的其余部分，尤其是其关键部分。 。

关于seL4

seL4体系结构 值得注意的是删除了一些部分来管理用户空间中的内核资源 并使用与用户资源相同的访问控制方法。

微内核 不提供高级抽象 已经准备好管理文件，进程，网络连接等，但是 仅提供了最小的机制来控制对物理地址空间的访问，中断和处理器资源。

与计算机交互的高级抽象和控制器是在微内核之上以用户级别执行的任务的形式实现的。

通过定义规则来组织对此类任务对微内核中可用资源的访问。

RISC-V提供了一个开放而灵活的系统 机器指令 允许创建用于任意应用的微处理器，而无需扣除 并没有施加使用条件。

RISC-V允许您创建完全开放的SoC和处理器。 当前，根据RISC-V规范，多家公司和社区获得了各种免费许可（BSD，MIT，Apache 2.0），正在开发数十种已经生产的微处理器内核，SoC和芯片的变体。

自Glibc 2.27，binutils 2.30，gcc 7和Linux 4.15内核发布以来，对RISC-V的支持一直存在。

关于seL4微内核测试

最初，微内核 seL4已针对32位ARM处理器进行了验证，而 x86 64位处理器的更高版本.

可以看出，RISC-V开放硬件体系结构与开放微内核的结合 seL4将达到新的安全水平因为将来的硬件组件也可以得到完全验证，这对于专有硬件体系结构是不可能实现的。

检查seL4时，必须假定硬件运行正常（即，如指定的那样）。 假设首先要有一个明确的规范，但并非所有硬件都如此。 

但是，即使存在这样的规范并且是规范的（即以支持有关其属性的数学推理的数学形式主义形式书写的），我们如何知道它实际上捕获了硬件的行为？ 

现实情况是，我们可以肯定不会。 硬件与软件没有什么不同，因为两者都是错误的。

但是拥有一个开放的ISA不仅具有免版税的优势。 其一是它允许开源硬件实现。

在检查seL4时，假定设备按指示工作，并且规格充分描述了系统的行为，但实际上设备并非没有错误，这在推测执行机制中经常出现的问题已得到很好的证明。说明。

开放的硬件平台简化了变更的集成 例如，与安全相关的功能是通过第三方渠道阻止所有可能的泄漏渠道，在这种情况下，通过硬件解决问题要比尝试通过软件找到解决方案要有效得多。

最后，如果您想了解更多信息，可以查阅 以下链接。