[HN Gopher] Synthesizing Correct-by-Construction Code for Crypto... ___________________________________________________________________ Synthesizing Correct-by-Construction Code for Cryptographic Primitives Author : johlo Score : 31 points Date : 2021-01-03 12:32 UTC (1 days ago) (HTM) web link (github.com) (TXT) w3m dump (github.com) | jey wrote: | Here'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. ___________________________________________________________________ (page generated 2021-01-04 23:01 UTC)