一句话：提出语言级安全概念与组合策略，实现高效掩码防护的自动化验证并优化AES S盒。
掩码是抵御功耗侧信道攻击的有效防护，但其设计复杂且易错。已有严格验证方法可扩展性不足，而现有组合式方法无法证明近期高效实现的安全性。本文提出新的组合式验证方法：引入两个语言级安全概念，并据此设计组合策略与验证算法，从而能够证明此前组合方法无法处理的高效实现。作者实现工具 CONVINCE，并通过大量实验验证其有效性；还利用该工具探索 AES S 盒设计空间，用更高效有限域乘法实现替换原实现，自动证明新版本无泄漏，最终将当前最优 AES 实现的随机数减少 1,600、XOR 运算减少 3,200。
Masking is one of the most effective countermeasures for securely implementing cryptographic algorithms against power side-channel attacks, the design of which however turns out to be intricate and error-prone. While techniques have been proposed to rigorously verify implementations of cryptographic algorithms, currently they are limited in scalability. To address this issue, compositional approaches have been investigated, but insofar they fail to prove the security of recent efficient implementations. To fill this gap, we propose a novel compositional verification approach. In particular, we introduce two new language-level security notions based on which we propose composition strategies and verification algorithms. Our approach is able to prove efficient implementations, which cannot be done by prior compositional approaches. We implement our approach as a tool CONVINCE and conduct extensive experiments to confirm its efficacy. We also use CONVINCE to further explore the design space of the AES Sbox with least refreshing by replacing its implementation for finite-field multiplication with more efficient counterparts. We automatically prove leakage-freeness of these new versions. As a result, we can effectively reduce 1,600 randomness and 3,200 XOR-operations of the state-of-the-art AES implementation.
@article{paperbot1855,
title = {Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks},
author = {Pengfei Gao and Yedi Zhang and Fu Song and Taolue Chen and Francois-Xavier Standaert},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622862}
}