4 ms·

Comments on a Formal Verification of PolarSSL

49 points by jeffreyrogers 11y ago

diafygi 11y ago
> If we don’t want UBs, why not just use a TLS written in Java or C# or some other safe language? Of course that’s a fine idea! But we’ll have to somehow shoehorn a Java runtime onto those embedded processors with ~64 KB of RAM where PolarSSL / mbed TLS run. Would this be a good use case for Rust? Are there any Rust TLS projects that are credible?
- aroch 11y ago
  A couple people have attempted re-implementations of OpenSSL's TLS functions (with API compat) in Rust. As far as I know, all of these are stalled / abandoned. It is too hard for one individual to do it, especially when that individual isn't a security pro. Mostly Rust uses libraries that wrap OpenSSL and attempt to do some verification of "safeness" before passing to OpenSSL
  - viraptor 11y ago
    I don't think that anyone (unless it's a sponsored team effort) will implement tls in Rust for a long time. At least not as pure-rust library. Before you even touch the tls layer you need: asn1, x509, crypto, network libs. Out of those, only crypto and network libs exist and are fairly young. Asn1 and x509 are slightly insane and will require months of development on their own. (and that's before you even get into useful extensions everyone wants, like ocsp) What's good though is that someone writing pure-rust-tls in a year or two can start with implementation that ignores anything below TLS1.2 and save a lot of code and scope for errors that way.
    - aroch 11y ago
      I once looked at making a toy ASN.1 parser for project...and quickly decided my time and sanity were best spent elsewhere
- xorcist 11y ago
  I find that comment amusing. Wasn't it Tomcat or some other high profile Java project that exhibited behaviour with security implications identical with Heartbleed, shortly after?
  - wolf550e 11y ago
    Do you means this? https://www.smacktls.com/#skip https://www.smacktls.com/#skip
tptacek 11y ago
My advice hasn't changed in the last few years: avoid the idiosyncratic TLS libraries, and stick with OpenSSL / BoringSSL / LibreSSL. Libraries like PolarSSL are (somewhat) less likely to have the simple memory corruption bugs that OpenSSL has had, but more likely to have crypto flaws.
- jly 11y ago
  I don't disagree with you, but mbed TLS and other similar libraries partly exist to solve the need for high-quality crypto/TLS in very small operating environments, where it may not be possible or easy to use OpenSSL. They are designed to be highly modular and lightweight, and easy to integrate custom crypto acceleration hardware. I don't know enough about OpenSSL to say whether it's easy to work with in these environments, but this is why these idiosyncratic libraries exist, and it may not be as simple as 'just use OpenSSL' in all cases, especially for the non-TLS crypto parts.
  - richm44 11y ago
    Last time I checked mbed TLS omitted lots of pretty critical functionality such as certificate verification to the user - this stuff is far from trivial and is a core component of the MITM protection.
- ploxiln 11y ago
  It seems like the common safe crypto expert suggestion of deferring to authority is a bit of a philosophical problem. Deferring to authority is how everyone got into this SSL/TLS/openssl mess! I guess it's what you have to do to make sure less skilled/experienced developers do the least-stupid thing they might do when it comes to crypto, but on the other hand, to not be on an openssl-emergency treadmill for the past few years, there's no alternative to being a very sharp and independent developer who uses something niche but quite well made like polarssl, or finally decides to attack the openssl codebase like the openbsd developers have done (and since you suggest their work, you must have confidence that they won't fk it up.)
- deathanatos 11y ago
  Respectfully, I understand why you give this advice — and it isn't bad advice — implementing crypto correctly is difficult. But OpenSSL, in particular, has not and is not serving the engineering community well. The defaults are insecure. The bugs are horrendous. The API and tools border on unusable. I would really like to see a crypto library with a good API; I also believe Rust would make a much better language to implement a crypto library in than C, and would serve the community better in the long run. If one agrees that this is the case (a better library needs to be built), then at some point, that project must get underway. While I understand why the rule "crypto is hard. Don't implement your own." exists, at some point someone must break it, no? How should someone go about doing that? Who should go about doing that, since it seems like no matter how much I learn, "don't implement your own crypto"[1] will always apply? Otherwise, we're stuck here with OpenSSL, unable to do anything about it — no? Of course, any new crypto library must fall in the "idiosyncratic" category; perhaps asked differently is there anything a new library could do to earn trust of people like yourself, and gain better acceptance? (e.g., tests?, though I do know that unit tests are not a proof of correctness in implementation.) [1] and by "don't implement your own", I mean exclusively implementing the current state of the art algorithms, such as SHA2, AES, RSA, etc. I do not mean inventing your own algorithms, which is a whole other breed of crazy.

49 points by jeffreyrogers 11y ago

> If we don’t want UBs, why not just use a TLS written in Java or C# or some other safe language? Of course that’s a fine idea! But we’ll have to somehow shoehorn a Java runtime onto those embedded processors with ~64 KB of RAM where PolarSSL / mbed TLS run. Would this be a good use case for Rust? Are there any Rust TLS projects that are credible?

aroch 11y ago
A couple people have attempted re-implementations of OpenSSL's TLS functions (with API compat) in Rust. As far as I know, all of these are stalled / abandoned. It is too hard for one individual to do it, especially when that individual isn't a security pro. Mostly Rust uses libraries that wrap OpenSSL and attempt to do some verification of "safeness" before passing to OpenSSL
- viraptor 11y ago
  I don't think that anyone (unless it's a sponsored team effort) will implement tls in Rust for a long time. At least not as pure-rust library. Before you even touch the tls layer you need: asn1, x509, crypto, network libs. Out of those, only crypto and network libs exist and are fairly young. Asn1 and x509 are slightly insane and will require months of development on their own. (and that's before you even get into useful extensions everyone wants, like ocsp) What's good though is that someone writing pure-rust-tls in a year or two can start with implementation that ignores anything below TLS1.2 and save a lot of code and scope for errors that way.
  - aroch 11y ago
    I once looked at making a toy ASN.1 parser for project...and quickly decided my time and sanity were best spent elsewhere
xorcist 11y ago
I find that comment amusing. Wasn't it Tomcat or some other high profile Java project that exhibited behaviour with security implications identical with Heartbleed, shortly after?
- wolf550e 11y ago
  Do you means this? https://www.smacktls.com/#skip https://www.smacktls.com/#skip

tptacek 11y ago

My advice hasn't changed in the last few years: avoid the idiosyncratic TLS libraries, and stick with OpenSSL / BoringSSL / LibreSSL. Libraries like PolarSSL are (somewhat) less likely to have the simple memory corruption bugs that OpenSSL has had, but more likely to have crypto flaws.

jly 11y ago
I don't disagree with you, but mbed TLS and other similar libraries partly exist to solve the need for high-quality crypto/TLS in very small operating environments, where it may not be possible or easy to use OpenSSL. They are designed to be highly modular and lightweight, and easy to integrate custom crypto acceleration hardware. I don't know enough about OpenSSL to say whether it's easy to work with in these environments, but this is why these idiosyncratic libraries exist, and it may not be as simple as 'just use OpenSSL' in all cases, especially for the non-TLS crypto parts.
- richm44 11y ago
  Last time I checked mbed TLS omitted lots of pretty critical functionality such as certificate verification to the user - this stuff is far from trivial and is a core component of the MITM protection.
ploxiln 11y ago
It seems like the common safe crypto expert suggestion of deferring to authority is a bit of a philosophical problem. Deferring to authority is how everyone got into this SSL/TLS/openssl mess! I guess it's what you have to do to make sure less skilled/experienced developers do the least-stupid thing they might do when it comes to crypto, but on the other hand, to not be on an openssl-emergency treadmill for the past few years, there's no alternative to being a very sharp and independent developer who uses something niche but quite well made like polarssl, or finally decides to attack the openssl codebase like the openbsd developers have done (and since you suggest their work, you must have confidence that they won't fk it up.)
deathanatos 11y ago
Respectfully, I understand why you give this advice — and it isn't bad advice — implementing crypto correctly is difficult. But OpenSSL, in particular, has not and is not serving the engineering community well. The defaults are insecure. The bugs are horrendous. The API and tools border on unusable. I would really like to see a crypto library with a good API; I also believe Rust would make a much better language to implement a crypto library in than C, and would serve the community better in the long run. If one agrees that this is the case (a better library needs to be built), then at some point, that project must get underway. While I understand why the rule "crypto is hard. Don't implement your own." exists, at some point someone must break it, no? How should someone go about doing that? Who should go about doing that, since it seems like no matter how much I learn, "don't implement your own crypto"[1] will always apply? Otherwise, we're stuck here with OpenSSL, unable to do anything about it — no? Of course, any new crypto library must fall in the "idiosyncratic" category; perhaps asked differently is there anything a new library could do to earn trust of people like yourself, and gain better acceptance? (e.g., tests?, though I do know that unit tests are not a proof of correctness in implementation.) [1] and by "don't implement your own", I mean exclusively implementing the current state of the art algorithms, such as SHA2, AES, RSA, etc. I do not mean inventing your own algorithms, which is a whole other breed of crazy.