3 ms·

Rustls is still not formally verified. It may not have memory errors, but there are a lot of other security errors besides just that (and there may be more of t

by zelly 5y ago

Rustls is still not formally verified. It may not have memory errors, but there are a lot of other security errors besides just that (and there may be more of them since it hasn't been used as much as open|boringssl has been used). It's a slight improvement at best. Ideally you want a formally verified SPARK or CompCert C implementation of TLS, but those are not open sores compilers so they won't fly.

nine_k 5y ago
Indeed — unless it's built from source by a compiler I can trust (and also build from source), what security guarantees may it offer? Having a SPARK-verified version would of course be great anyway.
staticassertion 5y ago
> It's a slight improvement at best. That's a hefty judgment. If we look at major attacks on TLS endpoints I'd summarize them as, in order,: 1. Memory safety 2. Weak / old configurations 3. Invalid state machine transitions Rustls addresses all 3 of those, or at least it attempts to. (1) is obvious - it's rust. (2) rustls only supports the subset of TLS versions that are considered safe. (3) rustls avoids issues like gotofail and smacktls by encoding state machines as types, turning invalid state transitions into type failures. Plus, the actual crypto primitives are extremely well tested and built off of other existing libraries. So yeah, maybe some aspect of the crypto is incorrect, but, while interesting from an academic perspective, the real world ranks those other 3 things as way more important.
- smitherfield 5y ago
  That's if you look at major PUBLICIZED attacks on TLS endpoints. It's quite plausible that the people who've found (i.e. are looking for) attacks based on incorrect crypto aren't publicizing them.
  - staticassertion 5y ago
    Sure, but there's no evidence of that.
    - smitherfield 5y ago
      No evidence? We know for a fact that US, Russian, Chinese, British, Israeli etc. intelligence agencies are looking for crypto vulnerabilities, and we know for a fact that they do not publicize the vulnerabilities they find.
      - staticassertion 5y ago
        Yes, I'm aware of many, many people looking for crypto vulnerabilities. I'm not aware of many exploits in the wild.
- zelly 5y ago
  https://www.openssl.org/news/vulnerabilities.html https://www.openssl.org/news/vulnerabilities.html Half of these are caused by C problems not present in Rust like: null pointer errors, buffer overflows, integer overflows. The rest are logic errors (e.g., parsing errors) or crypto vulnerabilities (e.g., side channel attacks). There's nothing about Rust that magically prevents these errors. These vulnerabilities are discovered through testing and more importantly real world usage. Rustls has not been used nearly as much as or as long as openssl, so critical bugs could be in Rustls. You could encode some logic in the type system, but the types are still code that have to be tested. It's not a formal proof. It could still be wrong. It depends on your threat model and your risk tolerance whether you want to depend on relatively unvetted code.
  - staticassertion 5y ago
    I'm just going by publicized, real world attacks, which I think fall under the 3 categories I listed. > These vulnerabilities are discovered through testing and more importantly real world usage. FWIW I disagree that real world usage is necessarily more important. It is quite important, but at the same time the real world usage isn't going to hit all sorts of weird quirky paths. By contrast, Rustls has 97% line coverage, OpenSSL has ~65%. Of course, coverage isn't everything, but that's notable. > It's not a formal proof. It could still be wrong. So long as the type system is sound, I'm not sure this is true. If you embed a state machine into your type system your type system guarantees that the state machine executes as defined. Granted this is not checking against an external model. I will say that rustls still will benefit from wider adoption and more evaluation but imo it addresses the largest concerns today.
floatboth 5y ago
CompCert is a verified compiler – as in the compiler itself won't silently miscompile your code. It has nothing to do with verifying your C code. For that, other tools can be used (e.g. Frama-C Wp). One verified TLS implementation is miTLS, written in F*.

by zelly 5y ago

nine_k 5y ago

Indeed — unless it's built from source by a compiler I can trust (and also build from source), what security guarantees may it offer? Having a SPARK-verified version would of course be great anyway.

staticassertion 5y ago

> It's a slight improvement at best. That's a hefty judgment. If we look at major attacks on TLS endpoints I'd summarize them as, in order,: 1. Memory safety 2. Weak / old configurations 3. Invalid state machine transitions Rustls addresses all 3 of those, or at least it attempts to. (1) is obvious - it's rust. (2) rustls only supports the subset of TLS versions that are considered safe. (3) rustls avoids issues like gotofail and smacktls by encoding state machines as types, turning invalid state transitions into type failures. Plus, the actual crypto primitives are extremely well tested and built off of other existing libraries. So yeah, maybe some aspect of the crypto is incorrect, but, while interesting from an academic perspective, the real world ranks those other 3 things as way more important.

smitherfield 5y ago
That's if you look at major PUBLICIZED attacks on TLS endpoints. It's quite plausible that the people who've found (i.e. are looking for) attacks based on incorrect crypto aren't publicizing them.
- staticassertion 5y ago
  Sure, but there's no evidence of that.
  - smitherfield 5y ago
    No evidence? We know for a fact that US, Russian, Chinese, British, Israeli etc. intelligence agencies are looking for crypto vulnerabilities, and we know for a fact that they do not publicize the vulnerabilities they find.
    - staticassertion 5y ago
      Yes, I'm aware of many, many people looking for crypto vulnerabilities. I'm not aware of many exploits in the wild.
zelly 5y ago
https://www.openssl.org/news/vulnerabilities.html https://www.openssl.org/news/vulnerabilities.html Half of these are caused by C problems not present in Rust like: null pointer errors, buffer overflows, integer overflows. The rest are logic errors (e.g., parsing errors) or crypto vulnerabilities (e.g., side channel attacks). There's nothing about Rust that magically prevents these errors. These vulnerabilities are discovered through testing and more importantly real world usage. Rustls has not been used nearly as much as or as long as openssl, so critical bugs could be in Rustls. You could encode some logic in the type system, but the types are still code that have to be tested. It's not a formal proof. It could still be wrong. It depends on your threat model and your risk tolerance whether you want to depend on relatively unvetted code.
- staticassertion 5y ago
  I'm just going by publicized, real world attacks, which I think fall under the 3 categories I listed. > These vulnerabilities are discovered through testing and more importantly real world usage. FWIW I disagree that real world usage is necessarily more important. It is quite important, but at the same time the real world usage isn't going to hit all sorts of weird quirky paths. By contrast, Rustls has 97% line coverage, OpenSSL has ~65%. Of course, coverage isn't everything, but that's notable. > It's not a formal proof. It could still be wrong. So long as the type system is sound, I'm not sure this is true. If you embed a state machine into your type system your type system guarantees that the state machine executes as defined. Granted this is not checking against an external model. I will say that rustls still will benefit from wider adoption and more evaluation but imo it addresses the largest concerns today.

floatboth 5y ago

CompCert is a verified compiler – as in the compiler itself won't silently miscompile your code. It has nothing to do with verifying your C code. For that, other tools can be used (e.g. Frama-C Wp). One verified TLS implementation is miTLS, written in F*.