[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)