We implemented, benchmarked, and analyzed OpenMZ, a separation kernel for RISC-V targeting secure coprocessors and embedded devices. OpenMZ is an open-source implementation of the MultiZone API, which partitions a system into a fixed number of zones that can communicate with each other and handle interrupts.
OpenMZ has a small code base of around 800 lines, making the kernel formally verifiable, and with an open-source RISC-V processor, it can be the foundation of a fully verified computing system. Moreover, OpenMZ has some real-time properties and a context switch of around 500 cycles, making it suitable for real-time applications.
Our security analysis shows that OpenMZ protects the zones' memory from direct access with RISC-V's PMP-mechanism, but not indirect access, e.g., through the DMA. Moreover, the MultiZone API has some vulnerabilities exposing the zones to both DoS attacks and timing side-channel attacks. To address these security issues, we suggest a few modifications to the API and the scheduler.