back

Trustworthy secure modular operating system engineering

fun(ctional) operating system and security protocol engineering

If you suspend your transcription on amara.org, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!

Please do not press “publish” on amara.org to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.

Video duration
01:01:02
Language
English
Abstract
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.

Talk ID
6443
Event:
31c3
Day
1
Room
Saal 2
Start
12:45 p.m.
Duration
01:00:00
Track
Science
Type of
lecture
Speaker
Hannes Mehnert
David Kaloper
Talk Slug & media link
31c3_-_6443_-_en_-_saal_2_-_201412271245_-_trustworthy_secure_modular_operating_system_engineering_-_hannes_-_david_kaloper
English
0.0% Checking done0.0%
0.0% Syncing done0.0%
0.0% Transcribing done0.0%
100.0% Nothing done yet100.0%
  

Work on this video on Amara!

English: Transcribed until

Last revision: 2 years, 2 months ago