4 ms·

> The basic idea is that vulnerabilities in cryptography require a different set of skills to find than "regular" security vulnerabilities do That may be true

by snaky 8y ago

> The basic idea is that vulnerabilities in cryptography require a different set of skills to find than "regular" security vulnerabilities do That may be true for traditional low-level hand-optimized implementations. But if we consider the trend is clearly toward the high-level proof-based code[1], which is way easier to audit, then open source is obviously better. [1] "Simple High-Level Code For Cryptographic Arithmetic - With Proofs, Without Compromises" https://deepspec.org/entry/Paper/Simple+High.2DLevel+Code+For+Cryptographic+Arithmetic+.2D.2D+With+Proofs.2C+Without+Compromises https://deepspec.org/entry/Paper/Simple+High.2DLevel+Code+Fo...

blattimwind 8y ago
Most issues (apart from legacy asymmetric primitives) are actually either in the implementation (common in widely deployed software) or the design (even more common in widely deployed software) of higher level protocols. Many implementations issues in crypto code are just regular code bugs. Meanwhile, design issues are not so readily apparent. There is no linter that will tell you that using the same AES key for years and keeping a block counter in an untrusted location is a bad idea. And if you make your code obscure enough ("abstract" in all the wrong ways), then people will have a really hard time figuring stuff like this out. And no one does proofs on protocol implementations in practice. Yes, there are some. Yes, there has been some progress to apply it to e.g. OpenSSL — after everyone has been using it for critical infrastructure for decades — so there's like, literally, one practical implementation that has seen a sliver of formal verification.
- nickpsecurity 8y ago
  There's tooling like Cryptol and SPARK to make this a lot easier than it was in the past. Cryptol can generate software or hardware that implements the high-level spec of the algorithm. Far as practical use, certainly not just one even though still extremely rare. Here's some more: Altran/Praxis Correct-by-Construction for a cert authority http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruction.pdf http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruct... Same company ports Skein from C to SPARK, finds trouble http://www.skein-hash.info/sites/default/files/SPARKSkein.pdf http://www.skein-hash.info/sites/default/files/SPARKSkein.pd... SPARK Ada is available under GPL and commercial licenses. The book below is quite easy to read compared to most stuff with formal methods. The companies building stuff like this usually also have tools to generate tests (property-based testing) from contracts/specs and can automatically turn anything you can't prove into runtime checks. Shocked it's not used more often in areas like smart contracts or cryptocurrency protocols. https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842/ref=sr_1_1?ie=UTF8&qid=1538687861&sr=8-1&keywords=high+integrity+applications https://www.amazon.com/Building-High-Integrity-Applications-... Galois built Cryptol for NSA but open sourced it. https://www.cryptol.net/ https://www.cryptol.net/ Rockwell Collins built SHADE and some other tools for high-assurance crypto. They build stuff for the defense sector mainly funded by NSA. They even have a separation-preserving, verified CPU. http://www.csl.sri.com/users/shankar/VGC05/Hardin.pdf http://www.csl.sri.com/users/shankar/VGC05/Hardin.pdf
tptacek 8y ago
There aren't that many people in the world that could build and use a Tamarin model for a crypto protocol, let alone prove it formally. Proof-driven cryptographic engineering is even more specialized than standard cryptographic engineering.
IncRnd 8y ago
> But if we consider the trend is clearly toward the high-level proof-based code[1], which is way easier to audit, then open source is obviously better. You disprove your own assertion. Cryptography is very specialized. All specializations in this world require specialized knowledge and niche experience, cryptography included. Assumptions about the obviousness of a specialization is almost itself the definition of an error.

by snaky 8y ago

blattimwind 8y ago

Most issues (apart from legacy asymmetric primitives) are actually either in the implementation (common in widely deployed software) or the design (even more common in widely deployed software) of higher level protocols. Many implementations issues in crypto code are just regular code bugs. Meanwhile, design issues are not so readily apparent. There is no linter that will tell you that using the same AES key for years and keeping a block counter in an untrusted location is a bad idea. And if you make your code obscure enough ("abstract" in all the wrong ways), then people will have a really hard time figuring stuff like this out. And no one does proofs on protocol implementations in practice. Yes, there are some. Yes, there has been some progress to apply it to e.g. OpenSSL — after everyone has been using it for critical infrastructure for decades — so there's like, literally, one practical implementation that has seen a sliver of formal verification.

nickpsecurity 8y ago
There's tooling like Cryptol and SPARK to make this a lot easier than it was in the past. Cryptol can generate software or hardware that implements the high-level spec of the algorithm. Far as practical use, certainly not just one even though still extremely rare. Here's some more: Altran/Praxis Correct-by-Construction for a cert authority http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruction.pdf http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruct... Same company ports Skein from C to SPARK, finds trouble http://www.skein-hash.info/sites/default/files/SPARKSkein.pdf http://www.skein-hash.info/sites/default/files/SPARKSkein.pd... SPARK Ada is available under GPL and commercial licenses. The book below is quite easy to read compared to most stuff with formal methods. The companies building stuff like this usually also have tools to generate tests (property-based testing) from contracts/specs and can automatically turn anything you can't prove into runtime checks. Shocked it's not used more often in areas like smart contracts or cryptocurrency protocols. https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842/ref=sr_1_1?ie=UTF8&qid=1538687861&sr=8-1&keywords=high+integrity+applications https://www.amazon.com/Building-High-Integrity-Applications-... Galois built Cryptol for NSA but open sourced it. https://www.cryptol.net/ https://www.cryptol.net/ Rockwell Collins built SHADE and some other tools for high-assurance crypto. They build stuff for the defense sector mainly funded by NSA. They even have a separation-preserving, verified CPU. http://www.csl.sri.com/users/shankar/VGC05/Hardin.pdf http://www.csl.sri.com/users/shankar/VGC05/Hardin.pdf

tptacek 8y ago

There aren't that many people in the world that could build and use a Tamarin model for a crypto protocol, let alone prove it formally. Proof-driven cryptographic engineering is even more specialized than standard cryptographic engineering.

IncRnd 8y ago

> But if we consider the trend is clearly toward the high-level proof-based code[1], which is way easier to audit, then open source is obviously better. You disprove your own assertion. Cryptography is very specialized. All specializations in this world require specialized knowledge and niche experience, cryptography included. Assumptions about the obviousness of a specialization is almost itself the definition of an error.