Not Quite So Broken Software

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.

You can read more in the papers below, or at the main homepage.

Recent Activity

: A Busy Week - Multicore, Releases, Interns and Visitors
: OCaml Inside: a drop-in replacement for libtls
: Conex: Establishing trust into data repositories
: Not-quite-so-broken TLS 1.3 mechanised conformance checking
: Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation
: Transport Layer Security purely in OCaml
: Not-So-Broken TLS: Re-engineering TLS in a Purely Functional Setting
: MirageOS: Leaving Legacy Behind: A Clean-Slate Approach to Operating Systems
: Safe TLS Stack Work
: Designing Secure Services with Unikernels: A Tough Nut to Crack
: Not-Quite-So-Broken TLS: Lessons in Re-engineering a Security Protocol Specification and Implementation
: Trustworthy Secure Modular Operating System Engineering
: MirageOS and OCaml-TLS: Fun Operating System Engineering