[biot]

What tools are typically used to develop these algorithms? The site has https://password-hashing.net/faq.html#qd which mentions attempts to formally define the security of a good algorithm though a quick scan of the two papers indicates the definitions are mathematical properties described in English. However, when it comes to implementations is there a generally accepted language/framework in which correctness can be proven? Haskell comes to mind as one such language which its proponents tout as ensuring correctness, though I lack the experience to determine whether this means "your broken algorithm runs 100% correctly" vs. "a broken algorithm will not compile".

[ReidZB]

Typically, cryptographic primitives (like block ciphers, hash functions, KDFs, etc) are written in C. Bugs are caught solely by the use of a sharp mind and careful reading.

There are really two reasons for this: (1) optimization is a really big deal; some impls go so far as to have asm for specific architectures or use architecture-specific features like SSE2 and (2) there really isn't very much code for a cryptographic primitive, typically <=1000 lines. (e.g., see https://github.com/khovratovich/Argon2/tree/master/Argon2i/r...).

Once a simple reference implementation is hand-checked, it can be used to generate comprehensive test vectors for other implementations.

This isn't my area of expertise, but I believe there's some research in applied crypto for implementation verification. I know https://github.com/GaloisInc/cryptol is a language that's supposed to help in that regard, but I don't know offhand who all uses that.

[technion]

The other reason for C is that the reference implementation is generally expected to eventually have bindings for every other language - a new standard won't flourish if you find out it's hard access to it in your choice of language.

If you can also write an implementation in something such as Haskell, verifying the input/output between the two implementations is a great way to assure it works as expected.

[ufo]

Low-level crypto stuff such as block cyphers and hashing functions is usually done in C or assembly language. One of the biggest reasons is that its very hard to avoid timing attacks on higher level languages (when a computation takes a different time to run depending on the inputs an attacker can extract some info about secrets you control). Performance is also really important because the bad guys will use whatever means necessary to speed up their brute-forcing and you don't want to give them too much of an edge.

Another reason for C and assembly is that when everything your algorithm manipulates is a bunch of bytes you don't get much advantage from a type system.