kirancodes.me
To Proof Maintenance & Beyond!
ASE 2019

Verifying Arithmetic in Cryptographic C Programs

Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

DOI 10.1109/ase.2019.00058dblp

Abstract

Cryptographic primitives are ubiquitous for modern security. The correctness of their implementations is crucial to resist malicious attacks. Typical arithmetic computation of these C programs contains large numbers of non-linear operations, hence is challenging existing automatic C verification tools. We present an automated approach to verify cryptographic C programs. Our approach successfully verifies C implementations of various arithmetic operations used in NIST P-224, P-256, P-521 and Curve25519 in OpenSSL. During verification, we expose a bug and a few anomalies that have been existing for a long time. They have been reported to and confirmed by the OpenSSL community. Our results establish the functional correctness of these C implementations for the first time.

BibTeX
@inproceedings{Liu-al:ASE19,
  author    = {Jiaxiang Liu and
               Xiaomu Shi and
               Ming{-}Hsien Tsai and
               Bow{-}Yaw Wang and
               Bo{-}Yin Yang},
  title     = {Verifying Arithmetic in Cryptographic C Programs},
  booktitle = {ASE},
  pages     = {552--564},
  publisher = {{IEEE}},
  year      = {2019},
}

Related papers