Hacker News new | ask | show | jobs
by rurban 1201 days ago
You'd be surprised how many of those submitted and approved crypto standards are still not tested with industry best practices.

buffer overflows or integer UB's and overflows are very common. ubsan, asan, valgrind tests are missing. some do offer symbolic verification of the algo, but not the implementations.

See my https://github.com/rurban/smhasher#crypto paragraph, and "Finding Bugs in Cryptographic Hash Function Implementations", Nicky Mouha, Mohammad S Raunak, D. Richard Kuhn, and Raghu Kacker, 2017. https://eprint.iacr.org/2017/891.pdf
1 comments
miohtama 1200 days ago
Hopefully people working on hashes and codecs will use Rust in the future, so Valgrinding and such are less needed.
link
rurban 1200 days ago
Or even better an explicitly secure language, not just one only claiming various safeties without actually implementing them.

ADA/Spark or Modula-2 would come to my mind, but there must be more like rune for constant-time and more such crypto-only problems. I'm sure djb has such one also. https://cr.yp.to/talks/2021.09.03/slides-djb-20210903-safere...

* https://github.com/GaloisInc/hacrypto

* https://github.com/fmlab-iis/cryptoline

* https://github.com/mit-plv/fiat-crypto/ (Bedrock2)

* https://github.com/hacl-star/hacl-star (F* and ValeCrypt)

* https://github.com/jasmin-lang/jasmin

* https://vst.cs.princeton.edu/

link
touisteur 1200 days ago
Yes, there are actually implementations of most standard stuff in Ada and SPARK (so with some level of proof)

Interesting posts (and links):

* https://blog.adacore.com/avoiding-vulnerabilities-in-crypto-...

* https://blog.adacore.com/sparknacl-two-years-of-optimizing-c...

* https://github.com/Componolit/libsparkcrypto

Proof of constant-time execution is an interesting field, but as I understand very much less mature than the SPARK toolset. If anyone has a toolchain working over llvm to check and/or make code constant-time, I'm interested.

I mean, if the standards people want to keep writing C, they can probably use Frama-C for the standard implementation...

link
seanw444 1200 days ago
Let me cross that one off my daily bingo card...
link