Not-Quite-So-Broken TLS / Aug 2015
Paper on rebuilding TLS securely but practically at USENIX Security 2015, presented with David Kaloper-Mersinjak, Hannes Mehnert and Peter Sewell. Not-Quite-So-Broken TLS was a from-scratch implementation in OCaml that served dual roles: both an executable specification for testing other TLS implementations and a production-ready library. By using a memory-safe language and modular design, we excluded entire classes of security vulnerabilities by construction. The implementation achieved reasonable performance (73-84% of OpenSSL throughput) despite the safety guarantees, and could be compiled into tiny Xen unikernels with a 4% TCB compared to Linux/OpenSSL stacks.