Verified seL4 on secure RISC-V processors

on YouTube ↗45m

" summary

seL4 is ported and running on RISC-V hardware (tested on SiFive HiFive Unleashed) with IPC latency comparable to ARM; HENSOLDT funds a full verification effort that is a few months from completing the critical formal refinement proof from abstract model to C and a binary-verification toolchain aimed for April. work includes hypervisor support, mixed‑criticality time protection (partitioning and flush padding) and active engagement with the RISC‑V Security committee to add ISA mechanisms.

AI-written summary · about

" chapters (12)

1. 0:00Introduction to seL4
2. 1:40Microkernel architecture
3. 4:16Licensing and IP
4. 6:07Real-world applications
5. 7:40Formal verification process
6. 11:08seL4 on RISC-V
7. 15:03RISC-V verification
8. 17:18RISC-V architecture insights
9. 21:52Mixed-criticality support
10. 25:59Timing channel defense
11. 30:20Hardware-software contract
12. 38:31seL4 foundation

" related talks

• 44mThe seL4 Foundation – growing through upheavalGernot Heiser · linux.conf.au 2022
• 18mProving RISC-V Security Model Compliance with SESIPEve Atallah · RISC-V Summit 2022
• 18mCPU Security in the Context of RISC-VKarthik Raj Shekar · RISC-V Summit North America 2024
• 19mAn Open Source Approach to System SecurityHelena Handschuh · RISC-V Summit 2019
• 47mA Security RISC? The State of Microarchitectural Attacks on RISC-VDaniel Weber, Michael Schwarz, Lukas Gerlach · Black Hat Europe 2023
• 13mRISC-V: Securing the Future of Open Source ComputingAndrew Dellow · Spring 2022 RISC-V Week — RISC-V International Day
• 28mFormal Assurance for RISC-V ImplementationsDaniel Zimmerman, Joseph Kiniry · 8th RISC-V Workshop Barcelona 2018
• 12mHardware Verification of Timing Side Channel Freedom in the Spectre EraAdam Chlipala, Clément Pit-Claudel, Thomas Bourgeat, Stella Lau · PLARCH 2023