L. Bunina

End-to-end verification of elliptic curve cryptographic primitives: From specification to secure code

   Objectives. The work set out to develop and substantiate a methodology for synthesizing high-performance and simultaneously verified implementations of elliptic curve cryptosystems.    The challenge of ensuring mathematical correctness and engineering security of the code was overcome by integrating machine-ch...