seL4 on RISC V Renode
summary
seL4 boots under Renode on a SiFive FU540 emulation and successfully runs the seL4-test suite (multi-hour run completes with all tests passing) after a small kernel tweak to remove problematic sfence arguments. Build uses repo + Docker, CMake/Ninja, and produces an ELF loaded by bbl/elf-loader. A Camkes/CampKeys setup composes a serial server/time server system, CampKeys generates ~27 files and computes roughly 1,000 capabilities so manual bookkeeping isn’t needed. Robot framework drives CI-style tests via Renode’s declarative monitor scripts and virtual networking support.
AI-written summary · about
chapters (12)
- 0:00Introduction to seL4
- 0:51Understanding seL4 basics
- 6:02Core security concepts
- 8:48Architectural strategies
- 11:09Setting up the environment
- 17:29Configuring and building
- 23:01Emulation with Renode
- 29:06Automated testing with Robot
- 32:34Complex system development
- 38:18Camkes implementation
- 48:28Building and running Camkes
- 52:30Conclusion and boot process
related talks
22mRISC-V & Renode: towards software-driven development
14mSimulating Heterogeneous Multi-node 32-bit and 64-bit RISC-V Systems Running Linux and Zephyr
29mRenode coming to a cloud near you
25mThe State of RISC V Software
26mseL4 and BEAM: A match made in Erlang
01h 00mHow to run Linux on RISC-V (with open hardware and open source FPGA tools)
10mRemote Development with SCRx-based SDK
34mRISC-V-Based Sandboxing for Secure and Efficient Software Execution