Latest Posts
-
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 [6] is an architectural extension that adds HW capabilities to modern processors. Morello [7] is the ARM implementation of CHERI. SeL4 [8] 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 virtualization
to implement a Virtual machine [1]. 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.
-
First Post
This is my first blog post. Hopefully, I will be able to soon replace this with a real post.