Side-channel attacks are a major threat to the security of cryptosystems. Masking is a widely used countermeasure against such attacks, but proving the security of masked algorithms is error-prone without formal verification. In this work, we propose a novel approach to formal verification of noninterference properties of masked algorithms based on probabilistic separation logic. By establishing a connection between noninterference and conditional independence, we show how noninterference can be verified using Lilac, a separation logic for conditional independence. We also provide several proof rules that facilitate the verification of probing security and demonstrate their application to example algorithms.

翻译：侧信道攻击对密码系统的安全性构成重大威胁。掩码是一种广泛使用的对抗此类攻击的防护措施，但缺乏形式化验证时，证明掩码算法的安全性容易出错。本文提出了一种基于概率分离逻辑的掩码算法无干扰性形式化验证新方法。通过建立无干扰性与条件独立性之间的关联，我们展示了如何利用面向条件独立性的分离逻辑Lilac验证无干扰性。此外，我们提供了若干便于验证探测安全性的证明规则，并通过示例算法验证了其有效性。