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 mitls.org 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

Broader topics


Other stories you might like

  • How ICE became a $2.8b domestic surveillance agency
    Your US tax dollars at work

    The US Immigration and Customs Enforcement (ICE) agency has spent about $2.8 billion over the past 14 years on a massive surveillance "dragnet" that uses big data and facial-recognition technology to secretly spy on most Americans, according to a report from Georgetown Law's Center on Privacy and Technology.

    The research took two years and included "hundreds" of Freedom of Information Act requests, along with reviews of ICE's contracting and procurement records. It details how ICE surveillance spending jumped from about $71 million annually in 2008 to about $388 million per year as of 2021. The network it has purchased with this $2.8 billion means that "ICE now operates as a domestic surveillance agency" and its methods cross "legal and ethical lines," the report concludes.

    ICE did not respond to The Register's request for comment.

    Continue reading
  • Fully automated AI networks less than 5 years away, reckons Juniper CEO
    You robot kids, get off my LAN

    AI will completely automate the network within five years, Juniper CEO Rami Rahim boasted during the company’s Global Summit this week.

    “I truly believe that just as there is this need today for a self-driving automobile, the future is around a self-driving network where humans literally have to do nothing,” he said. “It's probably weird for people to hear the CEO of a networking company say that… but that's exactly what we should be wishing for.”

    Rahim believes AI-driven automation is the latest phase in computer networking’s evolution, which began with the rise of TCP/IP and the internet, was accelerated by faster and more efficient silicon, and then made manageable by advances in software.

    Continue reading
  • Pictured: Sagittarius A*, the supermassive black hole at the center of the Milky Way
    We speak to scientists involved in historic first snap – and no, this isn't the M87*

    Astronomers have captured a clear image of the gigantic supermassive black hole at the center of our galaxy for the first time.

    Sagittarius A*, or Sgr A* for short, is 27,000 light-years from Earth. Scientists knew for a while there was a mysterious object in the constellation of Sagittarius emitting strong radio waves, though it wasn't really discovered until the 1970s. Although astronomers managed to characterize some of the object's properties, experts weren't quite sure what exactly they were looking at.

    Years later, in 2020, the Nobel Prize in physics was awarded to a pair of scientists, who mathematically proved the object must be a supermassive black hole. Now, their work has been experimentally verified in the form of the first-ever snap of Sgr A*, captured by more than 300 researchers working across 80 institutions in the Event Horizon Telescope Collaboration. 

    Continue reading
  • Shopping for malware: $260 gets you a password stealer. $90 for a crypto-miner...
    We take a look at low, low subscription prices – not that we want to give anyone any ideas

    A Tor-hidden website dubbed the Eternity Project is offering a toolkit of malware, including ransomware, worms, and – coming soon – distributed denial-of-service programs, at low prices.

    According to researchers at cyber-intelligence outfit Cyble, the Eternity site's operators also have a channel on Telegram, where they provide videos detailing features and functions of the Windows malware. Once bought, it's up to the buyer how victims' computers are infected; we'll leave that to your imagination.

    The Telegram channel has about 500 subscribers, Team Cyble documented this week. Once someone decides to purchase of one or more of Eternity's malware components, they have the option to customize the final binary executable for whatever crimes they want to commit.

    Continue reading
  • Ukrainian crook jailed in US for selling thousands of stolen login credentials
    Touting info on 6,700 compromised systems will get you four years behind bars

    A Ukrainian man has been sentenced to four years in a US federal prison for selling on a dark-web marketplace stolen login credentials for more than 6,700 compromised servers.

    Glib Oleksandr Ivanov-Tolpintsev, 28, was arrested by Polish authorities in Korczowa, Poland, on October 3, 2020, and extradited to America. He pleaded guilty on February 22, and was sentenced on Thursday in a Florida federal district court. The court also ordered Ivanov-Tolpintsev, of Chernivtsi, Ukraine, to forfeit his ill-gotten gains of $82,648 from the credential theft scheme.

    The prosecution's documents [PDF] detail an unnamed, dark-web marketplace on which usernames and passwords along with personal data, including more than 330,000 dates of birth and social security numbers belonging to US residents, were bought and sold illegally.

    Continue reading

Biting the hand that feeds IT © 1998–2022