Formal Verification of Probing Security via Conditional Independence
For cryptographers and security engineers, this provides a formal method to verify side-channel attack countermeasures, reducing error-prone manual proofs.
This work proposes a novel approach to formal verification of probing security for masked cryptographic algorithms by linking noninterference to conditional independence and using a separation logic (Lilac) to verify it, providing proof rules and demonstrating on examples.
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.