Version 1.7 a new dawn

lecture: Trustworthy secure modular operating system engineering

fun(ctional) operating system and security protocol engineering

Mirleft

We present Mirage OS, a modular library operating system developed from scratch in the functional programming language OCaml. Each service, called unikernel, is an OCaml application using libraries such as a TCP/IP stack, DNS. It is either compiled to a Xen virtual machine image or to a Unix binary (for development). State in 2014 is that it runs on x86 and arm, we implemented a clean-slate TLS (1.0, 1.1, 1.2), X.509, ASN.1 stack, crypto primitives, Off-the-record. We also have TCP/IP, HTTP, a persistent branchable store (similar to git) - all implemented in OCaml. A virtual machine serving data via https is roughly 2MB in size - no libc inside :)

Mirage OS is a (BSD-licensed) research project at University of Cambridge and released in December 2013 a 1.0 version. In 2014, 2.0 got released with full support on arm, a clean-slate TLS implementation, and the branchable data store Irmin. We (Hannes and David) developed a TLS stack from scratch (including cryptographic primitives, X.509, ASN.1), which we will present.

We intentionally breaks with the UNIX philosophy. Instead of using a programming language designed to replace platform-specific assembly code we use the functional programming language OCaml with higher-order functions, a composable module system, pattern matching, a sophisticated type system. Our developed TLS stack separates side effects, such as mutable memory, network input and output, etc., clearly from the pure functional core. This separation is not enforced on a language level, but by convention.

A mirage unikernel runs either as a Xen guest or as native Unix application. Each unikernel runs in a single address space, and does not include layers over layers of abstraction (kernel, user space, file system, processes, language runtime, threads, ...). The performance is not too bad (see link below). Each unikernel only uses those libraries it really needs - e.g. a name server does not depend on a file system or user accounts. A common unikernel is rather small in binary size: a web server, including TCP/IP stack and the data to be served, is less than a megabyte in size, including the OCaml runtime. There is no libc included :)

Modularity is the key for Mirage OS: the same application code can be compiled as a UNIX executable using the POSIX socket API, or as UNIX program using the userspace tun/tap interface and the TCP/IP stack written in OCaml, or as a Xen domU. This eases development, testing, debugging, and deployment.

Our target platform is the cubieboard2, a small board with a dual-core ARM A7 CPU and ethernet (and various other unused interfaces).

Code reviews, comments, contributions are always welcome.


Archived page - Impressum/Datenschutz