Publications and Talks

Published: 2019-09-10 (last updated: 2020-01-07)

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


Chaos Communication Congress 2019 (36c3) - Leaving Legacy Behind
Presenting the current state of MirageOS unikernels, with a focus on the reduction on resource usage (carbon footprint) of network services.

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 Communication Congress 2018 (35c3) - 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


Radical Networks 2019 - A Firewall for Your Radical Network (recording)
Discusses how to give a general understanding and strategy plan for network security tailored to everyone's individual needs. Explains what a network protocol is and how we read it, including insecure and secure protocols. Looks at tools to analyze and learn about a network (e.g. wireshark, traceroute). The idea of QubesOS and how to structure your system into different Qubes and run them, focusing on configuring and testing a firewall and why it has been obscure in the past, using our [Qubes-Mirage-Firewall](/Our Work/Projects#Firewall).

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.

BOB Konferenz 2016 - Dynamic programming at ease - with grammars, algebras, products
Discusses how dynamic programming is a technique to solve a combinatorial optimization problem by reducing complexity through reusing intermediate results that are stored in a table, instead of computing them again. Explores a formal framework for dynamic programming on sequences. Separating the problems of search space description, candidate description, candidate evaluation and tabulation helps us in thinking about dynamic programming.

QCon 2016 - API-first Architecture Transformation
Talks about the case study of building an API-first architecture at Etsy. She talks about what problems prompted this drastic change, the new tools they had to build to be able to work with the new system and what mistakes they made along the way.

EnthusiastiCon 2016 - OMG building a shell in 10 minutes
According to Wikipedia a shell script is a computer program designed to be run by a command line interpreter. Typical operations performed by shell scripts include file manipulation, program execution, and printing text. Sounds complicated? In this talk Stefanie Schirmer shows how to build a shell in ten minutes.

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.