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

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 …

  1. Anonymous Coward
    Anonymous Coward

    Verity

    "The goal of MiTLS is to produce a TLS library that can be mathematically proven to work as intended, verified bug free..."

    Mathematical proof is 100% rigorous, whereas fixing bugs in software is (ahem) not.

    Do they mean "semi-mathematically proven"? What?

    1. Anonymous Coward
      Anonymous Coward

      Re: Verity

      They mean a verified implementation of a wilfully b0rked spec.

      Arse over tit, if you ask me. Which they didn't.

      Some people have too much time on their hands.

    2. Lee D Silver badge

      Re: Verity

      Mathematical proofs are perfect.

      However, what you are proving is what's important. Most times, you end up mathematically proving that your code fits a standard or performs a certain calculation without error, only to find that the standard/calculation is doing the wrong thing anyway. All you've then proved is that you are doing the wrong thing every time, compliant to the standard.

      As such, it's not a panacea. It's a long-winded, difficult, expensive process to show up the flaws in your standards, the result of which you can't DIRECTLY implement in "real" code anyway. And your production code produced from it, or even your compiler of that code, may well make assumptions or mistakes that you have no control over (e.g. whether it wraps bits, stores in big/little-endian, whether division is within a certain margin, etc. etc. etc.) that you didn't account for in the proof.

      So it's mathematically proven. But any possible real-world implementation of it will not be. And that doesn't mean that what you've proven is USEFUL or CORRECT in itself, just that it's the inevitable mathematical conclusion of the assumptions, calculations and possible data that you plugged into your proof.

  2. Anonymous Coward
    Anonymous Coward

    Mathematically proven to implement the given specification, which in turn has to be written in a formal way. Bugs in the formal spec will translate to bugs in the implementation.

    F7 language? Try doing it in F77 instead :-)

    1. Anonymous Coward
      Anonymous Coward

      Logically that just moves the bug problem over to the spec. What purpose does this serve?

      Does "verified bug free" just mean the code will match the spec, whatever that happens to be?

      1. Anonymous Coward
        Anonymous Coward

        Does "verified bug free" just mean the code will match the spec, whatever that happens to be?

        Yup. Sounds like a nice little project to keep them in an indefinite supply of pork & gravy, while NSA grinds along keeping their specs aheadish of the "discovered" vulnerabilities.

        TLS1.3... 1.4... 1.5... 1.6... 2... 2.1... ...38.3...

        Who said job security is a thing of the past?

      2. Ken Hagan Gold badge

        "What purpose does this serve?"

        According to the article, the process revealed three new vulnerabilities in the spec. That's what usually happens when you sit down to test something rigorously or prove its correctness formally. LibreSSL is (or soon will be) better because of this work.

        Whether or not you ever use the resulting implementation is irrelevant. Like the old saying about battle plans: the value lies in the act of making it, not in having it once the bullets are flying.

  3. cantankerous swineherd

    good and worthwhile work that can still be blown away by knaves and fools such as dell.

  4. JLV

    quality takes time and money

    This is really nice and good news.

    However, the cynic in me notes that, when a recent Reg forum discussed injecting formal engineering discipline into software development, some folks were all over formal methods and how they would do away with our amateurish and non-engineering worthy practices. "It's a solved problem, we have formal methods", is almost what some seemed to be claiming.

    Whatever the merits of formal methods are in this case, and I assume there are plenty, it would seem as if applying them took considerable resources and time in order to bring this project to fruition.

    I hope this serves as a timely reminder to both camps. Yes, formal methods can help. But, they also don't quite seem to be a universally applicable silver bullet at the current time. Unless, of course, everyone can afford a team of 70-100 engineers and PhDs for 4 years as an entry price. Seems there is some work left for the rest of us informal slhackers ;-)

    On the other hand, I really like the fact that they weeded out errors in existing libraries and can be used to do that in the future. This type of effort should be deployed more often on oft-reused core critical subsystems that have stable and detailed specs already.

  5. Richard Lloyd

    Why not work on an existing TLS project?

    So here we go again - another reinvention of the wheel :-( Surely it would be a better use of their time to work on improving an existing TLS Open Source project? OpenSSL and GnuTLS are both very obvious candidates (and probably the most popular ones out there) and while I can see they are providing some benefit to those by discovering possible flaws in them, working directly on them would be a superior solution surely?

    1. Anonymous Coward
      Anonymous Coward

      Re: Why not work on an existing TLS project?

      You're missing the point entirely. The Inria project is about translating the TLS specification into code that can be mathematically proven to implement that specification correctly. Given the tools we currently have for this type of proof, it would be virtually impossible to do with any real-world imperative language such as the C family of languages and needs to be done in a declarative language. Given the Microsoft involvement, the F family of languages was an obvious choice.

      1. Anonymous Coward
        Anonymous Coward

        Re: Why not work on an existing TLS project?

        > Given the tools we currently have for this type of proof, it would be virtually

        > impossible to do with any real-world imperative language such as the C family

        > of languages and needs to be done in a declarative language.

        That statement is verifiably false.

        The first time that I whitnesses such a proofing tool in action was in 1996 (the KIV system, the Karlsruhe Interactive Verifier) and that tool emitted running code as the result of the proofing

        process. The tool offered the programming languages C and C++ for code output.

  6. tony2heads

    Mathematically correct code

    I have heard of a few cases of this, but in none of them have I heard that the code will run within a reasonable time.

    1. Richard Simpson

      Re: Mathematically correct code

      Is this an issue in this case? Surely TLS execution time isn't a limiting factor in most internet transactions? Even if it ran at a fraction of the current speed, would that be a problem for most modern computers? Hmm, perhaps an issue at the server end. Presumably this scheme can't be extended into hardware crypto accelerators?

      Also, forgive my ignorance, but I thought that TLS was primarily used to achieve a secure key exchange for a traditional cipher which is then used to exchange the actual data. I get the impressions that this work isn't fiddling with the actual cipher code which will remain just as fast and/or buggy as now but I am ready to be corrected on this point.

    2. allthecoolshortnamesweretaken

      Re: Mathematically correct code

      Is that even possible, considering Gödel's theorems?

      (Maths end-user here, aka engineer... give me any formula and I'll run the numbers, but don't ask me to prove that 2+2=4)

      1. This post has been deleted by its author

      2. John H Woods Silver badge

        Re: Mathematically correct code

        "Is that even possible, considering Gödel's theorems?"

        -- allthecoolshortnamesweretaken

        It is and it isn't :-) You hit (for instance) the halting problem if you use a sufficiently expressive [1] language; then you cannot prove whether a program will halt or not. The key is to use a different type of language that is more amenable to mathematical proofs -- I'm inclined believe this is why they are starting fresh and not working on an existing library, but I'm no expert.

        [1] Most modern programming languages meet the criteria: if you have a language where you can (a) test the return result of a function and (b) deliberately create an infinite loop, you'll hit the halting problem. Imagine a program (P) which takes a piece of code and calls a function (F) which returns whether that piece of code will complete or just hang (e.g. in an infinite loop). So P invokes F on some code and (bear with me) if the return result of F indicates that the said code will complete (i.e. will not halt), P then goes (deliberately) into an infinite loop. Now, what happens if you run P on itself? Suddenly you have a paradox: the only conclusion is that it is not possible to create the function F in any language in which, given F, you could create P.

  7. PassiveSmoking

    Invisible features

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

    And the Titanic only needed 20 lifeboats until it was sinking.

    The problem with things like security is that they're invisible to the user, therefore it's normally very difficult to impossible to make a case to management for investing time and resources into improving security, until Bobby Tables has stolen your database and you're all over the news for the leak of 40,000 sets of credit card details you were responsible for.

    This attitude needs to change if any real progress is to be made. You can improve the TLS library all you want and it won't do any good if developers are not allowed to update the TLS libraries in their software because management want a cute song to play whenever a customer puts something in their basket.

    1. Donkey Molestor X

      Re: Invisible features

      or as motorcyclists say, "You dress for the crash, not for the ride."

  8. Anonymous Coward
    Anonymous Coward

    "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth

  9. anonymous boring coward Silver badge

    Verifiably?

    Good luck with that.

    It won't be a very large program/block-of-code, that's for sure.

  10. anonymous boring coward Silver badge

    And, BTW, are they also intending to mathematically prove the correctness and incorruptability of every library and OS function that the supposed TLS implementation may happen to call, in all scenarios, on all platforms, for all versions?

    At least they probably get some funding for this pie-in-the-sky academia.

    1. Donkey Molestor X

      it's cynics like you that make me happy you're working on some CRUD app and not designing a bridge or a ignition shaft detente. the term "software engineer" can't die soon enough for me.

  11. Alistair
    Windows

    Interesting.

    I would hope that their accounting books are as open source as their code will be............

  12. WebDev

    Formal verification is real

    Chiming in a bit late here. A lot of you seem not to have heard of formal verification methods before and are skeptical of them. It's actually quite valid and effective. You can definitely eliminate things like buffer overflows and memory leaks with it -- bugs that recur forever in typical C-based software.

    Formal verification is quite hard, and thus rare in industry (and in academia). There aren't great tools for it, and so a lot of development teams never look into it.

    A good example of formal verification in practice is the seL4 microkernel project. They lay out their proof and what it means here: http://sel4.systems/Info/FAQ/proof.pml

    A formally verified TLS library seems like a no-brainer, something I would've expected the US government to create several years ago. It's stunning that the industry and its customers have been willing to use unverified crypto libraries written in C, which guarantees insecurity. And that's what we see with OpenSSL – a neverending stream of critical vulnerabilities due to artifacts of C programming like buffer overflows. This is ludicrous – crypto libraries that are insecure? What's the point of that? Microsoft's effort is long overdue. We don't just need a provably secure TLS library – we need three or four of them.

POST COMMENT House rules

Not a member of The Register? Create a new account here.

  • Enter your comment

  • Add an icon

Anonymous cowards cannot choose their icon

Other stories you might like