RISC-V有很多吸引人的地方，从架构的开放性、基于简单性和可扩展性的全新设计，以及RISC-V基金会从头开始对安全的坚定承诺。因此，RISC-V以其无与伦比的验证和安全故事对开源seL4微内核来说是一个极具吸引力的平台。这导致业界参与者，特别是总部位于德国的HENSOLDT Cyber，在RISC-V和seL4的组合上下了很大的赌注，导致他们资助在RISC-V上对seL4进行正式验证(实现正确性证明)。我将讨论我们在RISC-V架构上实现和验证seL4的经验，以及我们用来构建安全系统的相关开源技术。这包括支持按体系结构的安全方法的CAmkES组件框架，以及旨在降低文件系统和设备驱动程序等经过验证的系统组件成本的Cogent系统语言。一个有趣的方面是定时频道。多年来，我们一直致力于“时间保护”，也就是内存保护的时间等价物，作为一种系统的定时通道预防。我们在x86和ARM处理器上的经验是，它们完全缺乏这样做的机制。RISC-V提供了一个机会来实现这一点，我将报告我与RISC-V基金会的安全常设委员会合作将所需机制纳入处理器规范的经验。
@misc{Heiser_20，Author={Heiser，Gernot}，Month=Jan，Date={2020-1-17}，Year={2020}，关键词={操作系统；验证；网络安全；安全关键系统；{RISC}-{V}}，标题={安全{RISC}-{V}处理器}，地址={黄金海岸}，NumPages={Online}，视频={https://www.youtube.com/watch?v=wJ96s3pNtI0&；Feature=youtu.be}，备注={at linux.conf.au}，Booktitle={linux.conf.au}，Publisher={Online}，幻灯片={https://ts.data61.csiro.au/publications/papers/Heiser_20.slides.pdf}}