4 ms·

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

by 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...

by rurban 4y ago

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...