Thomas Leonard's blog

Lambda Capabilities

"Is this software safe?" is a question software engineers should be able to answer, but doing so can be difficult. Capabilities offer an elegant solution, but seem to be little known among functional programmers. This post is an introduction to capabilities in the context of ordinary programming (using plain functions, in the style of the lambda calculus).

Isolating Xwayland in a VM

In my last post, Qubes-lite with KVM and Wayland, I described setting up a Qubes-inspired Linux system that runs applications in virtual machines. A Wayland proxy running in each VM connects its applications to the host Wayland compositor over virtwl, allowing them to appear on the desktop alongside normal host applications. In this post, I extend this to support X11 applications using Xwayland.

Qubes-lite with KVM and Wayland

I've been running QubesOS as my main desktop since 2015. It provides good security, by running applications in different Xen VMs. However, it is also quite slow and has some hardware problems. I've recently been trying out NixOS, KVM, Wayland and SpectrumOS, and attempting to create something similar with more modern/compatible/faster technology.

This post gives my initial impressions of these tools and describes my current setup.

CI/CD Pipelines: Monad, Arrow or Dart?

In this post I describe three approaches to building a language for writing CI/CD pipelines. My first attempt used a monad, but this prevented static analysis of the pipelines. I then tried using an arrow, but found the syntax very difficult to use. Finally, I ended up using a light-weight alternative to arrows that I will refer to here as a dart (I don't know if this has a name already). This allows for static analysis like an arrow, but has a syntax even simpler than a monad.

Using TLA+ to Understand Xen Vchan

The vchan protocol is used to stream data between virtual machines on a Xen host without needing any locks. It is largely undocumented. The TLA Toolbox is a set of tools for writing and checking specifications. In this post, I'll describe my experiences using these tools to understand how the vchan protocol works.

A Unikernel Firewall for QubesOS

QubesOS provides a desktop operating system made up of multiple virtual machines, running under Xen. To protect against buggy network drivers, the physical network hardware is accessed only by a dedicated (and untrusted) "NetVM", which is connected to the rest of the system via a separate (trusted) "FirewallVM". This firewall VM runs Linux, processing network traffic with code written in C.

In this blog post, I replace the Linux firewall VM with a MirageOS unikernel. The resulting VM uses safe (bounds-checked, type-checked) OCaml code to process network traffic, uses less than a tenth of the memory of the default FirewallVM, boots several times faster, and should be much simpler to audit or extend.

CueKeeper Internals: Experiences with Irmin, React, TyXML and IndexedDB

In CueKeeper: Gitting Things Done in the browser, I wrote about CueKeeper, a Getting Things Done application that runs client-side in your browser. It stores your actions in a Git-like data-store provided by Irmin, allowing you to browse the history, revert changes, and sync (between tabs and, once the server backend is available, between devices). Several people asked about the technologies used to build it, so that's what this blog will cover.

CueKeeper: Gitting Things Done in the Browser

Git repositories store data with history, supporting replication, merging and revocation. The Irmin library lets applications use Git-style storage for their data. To try it out, I've written a GTD-based action tracker that runs entirely client-side in the browser.

CueKeeper uses Irmin to handle history and merges, with state saved in the browser using the new IndexedDB standard (requires a recent browser; Firefox 37, Chromium 41 and IE 11.0.9600 all work, but Safari apparently has problems if you open the page in multiple tabs).

Securing the Unikernel

Back in July, I used MirageOS to create my first unikernel, a simple REST service for queuing file uploads, deployable as a virtual machine. While a traditional VM would be a complete Linux system (kernel, init system, package manager, shell, etc), a Mirage unikernel is a single OCaml program which pulls in just the features (network driver, TCP stack, web server, etc) it needs as libraries. Now it's time to look at securing the system with HTTPS and access controls, ready for deployment.

Visualising an Asynchronous Monad

Many asynchronous programs make use of promises (also known as using light-weight threads or an asynchronous monad) to manage concurrency. I've been working on tools to collect trace data from such programs and visualise the results, to help with profiling and debugging.

The diagram below shows a trace from a Mirage unikernel reading data from disk in a loop. You should be able to pan around by dragging in the diagram, and zoom by using your mouse's scroll wheel. If you're on a mobile device then pinch-to-zoom should work if you follow the full-screen link, although it will probably be slow. If nothing else works, the ugly zoom buttons at the bottom zoom around the last point clicked.