2 ms·

Hopefully people working on hashes and codecs will use Rust in the future, so Valgrinding and such are less needed.

rurban 4y 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-saferewrite-4x3.pdf https://cr.yp.to/talks/2021.09.03/slides-djb-20210903-safere... * https://github.com/GaloisInc/hacrypto https://github.com/GaloisInc/hacrypto * https://github.com/fmlab-iis/cryptoline https://github.com/fmlab-iis/cryptoline * https://github.com/mit-plv/fiat-crypto/ https://github.com/mit-plv/fiat-crypto/ (Bedrock2) * https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star (F* and ValeCrypt) * https://github.com/jasmin-lang/jasmin https://github.com/jasmin-lang/jasmin * https://vst.cs.princeton.edu/ https://vst.cs.princeton.edu/
- touisteur 4y 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-code-with-spark https://blog.adacore.com/avoiding-vulnerabilities-in-crypto-... * https://blog.adacore.com/sparknacl-two-years-of-optimizing-crypto-code-in-spark-and-counting https://blog.adacore.com/sparknacl-two-years-of-optimizing-c... * https://github.com/Componolit/libsparkcrypto 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...
seanw444 4y ago
Let me cross that one off my daily bingo card...

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-saferewrite-4x3.pdf https://cr.yp.to/talks/2021.09.03/slides-djb-20210903-safere... * https://github.com/GaloisInc/hacrypto https://github.com/GaloisInc/hacrypto * https://github.com/fmlab-iis/cryptoline https://github.com/fmlab-iis/cryptoline * https://github.com/mit-plv/fiat-crypto/ https://github.com/mit-plv/fiat-crypto/ (Bedrock2) * https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star (F* and ValeCrypt) * https://github.com/jasmin-lang/jasmin https://github.com/jasmin-lang/jasmin * https://vst.cs.princeton.edu/ https://vst.cs.princeton.edu/

touisteur 4y 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-code-with-spark https://blog.adacore.com/avoiding-vulnerabilities-in-crypto-... * https://blog.adacore.com/sparknacl-two-years-of-optimizing-crypto-code-in-spark-and-counting https://blog.adacore.com/sparknacl-two-years-of-optimizing-c... * https://github.com/Componolit/libsparkcrypto 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...

seanw444 4y ago

Let me cross that one off my daily bingo card...