一句话：提出自动形式化验证工具 llvm2CryptoLine，可高效验证工业密码库 C 程序中的非线性算术运算。
密码原语实现的正确性对现代安全至关重要，而其实现中常包含难以验证的非线性算术运算。本文提出 llvm2CryptoLine，一个面向密码学 C 程序中算术运算的自动形式化验证工具。该工具将 C 程序经 LLVM 中间表示翻译到 CryptoLine 验证框架，从而对算术运算进行形式化验证。作者在来自工业密码库 OpenSSL、wolfSSL 和 NaCl 的 51 个算术 C 程序上进行了评估，llvm2CryptoLine 成功验证了全部程序，且大多数程序可被完全自动、高效地验证。论文还提供了演示视频与开源代码。
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.
@inproceedings{Chen0S0WY23,
title = {llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs},
author = {Ruiling Chen and Jiaxiang Liu and Xiaomu Shi and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang},
booktitle = {FSE},
year = {2023},
doi = {10.1145/3611643.3613096}
}