Finding security bugs on the road to creating a verifiably secure TLS lib

Microsoft, French bods push for mathematically provable bug-free code

Microsoft and French research organization Inria have jointly published the source code for a more secure implementation of TLS – a first step in hopefully increasing the security of millions online.

The software library emerged from a project called MiTLS, whose website is curiously missing in action at time of writing. Its GitHub account can be found here: there you'll find implementations of TLS written in F* and F7.

TLS is used worldwide to provide secure HTTPS connections for online banking and shopping, among many other things. The goal of MiTLS is to produce a TLS library that can be mathematically proven to work as intended, formally verified bug free – certainly free of the sorts of bugs that turn into security vulnerabilities in today's TLS software libraries, such as OpenSSL.

Work on the verifiable library led to the discovery of the Triple Handshake, Freak, and Logjam vulnerabilities in other TLS libraries, we're told.

"We did not find them because we were looking for attacks. We found them as a side effect,” said Cedric Fournet, a principal researcher at Microsoft Research Cambridge and one of the project's lead researchers, in a blog post.

Fournet told El Reg that the team expected to find small errors, but in the end unearthed more substantial flaws, something that came as a surprise.

While the MiTLS gang works towards creating a library that can be mathematically proven to be secure, the source code releases now are geared toward helping academic and security experts create their own bug-free implementations of TLS.

The project started off back in 2011 as a way to address the differences between the theoretical security models being created in research labs and the practical implementations of internet security. What initially started off as a six-month project was expanded into an open-ended research exercise.

The vulnerabilities the Microsoft/Inria team discovered along the way highlighted that many companies were using outdated cryptographic algorithms in their TLS implementations, leaving their customers more open to attack as a result. Fournet said that some avoided updating because upgrading to a new set of algorithms can be costly and time-consuming, and may result in elements of a system not working properly or running more slowly.

In addition, many fail to see the benefits of upgrading until a particular serious vulnerability in older technologies is exposed.

The MS/Inria joint research team is working closely with other security experts and academics also working to overhaul the TLS protocol, a combined effort led by the IETF that is scheduled to spawn the next version of the protocol sometime next year. The Snowden revelations of mass surveillance by Western intel agencies have pushed participants in the process to be "more ambitious" about the forthcoming revamp, according to Fournet. This has resulted in technologies such as Perfect Forward Secrecy getting pushed into TLS 1.3, for example.

The MS/Inria Centre brings together a total of 100 researchers comprising 40 permanent researchers from Inria, 30 permanent researchers from Microsoft Research, and 30 non-permanent researchers (interns, postdoctoral, and PhD students). Alongside security, other fields of research including machine learning and cloud computing are being studied. Workers are focused on fundamental, long-term research. ®

Similar topics

Other stories you might like

Biting the hand that feeds IT © 1998–2021