Experience of running hybrid CHERI userspace on seL4
In this article, I share the experience of getting to a point where we could run userspace applications in seL4, which had CHERI capabilities enabled(Hybrid mode). CHERI  is an architectural extension that adds HW capabilities to modern processors. Morello  is the ARM implementation of CHERI. SeL4  is a formally verified microkernel widely deployed in security-critical applications. Since seL4 is formally verified, it might not benefit from CHERI capabilities, but the user application running on seL4 will still benefit.
Linux Docker Build
Steps to build the linux kernel in a docker container and install it on the host. This is done so that it does not mess up the packages installed on the host.
Virtual Machine Core Idea
While trying to find tutorials on how to implement a simple hypervisor, most of the articles I found online were about using Intel’s VT-X extensions – called
Hardware extensions for virtualizationto implement a Virtual machine . However, the idea of a virtual machine is so much older than the hardware extensions meant to make virtualization more accessible. So, I wanted to get to the crux of what we are virtualizing and how. Then later, see how hardware extensions for virtualization make it either easier or speed things up.
Genode: Running out of capabilities on 64-bit platforms
I am using Genode(with seL4) as the OS platform for demonstrating my research ideas. As with starting with a new platform I have run into some hurdles.
seL4: Page count mismatch in sel4utlils vspace library
Updated Feb 2, 2022 Root cause at the bottom
I was looking at the sel4utils/vspace library and noticed a mismatch in the number of pages allocated as per the two data structures which keep track of the address space. Below I have laid out my test setup, steps to reproduce and finally the exact questions.
This is my first blog post. Hopefully, I will be able to soon replace this with a real post.