Publications and Talks

Published: 2019-09-10 (last updated: 2019-09-12)

We regularly give talks and write publications about our work, OCaml and MirageOS and other aspects of coding, security and computer science that we have expertise in. Below are some examples of these, if you are interested in having a Robur member speak at your event please reach out to us.

Hannes Mehnert


CERN Computing Seminar 2019 – MirageOS: robust and secure services for the cloud
Presenting MirageOS and its advantages along with explaining several applications being developed within it.

BOB 2018 - Engineering TCP/IP with logic
Presents a formal model of TCP/IP (developed 2000-2009 and refurbished since 2016), how it can be used to validate the FreeBSD TCP/IP stack, and what was learned while writing it. It is modeled as a label transition system, including timers, re-transmission, etc.

BornHack 2018 - MirageOS: what did we achieve in the last year?
This is a continuation of earlier talks at Bornhack (2016, 2017), and goes into detail of some active projects, such as: community repository signing (for secure updates), DNS infrastructure, our Prototype Fund sponsored CalDAV-server.

Chaos Computer Club Congress 2018 - Domain Name System
Discusses the basic usage of DNS, including stub and recursive resolver, server; various protocol extensions including zone transfer, dynamic updates, authentication, notifications; privacy extensions (query path minimization, DNS-over-TLS); provisioning let's encrypt certificates; and attacks (poisoning, amplification). Explains the Robur implementation of DNS with above mentioned extensions as minimized MirageOS unikernels.


Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API (JACM vol 66, January 2019), full paper. (Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough)

Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation (Usenix security 2015), video presentation (David Kaloper-Meršinjak, Hannes Mehnert, Anil Madhavapeddy, Peter Sewell)

Not-quite-so-broken TLS 1.3 Mechanized Conformance Checking - TLS 1.3 Ready or Not (TRON), workshop website (David Kaloper-Meršinjak and Hannes Mehnert)

Martin Lucina


FOSDEM 2019 - Solo5: A sandboxed, re-targetable execution environment for unikernels
Explains Solo5 which is a microkernel-friendly, sandboxed, re-targetable execution environment for unikernels, with a taste for minimalism. Presents the interfaces it offers to the unikernel/library operating system/application developer. Using existing library operating systems, such as MirageOS, demonstrates the developer experience for various Solo5 targets, going on to show how rigorously applying minimalist principles to interface design is used to our advantage, blurring traditional lines between unikernels, processes, kernels and hypervisors.


Unikernels as Processes - ACM Symposium on Cloud Computing 2018 (Dan Williams, Ricardo Koller, Martin Lucina, Nikhil Prakash)

Mindy Preston


DevOpsDays MSN 2018 - FuzzOps
Discusses testing software to find bugs before deploying software, including continuous integration solutions and property-based testing. Looks at issues of testing frameworks, including common human errors. Explains fuzzers - a solution to this important problem in which computers generate inputs and find counter examples to enable more complete code testing and bug finding.

Confreaks 2017 - DHCP: IT’S MOSTLY YELLING!! Discusses how the Dynamic Host Configuration Protocol (DHCP) is structured and how it is used in a network. Explains how addressing and packet structure (or yelling) in DHCP works to establish a connection, and what can go wrong. Looks at tcpdump as a way to examine this yelling along with DHCP options to help establish a quieter and more secure connection.

Strange Loop 2015 - Non-Imperative Network Programming
Discusses how network programming is often taught and practiced in C, but it doesn't have to be. We can build better network stacks -- ones more expressive, intuitive, and robust -- in other languages! There are many non-C network stacks in the world, and we can learn a lot from the diversity of solutions for common problems.

Stefanie Schirmer


Berlin Buzzwords 2018 - Your Search Service as a Composable Function
Discusses the real-time processing pipeline of modern search systems. Speaking from her previous experience at Etsy Stefanie explains how several different backends power Etsy's search, among them Solr, Elasticsearch, our own key-value-store Arizona, and services for machine learning and inference. How do all these systems work together, present a common interface to Etsy's developers and a coherent search experience to our users? She talks about their learnings along the way of building this proxy, and trying to find the right abstraction for the search problem.

JSConf EU 2015 - Functional programming and curry cooking in JS
This talk explores functional programming concepts, which help us create powerful abstractions to master complex problems and create more simple and elegant programs. JavaScript allows us to ease into the functional programming style, letting us focus just on the concepts, without the distraction of learning a specific functional programming language. To make the dry functional programming concepts more digestible, we use cooking as an analogy. And since the logician Haskell Curry invented functional programming, we combine our journey in JavaScript with examples and recipes for tasty curry dishes.