一句话：提出面向算术程序掩码防护的形式化验证方法，并实现工具 QMVerif，提升精度与可扩展性。
密码算法广泛用于保护数据隐私，但其实现可能遭受实际功耗侧信道攻击，攻击者可通过分析设备功耗与私有数据的相关性推断秘密。掩码方案被提出以抵御此类攻击，但依赖安全掩码方案的实现并非先验安全。现有掩码防护形式化验证与掩码强度量化技术主要局限于布尔程序，且精度较低。本文提出一种用于形式化验证算术程序掩码防护的方法，在算术程序上具有更高精度，在布尔程序上具有更好可扩展性，并支持组合推理。作者实现验证工具 QMVerif，并在包括完整 AES、DES 与 MAC-Keccak 的密码基准上进行广泛评估，实验结果证明了该方法的有效性与效率。
Cryptographic algorithms are widely used to protect data privacy in many aspects of daily lives from smart card to cyber-physical systems. Unfortunately, programs implementing cryptographic algorithms may be vulnerable to practical power side-channel attacks, which may infer private data via statistical analysis of the correlation between power consumptions of an electronic device and private data. To thwart these attacks, several masking schemes have been proposed. However, programs that rely on secure masking schemes are not secure a priori. Although some techniques have been proposed for formally verifying masking countermeasures and for quantifying masking strength, they are currently limited to Boolean programs and suffer from low accuracy. In this work, we propose an approach for formally verifying masking countermeasures of arithmetic programs. Our approach is more accurate for arithmetic programs and more scalable for Boolean programs comparing to the existing approaches. We have implemented our methods in a verification tool QMVerif which has been extensively evaluated on cryptographic benchmarks including full AES, DES and MAC-Keccak. The experimental results demonstrate the effectiveness and efficiency of our approach, especially for compositional reasoning.
DOI 原文 ·
@inproceedings{paperbot5998,
title = {Formal verification of masking countermeasures for arithmetic programs},
author = {Pengfei Gao},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3418920}
}