Practical Formal Methods to Deliver Secure, High-Performance Internet Applications
Anil Madhavapeddy
The Internet's security record in recent years has been extremely poor, with self-propagating malware regularly wreaking havoc due to software errors. Most efforts in the systems community have focussed on containment (e.g., virtualisation) or innoculation (e.g., non-exec heaps) to prevent attackers from taking control of hosts. However, attackers persist in finding ways past these defences.
We argue that these approaches are insufficient, and describe our solution of recreating complex Internet servers using modern static type systems and model checkers to obtain more formal security guarantees. We base our work on OCaml, and the resulting applications are high-performance, portable and efficient. We contribute the MPL data description language, used to parse complex network protocols (e.g. SSH, DNS, BGP, IPv4), and the SPL state machine description language which allows the static verification and dynamic enforcement of protocol state machines.
As a concrete case study, we demonstrate performance results for our 'mlssh' server and compare it with the reference OpenSSH.
|
