密码算法的代码验证和安全实现--研究survey

这方面的研究最近非常热，IEEE Symposium on Security & Privacy 2019 (S&P'19)发表了一篇Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises，相关github页面 fiat-crypto: Cryptographic Primitive Code Generation by Fiat

之前还有一些研究论文（包括CCS 2017的HACL和今年最新的EverCrypt）：

Secure, fast and verified cryptographic applications: a scalable approach

HACL*: A Verified Modern Cryptographic Library

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider

其中EverCrypt号称完成了经过验证、且和其它所有密码算法库实现相比性能最好的Curve25519实现（即使其它密码算法库没有经过验证，例如OpenSSL）