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 our research areas while embracing an open, inclusive community that we greatly admire. Most recently, we have been interested in the use of Xen on ARM devices. We believe that Xen may be uniquely situated to serve as a medium- to high-assurance platform for future mobile and automotive systems, particularly when combined with our SMACCMPilot and related efforts.
In short, the fact that we combine our secure platform designs and tools — tools like Ivory and HaLVM — with an active, vibrant open source project like Xen has led to some very cool technologies for Galois over the last months and years, and we certainly see this trend continuing into the future.