4 ms·
Synthesizing Correct-by-Construction Code for Cryptographic Primitives
- jey 6y agoHere's the abstract from their paper: We introduce a new approach for implementing cryptographic arithmetic in short high-level code with machine checked proofs of functional correctness. We further demonstrate that simple partial evaluation is sufficient to transform such initial code into the fastest-known C code, breaking the decades old pattern that the only fast implementations are those whose instruction-level steps were written out by hand. These techniques were used to build an elliptic-curve library that achieves competitive performance for 80 prime fields and multiple CPU architectures, showing that implementation and proof effort scales with the number and complexity of conceptually different algorithms, not their use cases. As one outcome, we present the first verified high-performance implementation of P-256, the most widely used elliptic curve. Implementations from our library were included in BoringSSL to replace existing specialized code, for inclusion in several large deployments for Chrome, Android, and CloudFlare.
- johlo 6y agoA list of projects using the code generated by fiat-crypto: https://github.com/mit-plv/fiat-crypto/issues/902 https://github.com/mit-plv/fiat-crypto/issues/902