4 ms·
Cryptol is a nice tool, but it can't eliminate most important crypto bugs (for example, the sorts of bugs found in OpenSSL). It's useful for proving things abo
by hnhnhn3 11y ago
Cryptol is a nice tool, but it can't eliminate most important crypto bugs (for example, the sorts of bugs found in OpenSSL). It's useful for proving things about bit-mixy crypto code like AES, SHA, etc, but that code rarely has bugs (due to known-answer tests).
- nickpsecurity 11y agoWell, it actually shouldn't introduce most of the bugs you find in OpenSSL. Plus, you don't use it alone. It works like this: 1. Cryptographers come up with the algorithms and protocols with their mathematical proofs applied to their properties. 2. Someone uses tools like CRYPTOL for algorithms or AnBx for protocols to generate the code. http://www.dsi.unive.it/~modesti/anbx/ http://www.dsi.unive.it/~modesti/anbx/ 3. The code is run through visual inspections, static analysis tools like ASTREE or SPARK, tests, covert channel analysis, and so on. Modified if problems are found. 4. An optimizing version of a certified compiler like CompCert produces the object code. 5. It's distributed with public key cryptography and/or Merkle Signatures if people don't trust that. There's modern versions with efficient or unlimited signing. 6. Optionally, a subversion-resistant process builds the fist compiler and checkers in stages.
- hnhnhn3 11y agoYou can get a nice PLDI paper by following those steps!
- nickpsecurity 11y agoNever looked into it. Will do.