Does open-source cryptographic software work correctly? [pdf]
cr.yp.to
cr.yp.to
Another way to think like this is to approach testing using fuzzing, but in a way that is designed to have 100% coverage of invariants.
Basic fuzzing generates random inputs looking for a crash, without asserting invariants along the way. Invariant fuzzing, on the other hand, is concerned not just with the inputs to a function but also the outputs.
For example, if a function is expected to throw exceptions for bad inputs, then use invariant fuzzing to test that all exceptions are thrown for a variety of bad inputs. Writing an invariant fuzz test like this often takes less code than writing hundreds of unit tests, which have significantly less coverage.
Another example, and this is how we found CVE 2019-1543 in OpenSSL [1]. For all the AEAD ciphers in OpenSSL that we wanted to support, we fuzzed [2] and round-tripped various combinations of {key, iv, plaintext/ciphertext, aad, tag}, comparing against an independent interface, while also randomly corrupting bytes in {key, iv, ciphertext, aad, tag} to ensure that AEAD authenticity invariants were being kept by OpenSSL. We needed the "A"s in the AEADs so we tested them.
Adding this AEAD authenticity invariant test to our fuzz test took 25 lines of code and found the CVE in literally a second.
After the CVE was found, OpenSSL added a test vector. This was 8 lines of code, and tested authenticity only for a single test vector, without covering the entire range of IV lengths, which was the root of the issue that the CVE uncovered. All this effort, for little gain, when the whole spectrum could have been tested across a few thousand vectors in the same amount of code.
If you are interested in this kind of thing, Guido Vranken is taking the same approach to the next level for multiple crypto libraries [3].
[1]: https://nvd.nist.gov/vuln/detail/CVE-2019-1543
When it comes specifically to cryptography, I think formal verification should be added for increased confidence.
(I'm not saying "don't bother writing tests if you're using a strongly typed language" - these things can and should be be complementary)
As cool as Idris is, in my experience it has been quite buggy. I would suggest Agda or Coq instead which are more mature.
https://github.com/google/wycheproof is a Google's effort to test for known attacks. If your crypto library does not mention Project Wycheproof or known attacks listed there, ignore it.
For some bugs the probability of triggering them with 'random' inputs ends up being a something like 1:2^64 or worse... so there unit tests aren't necessarily helpful.
In libsecp256k1 we include tests generated from specially constructed distributions that are more likely to generate errors (which, for example, found bugs when run against openssl that had 1:2^256 level odds of being detected by uniform random tests), as well as test generated using absurd amounts of whitebox fuzzing and symbolic execution-- but even these levels of tests aren't guarantees. We hope, however, that the set of bugs that might get past this testing is largely orthogonal to the issues that get past review or our use of formal methods.
Tests also lose their power when they don't get run on every compiler+architecture+configuration. Few pieces of software do runtime self-tests and few users (or even distributions) actually run the test suite on their particular system. When they are cross-compiling to an embedded system, it might not even be realistically possible to do so.
Sadly even formal proofs are not guarantees for security in practice, especially when you're talking about constructs more complicated than field arithmetic, because the proven properties seldom map precisely to our intuitions about what constitutes correct behavior. This is especially true for very open ended code where it gets applied to applications which were entirely unforeseen by the developer.
Right now I believe we've have a testing methodology in place for every class of serious issue we've ever had in development that would have a fighting chance of catching it even if we didn't know about the specific issue. But then again, I would have also said the same thing before the last class of errors we found that our process was unlikely to detect. :)
Then again, this doesn't really sound all that different from the kinds of security assumptions normally made in cryptography: Why is the discrete log problem (in certain groups) hard? Because no one knows of an effective attack.
The difference is that many (most?) pieces of open source software receive little to effectively no peer review.
Fuzzing works quite well though. (Even for the cornercase bugs that fuzzing can't find by chance because they're too rare, but modern coverage-guided fuzzing works surprisingly well for that case.)