The Engineering Question
How can an open processor architecture and a small, capability-based kernel work together to support secure embedded virtualization?
My Contribution
My master's research implemented seL4 with RISC-V H-extension v0.6.1 on a Rocket softcore in the FPGA fabric of a Zynq UltraScale+ MPSoC ZCU102. The work brought the processor's virtualization support and the microkernel into the same hardware–software design.
Research Outputs
The thesis, seL4 on RISC-V - Developing High Assurance Platforms with Modular Open-Source Architectures, is available through Grand Valley State University's ScholarWorks repository.
The related paper, Embedded Virtualization on RISC-V with seL4, coauthored with Nabeeh Kandalaft, appeared at IEEE UEMCON in 2023 and received a Best Paper Award.
The Broader Thread
This work connects to my ongoing engineering in seL4 virtual machine monitors, board support packages, device drivers, and isolation across ARM and RISC-V platforms.
Interested in this area? Start a conversation →