Over the last few months, Galois has published or spoken about a variety of technologies based on the open source Xen hypervisor: our port of FreeRTOS on Xen, our MAC-enhanced version of the XenStore, and, of course, our continuing work on the Haskell Lightweight Virtual Machine (a.k.a., the HaLVM). Based on all this activity, I get asked the obvious question: Why is Xen so compelling to Galois? For the last fifteen years, Galois has been building trustworthy solutions to meet our customers’ critical demands. When we build out some of these solutions, both as prototypes and as deliverable software, we inevitably run into the question of platform. Our designs are good, and our software is good, but what platform can we run on that provides the stability and guarantees that we require? In the future, we hope to see high-assurance, formally verified separation and real-time kernels on which we can build the truly robust systems of our dreams. NICTA’s seL4 has taken several major steps towards that goal, and we follow its development quite closely; in fact, we have used it in some of our more forward-looking projects. While we wait for these technologies to mature, however, Xen has been a great choice for Galois. Xen has many aspects of a secure microkernel that we need: it is small, it provides strong security through its XSM layer, and it can run on a wide variety of hardware platforms. Further, because Xen is open source software, we can freely inspect, modify, and remove any code that interferes with our efforts. Better yet, because Xen is a virtualization solution, it allows us to run full-featured operating systems as “applications” on our kernel. Thus, in many cases, we can provide our clients extremely secure solutions without sacrificing the user interfaces they expect. In addition, we have been impressed by the passion and openness of the Xen community. Particularly over the last few years, we have seen Xen thrive and expand into areas that match well with...