s2n-bignum

Not in Coq, but you might find this interesting from AWS: https://github.com/awslabs/s2n-bignum?tab=readme-ov-file#tes...

I'm super proud of the work that the aws-lc team have been doing. Insanely powerful optimizations on many platforms (not least Graviton!) ... and those optimizations are formally generated or formally verified (see https://github.com/awslabs/s2n-bignum and https://github.com/awslabs/aws-lc-verification for directly related work) and also make massive improvements to the constant-timeness of the operations, which is important for mitigating side-channels. I suspect most of the team would tell anyone "We have to write this in Assembly and C, but you don't have to! Rust is what we prefer to see at the application layer."

> Does 25519 suffer from key/data-dependant execution time? I mean, when implemented naively, yes, but the industry has been aware of timing attacks for decades such that this is table stakes for any crypto implementations. From the article: > We also do our best to execute the algorithms in constant time, to thwart side-channel attacks that infer secret information from the durations of computations. https://github.com/awslabs/s2n-bignum (where most of the heavy lifting is done, per the article) further explicitly states that "Each function is moreover written in a constant-time style to avoid timing side-channels."