llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs

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

Abstract

Correct implementations of cryptographic primitives are essential for modern security. These implementations often contain arithmetic operations involving non-linear computations that are infamously hard to verify. We present llvm2CryptoLine, an automated formal verification tool for arithmetic operations in cryptographic C programs. llvm2CryptoLine successfully verifies 51 arithmetic C programs from industrial cryptographic libraries OpenSSL, wolfSSL and NaCl. Most of the programs are verified fully automatically and efficiently. A screencast that showcases llvm2CryptoLine can be found at https://youtu.be/QXuSmja45VA. Source code is available at https://github.com/fmlab-iis/llvm2cryptoline.

BibTeX

@inproceedings{Chen-al:FSE23,
  author    = {Ruiling Chen and
               Jiaxiang Liu and
               Xiaomu Shi and
               Ming{-}Hsien Tsai and
               Bow{-}Yaw Wang and
               Bo{-}Yin Yang},
  title     = {{llvm2CryptoLine:} Verifying Arithmetic in Cryptographic C Programs},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {2167--2171},
  publisher = {{ACM}},
  year      = {2023},
}

llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs

Abstract

Related papers