Not quite so broken
Protocol implementations have lots of security flaws. The immediate causes of these are often programming errors, e.g. in memory management, but the root causes are more fundamental: the challenges of interpreting the ambiguous prose specification (RFCs), the complexities inherent in large APIs and code bases, inherently unsafe programming choices, and the impossibility of directly testing conformance between implementations and the specification.
Not-quite-so-broken is the theme of our re-engineered approach to security protocol specification and implementation that addresses these root causes. The same code serves two roles: it is both a specification, executable as a test oracle to check conformance of traces from arbitrary implementations, and a usable implementation; a modular and declarative programming style provides clean separation between its components. Many security flaws are thus excluded by construction.
Read more in our paper: Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation by David Kaloper-Meršinjak, Hannes Mehnert, Anil Madhavapeddy and Peter Sewell, published at Usenix Security 2015. We implemented some libraries in OCaml using this approach:
- TLS (API documentation), the most widely used security protocol on the Internet (
- X.509 (API documentation)certificate handling (including public and private RSA keys (PKCS8), certificate signing requests (PKCS10))
- ASN.1 parser and unparser combinators
- nocrypto (API documentation) underlying cryptographic primitives (symmetric: 3DES, AES; hash: MD5, SHA 1, SHA 2; asymmetric: DH, DSA, RSA; CSPRNG: Fortuna; ECB/CBC/CCM/GCM modes)
- OTR (API documentation), the Off-the-record protocol
Code using nqsb:
- MirageOS, a library operating system
- BTC Piñata, our bitcoin bait
- TLS handshake visualisation, our interactive visualisation
- tlstunnel, an application handling TLS, forwarding the plaintext to another service via TCP
- tlstools, some TLS utilities
- certify, an application to generate certificates, certificate signing requests, and basic CA signing
- mirage-seal, an application which produces a stand-alone unikernel serving a directory via https
- tlsclient, a TLS client
- jackline, a terminal XMPP client using OTR and TLS
- pcap trace checker, which lets you validate recorded TLS sessions
Texts about nqsb:
- hannes blog: full stack engineer
- (paper) 2016-02-21 @TRON: Not-quite-so-broken TLS 1.3 Mechanised Conformance Checking
- (paper) 2015-08-10 @UsenixSecurity: Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation
- 2015-07-22: Organized chaos: managing randomness
- 2015-07-07: Easy HTTPS Unikernels with mirage-seal
- 2015-06-29: Reviewing the Bitcoin Pinata
- 2015-06-26: MirageOS v2.5 with full TLS support
- 2015-06-26: Why OCaml-TLS?
- 2015-02-10: Smash the Bitcoin Pinata for fun and profit! (Amir's post, MirageOS post, (german) Golem post)
- (video) 2014-12-27 @31c3: Trustworthy secure modular operating system engineering
- 2014-07-14: Protocol implementation and mitigations to known attacks
- 2014-07-11: ASN.1 and notation embedding
- 2014-07-10: Adventures in X.509 certificate parsing and validation
- 2014-07-09: Building the nocrypto library core
- 2014-07-08: Introducing transport layer security (TLS) in pure OCaml
Parts of this work were supported by REMS: Rigorous Engineering for Mainstream Systems EPSRC Programme Grant EP/K008528/1, and by the European Union’s Seventh Framework Programme FP7/2007–2013 under the User Centric Networking project (no. 611001).
Thanks to IPredator for hosting.