Contemporary operating systems suffer from being enormous code bases, riddled with bugs, still supporting legacy hardware (like floppy drives). A common attack vector is based on unsafe memory operations - lack of bounds checks (buffer overflows) and temporal memory safety violations (double free, use after free).

But the environment changed: for security reasons, each service is usually isolated in its own virtual machine, and the virtual machines are scheduled by the hypervisor onto the physical hardware. The requirements for operating systems changed, but most operating systems are only extended to support more complex environments.

In this talk I will present a radical approach to operating systems design: back to ring 0, starting from scratch. Programming language technology has progressed since UNIX was written in C, automated memory management is widely used, strong and static types are usable, and we learned how to build reusable libraries and package those.

MirageOS is a library operating system written mostly in OCaml, a functional and modular programming language. It targets hypervisors, thus does not contain hardware-specific drivers, but generic drivers (e.g. a VirtIO network driver). Each MirageOS application consists of only those OCaml libraries required - why should my name server have user management and a file system? The lines of code, and thus the attack vectors, are drastically reduced. We already implemented various common network protocols, such as HTTP, TCP/IP, TLS, DHCP.

I will explain the design and implementation of our TLS stack in more detail, which separates the effectful bits from the protocol logic very clearly, while preserving reasonable performance.

Links:

• mirage.io
• nqsb.io

Hannes Mehnert

Hannes Mehnert is currently a PostDoc at the University of Cambridge. In his spare time, he is not only a hacker, coauthor of a book on indian cuisine and functional programming in JavaScript, but also a barista and likes to travel with and repair his recumbent bicycle.

He researches in several engineering areas: from programming languages (such as compiler optimisation visualisation and type systems) over full functional correctness proofs of object-oriented code, development environments for dependently typed languages, to re-engineering network protocols (TCP/IP) and security protocols (TLS, OTR). He feels safe in a garbage collected environment, and appreciates the expressive power of declarative purely functional code.

Websites:

• www.cl.cam.ac.uk/~hm519/
• hannes.nqsb.io
• @h4nnes