在RISC-V上验证到二进制代码

2020年6月20日我们宣布，世界上第一个操作系统（OS）内核具有机器检查的实施正确性证明，现在还针对RV64架构进行了验证，使其成为RISC-V的第一个正式验证的操作系统。我们很高兴地宣布，此验证现已扩展到可执行的二进制文件，这意味着在处理器上运行的机器代码被证明是对内核规范进行正确的。 RISC-V是实现这一目标的前64位架构。

先前宣布的证据意味着，根据SEL4的C语言的语义，内核将始终按照指定行为。其中，这意味着SEL4不能用堆栈溢出攻击，格式化的输入或其他形式的代码注射或控制流动劫持 - 它在非常强烈的意义上被证明是可怕的。但是，仍然存在由错误（或损害）C编译器或来自编译器和内核开发人员以不同方式解释C语义的安全漏洞的风险。

新完成的二进制验证完全删除了这些风险 - 它保证了我们证明了关于可执行代码的C代码的属性，从而根据内核的正式规范所需的可执行内核二进制行为。

虽然SEL4的实施正确性证明，但互动定理证明，数十万（大多数手写但机器检查）的证明线，二进制验证使用自动刀具链（有关详细信息，请参阅SEL4白皮书）。刀具链将C代码以及二进制转换为代表程序控制流的中间语言。然后，它使用SMT求解器来证明两个程序的等价，一次一个短代码序列。

SMT求解器通过非常有效地探索状态空间，使用状态压缩技术来证明属性，以使问题发布。我们以前为32位ARMV7架构建立了二进制验证工具链。随着状态空间呈指数呈指数级大小，将步骤达到64位架构，需要克服显着的可扩展性挑战 - 这是我们围绕马特布拉切尔和Zoltan Kocsis的团队的聪明才智可以克服。

这项工作代表了RISC-V和SEL4生态系统的重要步骤。除RISC-V之外的64位架构目前还有一个具有如此全面验证和安全故事的操作系统。和SEL4有RISC-V的理想基础，用于在计算机系统安全方面驾驶进一步创新，特别是根据我们通过调用时间保护的方法对我们通过定时渠道进行系统预防的工作。保持调整以获得更多令人兴奋的结果！

我们现在通过宣布RISC-V International和Sel4 Foundation正在将彼此作为助理成员加入彼此来形式化两种生态系统之间的联系。