TITLE : MirageOS - robust operating system design from the grounds up
Click here to download the PDF Slides
ABSTRACT :
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.
BIO :
Hannes Mehnert is a postdoctoral researcher at University of Cambridge
working with the semantics, systems, and security group. He finished
his PhD at the IT University of Copenhagen about formally verifying
software.
He researches in several engineering areas: from programming languages
(such as compiler optimisation visualisation, type systems) over full
functional correctness proofs of object-oriented code, development
environments for dependently typed languages, to network protocols
(TCP/IP) and security protocols (TLS, OTR). He feels safe in a garbage
collected environment, and appreciates purely functional goodness.