RISC-V基金会 关于验证微内核的运行 在具有 RISC-V 指令集架构的系统上。 验证归结为 seL4 操作的可靠性，表明完全符合正式语言中指定的规范。 可靠性证明 基于 RISC-V RV4 处理器的关键任务系统中的 seL64，需要提高可靠性并保证不出现故障。 在 seL4 内核之上运行的软件开发人员可以完全确信，如果系统的某个部分出现故障，这种故障不会蔓延到系统的其余部分，特别是其关键部分。
seL4 微内核最初针对 32 位 ARM 处理器进行验证，后来针对 64 位 x86 处理器进行验证。 值得注意的是，开放RISC-V硬件架构与开放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 支持就已存在。
来源： opennet.ru