Latest Posts

• Determining the PID of a FUSE Daemon based on the /proc/mounts

  I am toying with a trivial Passthrough FUSE file system [1] mounted at /some-path/fusey-files, the PID of the FUSE daemon is 1234. and I wanted to programmatically find out (using /proc or /sys or some other kernel interface such as ioctl) that this mount is backed by the FUSE daemon running at PID 1234? What I have found so far is hacky and imprecise, and I feel like the FUSE module in the kernel must have this information, and I am just missing something.

• Understanding the various mounts setup by a Docker container

  Why does a docker container have so many mounts?

• 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.