CHERI
CHERI and Microkernels
Following the first CHERI Microkernel Workshop in April 2016, there has been substantial interest in whether CHERI's architectural features can help support more expressive or performant microkernel designs. At one end of the spectrum, current virtual-memory-based microkernels (e.g., seL4, L4, Barrelfish) could be extended to support in-address-space memory protection and compartmentalisation, much in the style of CheriBSD. They could also be extended to use certain CHERI features to improve performance — for example, using sealed capabilities to avoid entering the kernel for certain types of delegation operations. At the other extreme, CHERI's protection and compartmentalisation features could be used in place of MMU-based techniques to implement a single address-space operating-system design, minimising or entirely eliminating use of virtual memory.
cl-cheri-microkernel mailing list
We have created a mailing list, cl-cheri-microkernel, to host discussions about using CHERI in microkernel design: