undefined | Better HN

0 pointsrurban3y ago0 comments

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/

0 comments

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

j / k navigate · click thread line to collapse