一句话：提出自动化方法验证密码学 C 程序中的大数非线性算术，首次建立 OpenSSL 若干曲线实现的函数正确性。
密码学原语是现代安全的基石，其 C 实现的正确性对抵御恶意攻击至关重要。然而，这类程序中的典型算术运算包含大量非线性操作，使现有自动化 C 验证工具难以应对。本文提出一种面向密码学 C 程序的自动化验证方法，并应用于 OpenSSL 中 NIST P-224、P-256、P-521 以及 Curve25519 所用的各类算术运算的 C 实现。验证过程不仅成功建立了这些实现的函数正确性（据作者所述为首次），还暴露出一个 bug 以及若干长期存在的异常，相关问题已报告给 OpenSSL 社区并获得确认。该工作表明自动化验证技术可有效处理真实密码库中大数算术这一难题。
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.
DOI 原文 ·
@inproceedings{paperbot5284,
title = {Verifying Arithmetic in Cryptographic C Programs},
author = {Jiaxiang Liu and Xiaomu Shi and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00058}
}