A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs
This work addresses the error-prone task of verifying masked implementations for cryptographic algorithms, which is crucial for security against side-channel attacks, though it appears incremental by building on existing verification techniques.
The paper tackles the problem of verifying masked arithmetic programs against side-channel attacks by proposing a sound type system with efficient inference and novel model-counting and pattern-matching methods to reduce spurious detections. The approach outperforms state-of-the-art baselines in applicability, accuracy, and efficiency, as confirmed by experiments on various cryptographic implementations.
Side-channel attacks, which are capable of breaking secrecy via side-channel information, pose a growing threat to the implementation of cryptographic algorithms. Masking is an effective countermeasure against side-channel attacks by removing the statistical dependence between secrecy and power consumption via randomization. However, designing efficient and effective masked implementations turns out to be an error-prone task. Current techniques for verifying whether masked programs are secure are limited in their applicability and accuracy, especially when they are applied. To bridge this gap, in this article, we first propose a sound type system, equipped with an efficient type inference algorithm, for verifying masked arithmetic programs against higher-order attacks. We then give novel model-counting based and pattern-matching based methods which are able to precisely determine whether the potential leaky observable sets detected by the type system are genuine or simply spurious. We evaluate our approach on various implementations of arithmetic cryptographicprograms.The experiments confirm that our approach out performs the state-of-the-art base lines in terms of applicability, accuracy and efficiency.