Summary. My PhD dissertation work proposed an architecture for constructing new implementations of standard Internet protocols with integrated formal methods such as model checking and functional programming that were then not used in deployed servers. A more informal summary is "rewrite all the things in OCaml from C!", which lead to a merry adventure into implementing many networks protocols from scratch in a functional style, and learning lots about how to enforce specifications without using a full blown proof assistant.
In the late 90s while working at MVACS on the Mars Polar Lander, I found myself using the secure OpenBSD operating system to deploy the self-hosted service that @nickludlam and I have run together ever since. I became an OpenBSD developer with commit rights and went to several hackathons, a sample of which you can read in OpenBSD C2K5 thoughts. Back then, my primary open source experience was working on C code in the OpenBSD base system and in PHP code while hacking on the popular Horde/IMP groupware system for my own email.
I rapidly tired of hacking in C code and looked for safer alternatives. While procrastinating over PhD coffee with Dave Scott he suggested I look into writing a system daemon in OCaml. Why not have a go at a SSH server written entirely in a type-safe functional language? Being a PhD student sorely in need of a challenge, I took up the project.
There were a couple of different challenges involved:
- There was no good way of expressing packet parsing policies for the complex dynamics of real Internet protocols. I developed a domain-specific language for this in OCaml known as MPL (the "meta packet language") and used it to successfully parse DNS, BGP, Ethernet, IP, SSH and a host of other binary protocols. The work won the best student paper award at EuroSys 2007 in Melange: creating a "functional" internet, and helped to lay the foundation for a growing belief in industrial circles that C was not the only way to do low-level parsing.
- Once parsing was fixed, I also had to express complex state machines using OCaml. Using a functional language was not a silver bullet to solve this problem since the state machines still had to be verified against a spec. I had a first go at this in The Case for Abstracting Security Policies using system call tracing, but decided that was a dead end due to the poor granularity. I then designed another domain-specific language called SPL in On the challenge of delivering high-performance, dependable, model-checked internet servers and SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions and a detailed writeup in Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language. This turned out to be a pretty pragmatic solution by using model checking and even included an early visual debugger for protocol state machines. The work holds up surprisingly well in 2021: while theorem provers and refinement types based languages like Fstar produce amazing results, they still require a lot more effort than my simpler model-checking-based solution.
All this work resulted in the Melange framework that I put together in OCaml and evaluated, and published in my Creating High-Performance, Statically Type-Safe Network Applications PhD thesis with the following abstract:
A typical Internet server finds itself in the middle of a virtual battleground, under constant threat from worms, viruses and other malware seeking to subvert the original intentions of the programmer. In particular, critical Internet servers such as OpenSSH, BIND and Sendmail have had numerous security issues ranging from low-level buffer overflows to subtle protocol logic errors. These problems have cost billions of dollars as the growth of the Internet exposes increasing numbers of computers to electronic malware. Despite the decades of research on techniques such as model-checking, type-safety and other forms of formal analysis, the vast majority of server implementations continue to be written unsafely and informally in C/C++.
In this dissertation we propose an architecture for constructing new implementations of standard Internet protocols which integrates mature formal methods not currently used in deployed servers: (i) static type systems from the ML family of functional languages; (ii) model checking to verify safety properties exhaustively about aspects of the servers; and (iii) generative meta-programming to express high-level constraints for the domain-specific tasks of packet parsing and constructing non-deterministic state ma- chines. Our architecture -— dubbed MELANGE -— is based on Objective Caml and contributes two domain-specific languages: (i) the Meta Packet Language (MPL), a data description language used to describe the wire format of a protocol and output statically type-safe code to handle network traffic using high-level functional data structures; and (ii) the Statecall Policy Language (SPL) for constructing non-deterministic finite state automata which are embedded into applications and dynamically enforced, or translated into PROMELA and statically model-checked. Our research emphasises the importance of delivering efficient, portable code which is feasible to deploy across the Internet. We implemented two complex protocols -— SSH and DNS -— to verify our claims, and our evaluation shows that they perform faster than their standard counterparts OpenSSH and BIND, in addition to providing static guarantees against some classes of errors that are currently a major source of security problems.
I didn't do much on this immediately after submitting my thesis since I was busy working on Xen Hypervisor from 2006-2009 or so. However, the first thing I did when I quit Citrix was to start the MirageOS project (the successor to Melange) with Thomas Gazagnaire and Dave Scott in order to develop better personal data infrastructure with Personal Containers. This formed the foundation for my subsequent research into library operating systems and the concept of Unikernels. Read more about the subsequent work there, or sample Turning Down the LAMP: Software Specialisation for the Cloud to get a taster of the direction Melange evolved in.
Reflecting on my PhD research in 2021, I think that it was a pretty good piece of systems research. It didn't make any deep contributions to formal verification or programming language research, but it did posit a clear systems thesis and implement and evaluate it without a huge team being involved. That's more difficult to do these days in the era of large industrial research teams dominating the major conferences, but certainly not impossible.
Choosing a good topic for systems research is crucial, since the context you do the research in is as important as the results you come up with. Much of my subsequent career has been influenced by the "crazy challenge" that Dave Scott set me back in 2003 to do systems programming in a functional language, with all the intellectual and engineering challenges that came along with that extreme (back in 2003) position.
Relevant Ideas
- Not-quite-so-broken TLS in OCaml
by Hannes Mehnert and David Kaloper-Mersinjak cosupervised with Peter Sewell in 2014 (Completed). - Functional ABNF parser generators
by Nicholas Skehin in 2011 (Completed, Part II).
Relevant Papers
|
[»] Using functional programming within an industrial product group: perspectives and perceptions |  |
|
[»] Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language |  |
|
[»] Melange: creating a "functional" internet |  |
|
[»] SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions |  |
|
[»] On the challenge of delivering high-performance, dependable, model-checked internet servers |  |
|
[»] The Case for Abstracting Security Policies |  |
News Updates
» Paper on our experiences with writing the Xen control stack in OCaml at ICFP 2010.» Paper on a DSL for specifying temporal protocol automata at ICFEM 2009.» Won best student paper for my PhD work on a high-performance functional packet parsing DSL at Eurosys 2007!» Workshop paper on temporal automata for protocol specifications at SPIN 2005.» Paper on temporal automata for protocol implementations at HotDep 2005 / «
» Blogged about the OpenBSD C2K5 hackathon trip in Canada.» Paper on security policies using a declarative language at SAM 2003.