5 ms·

No software can be quaranteed to be bug-free. And Heartbleed bug was in the extension, not in the core software. > (citation needed, btw) Not really. But if

by nicce 4y ago

No software can be quaranteed to be bug-free. And Heartbleed bug was in the extension, not in the core software. > (citation needed, btw) Not really. But if you insist, OpenSSL is defacto crypto library [1] , at least on server side. Browsers and OpenSSL takes the most burden for securing every-day use of internet in the world. There are billions testers every day. [1] : https://crocs.fi.muni.cz/public/papers/acsac2017 https://crocs.fi.muni.cz/public/papers/acsac2017)

naasking 4y ago
> No software can be quaranteed to be bug-free. Sure, this is done all the time via verification and other formal methods. It's not common in the industry, but not entirely uncommon either.
- ranger_danger 4y ago
  got any examples of this being used in popular FOSS software?
  - naasking 4y ago
    Depends what you mean by "popular". seL4 [1] is formally verified, open source and is used as baseband firmware in millions of phones, among other uses. Google just recently started an embedded OS based on it as well. CompCert [2] is a formally verified optimizing C compiler. Most formal verification happens in compilers or low-level mission critical systems due to the cost. If you want to write some formally verified C, you can check out Frama-C [3]. [1] https://sel4.systems/ https://sel4.systems/ [2] https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert [3] https://frama-c.com/ https://frama-c.com/
    - ranger_danger 4y ago
      >all the time >not common >the cost That's what I thought... and seL4 was the only one I could think of as well. I always see arguments around auditing as well but I think realistically unless a project has some enormous resources capable of funding this things themselves, you can't expect it to happen, but so many people poo-poo projects simply because it's "not audited", but to me that's silly because 1. most projects can't afford that, 2. who gets to say what has been audited "well enough", and 3. auditing results are only valid for specific snapshots of a repo and are completely invalidated as soon as any new changes are made.
      - naasking 4y ago
        It does happen all the time in commercial contexts in certain industries. Look up Spark Ada for lots of commercials applications.
- mh7 4y ago
  Nope, not even formal proofs can save you, see WPA2/KRACK. Using proofs just shifts the bugs into the assumptions/axioms (i.e you think your proof is proving X but it's actually proving Y)
vlovich123 4y ago
Given the lack of mention in the paper, I suspect they’re unable to distinguish OpenSSL from its forks, notably BoringSSL. OpenSSL might be used in an offline mode but I don’t think anyone really trusts it for online these days.
- nicce 4y ago
  BoringSSL is more for client side tbf. It was built for Chromium. It is not recommended to use for general parties, even Google does not recommend.
  - rockwotj 4y ago
    It was not built for chromium AFAIK To quote: https://boringssl.googlesource.com/boringssl/ https://boringssl.googlesource.com/boringssl/ BoringSSL arose because Google used OpenSSL for many years in various ways and, over time, built up a large number of patches that were maintained while tracking upstream OpenSSL. As Google's product portfolio became more complex, more copies of OpenSSL sprung up and the effort involved in maintaining all these patches in multiple places was growing steadily. Currently BoringSSL is the SSL library in Chrome/Chromium, Android (but it's not part of the NDK) and a number of other apps/programs.
  - vlovich123 4y ago
    Can you clarify how you came to this conclusion? No idea about self-hosted stuff of course, but I'm pretty sure BoringSSL is one of the gold standards for the big cloud providers. Counterpoints: > Encryption Implemented in the Google Front End for Google Cloud Services and Implemented in the BoringSSL Cryptographic Library https://cloud.google.com/docs/security/encryption-in-transit https://cloud.google.com/docs/security/encryption-in-transit > We use a common cryptographic library, Tink, which includes our FIPS 140-2 validated module (named BoringCrypto) to implement encryption consistently across Google Cloud https://cloud.google.com/docs/security/encryption/default-encryption https://cloud.google.com/docs/security/encryption/default-en... > It may (or may not!) come as surprise, but a few months ago we migrated Cloudflare’s edge SSL connection termination stack to use BoringSSL: Google's crypto and SSL implementation that started as a fork of OpenSSL. https://blog.cloudflare.com/make-ssl-boring-again/ https://blog.cloudflare.com/make-ssl-boring-again/ > We ported our SMTP server to use BoringSSL, Cloudflare’s SSL/TLS implementation of choice https://blog.cloudflare.com/email-routing-leaves-beta/ https://blog.cloudflare.com/email-routing-leaves-beta/ > We are pleased to announce the availability of s2n-quic, an open-source Rust implementation of the QUIC protocol added to our set of AWS encryption open-source libraries. <snip> AWS-LC is a general-purpose cryptographic library maintained by AWS which originated from the Google project BoringSSL. https://aws.amazon.com/blogs/security/introducing-s2n-quic-open-source-protocol-rust/ https://aws.amazon.com/blogs/security/introducing-s2n-quic-o... This last one is not 100% clear but I would imagine AWS dogfoods their own encryption libraries to build their internal cloud stack.

by nicce 4y ago

naasking 4y ago

> No software can be quaranteed to be bug-free. Sure, this is done all the time via verification and other formal methods. It's not common in the industry, but not entirely uncommon either.

ranger_danger 4y ago
got any examples of this being used in popular FOSS software?
- naasking 4y ago
  Depends what you mean by "popular". seL4 [1] is formally verified, open source and is used as baseband firmware in millions of phones, among other uses. Google just recently started an embedded OS based on it as well. CompCert [2] is a formally verified optimizing C compiler. Most formal verification happens in compilers or low-level mission critical systems due to the cost. If you want to write some formally verified C, you can check out Frama-C [3]. [1] https://sel4.systems/ https://sel4.systems/ [2] https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert [3] https://frama-c.com/ https://frama-c.com/
  - ranger_danger 4y ago
    >all the time >not common >the cost That's what I thought... and seL4 was the only one I could think of as well. I always see arguments around auditing as well but I think realistically unless a project has some enormous resources capable of funding this things themselves, you can't expect it to happen, but so many people poo-poo projects simply because it's "not audited", but to me that's silly because 1. most projects can't afford that, 2. who gets to say what has been audited "well enough", and 3. auditing results are only valid for specific snapshots of a repo and are completely invalidated as soon as any new changes are made.
    - naasking 4y ago
      It does happen all the time in commercial contexts in certain industries. Look up Spark Ada for lots of commercials applications.
mh7 4y ago
Nope, not even formal proofs can save you, see WPA2/KRACK. Using proofs just shifts the bugs into the assumptions/axioms (i.e you think your proof is proving X but it's actually proving Y)

vlovich123 4y ago

Given the lack of mention in the paper, I suspect they’re unable to distinguish OpenSSL from its forks, notably BoringSSL. OpenSSL might be used in an offline mode but I don’t think anyone really trusts it for online these days.

nicce 4y ago
BoringSSL is more for client side tbf. It was built for Chromium. It is not recommended to use for general parties, even Google does not recommend.
- rockwotj 4y ago
  It was not built for chromium AFAIK To quote: https://boringssl.googlesource.com/boringssl/ https://boringssl.googlesource.com/boringssl/ BoringSSL arose because Google used OpenSSL for many years in various ways and, over time, built up a large number of patches that were maintained while tracking upstream OpenSSL. As Google's product portfolio became more complex, more copies of OpenSSL sprung up and the effort involved in maintaining all these patches in multiple places was growing steadily. Currently BoringSSL is the SSL library in Chrome/Chromium, Android (but it's not part of the NDK) and a number of other apps/programs.
- vlovich123 4y ago
  Can you clarify how you came to this conclusion? No idea about self-hosted stuff of course, but I'm pretty sure BoringSSL is one of the gold standards for the big cloud providers. Counterpoints: > Encryption Implemented in the Google Front End for Google Cloud Services and Implemented in the BoringSSL Cryptographic Library https://cloud.google.com/docs/security/encryption-in-transit https://cloud.google.com/docs/security/encryption-in-transit > We use a common cryptographic library, Tink, which includes our FIPS 140-2 validated module (named BoringCrypto) to implement encryption consistently across Google Cloud https://cloud.google.com/docs/security/encryption/default-encryption https://cloud.google.com/docs/security/encryption/default-en... > It may (or may not!) come as surprise, but a few months ago we migrated Cloudflare’s edge SSL connection termination stack to use BoringSSL: Google's crypto and SSL implementation that started as a fork of OpenSSL. https://blog.cloudflare.com/make-ssl-boring-again/ https://blog.cloudflare.com/make-ssl-boring-again/ > We ported our SMTP server to use BoringSSL, Cloudflare’s SSL/TLS implementation of choice https://blog.cloudflare.com/email-routing-leaves-beta/ https://blog.cloudflare.com/email-routing-leaves-beta/ > We are pleased to announce the availability of s2n-quic, an open-source Rust implementation of the QUIC protocol added to our set of AWS encryption open-source libraries. <snip> AWS-LC is a general-purpose cryptographic library maintained by AWS which originated from the Google project BoringSSL. https://aws.amazon.com/blogs/security/introducing-s2n-quic-open-source-protocol-rust/ https://aws.amazon.com/blogs/security/introducing-s2n-quic-o... This last one is not 100% clear but I would imagine AWS dogfoods their own encryption libraries to build their internal cloud stack.