A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs

摘要: Side-channel attacks, which are capable of breaking secrecy via side-channel information, pose a growing threat to the implementation cryptographic algorithms. Masking is an effective countermeasure against attacks by removing statistical dependence between and power consumption randomization. However, designing efficient masked implementations turns out be error-prone task. Current techniques for verifying whether programs secure limited in their applicability accuracy, especially when they applied. To bridge this gap, article, we first propose sound type system, equipped with inference algorithm, arithmetic higher-order attacks. We then give novel model-counting-based pattern-matching-based methods that able precisely determine potential leaky observable sets detected system genuine or simply spurious. evaluate our approach on various programs. The experiments confirm outperforms state-of-the-art baselines terms applicability, efficiency.