Paper 2024/1202

Prover - Toward More Efficient Formal Verification of Masking in Probing Model

Abstract

In recent years, formal verification has emerged as a crucial method for assessing security against Side-Channel attacks of masked implementations, owing to its remarkable versatility and high degree of automation. However, formal verification still faces technical bottlenecks in balancing accuracy and efficiency, thereby limiting its scalability. Former efficient tools like \textsf{maskVerif} and CocoAlma are often inaccurate when verifying schemes utilizing properties of Boolean functions. Later, SILVER addressed the accuracy issue, albeit at the cost of significantly reduced speed and scalability compared to \textsf{maskVerif}. Consequently, there is a pressing need to develop formal verification tools that are both efficient and accurate for designing secure schemes and evaluating implementations. This paper's primary contribution lies in proposing several approaches to develop a more efficient and scalable formal verification tool called \textsf{Prover}, which is built upon SILVER. Firstly, inspired by the auxiliary data structures proposed by Eldib et al. and optimistic sampling rule of maskVerif, we introduce two reduction rules aimed at diminishing the size of observable sets and secret sets in statistical independence checks. These rules substantially decrease, or even eliminate, the need for repeated computation of probability distributions using Reduced Ordered Binary Decision Diagrams (ROBDDs), a time-intensive procedure in verification. Subsequently, we integrate one of these reduction rules into the uniformity check to mitigate its complexity. Secondly, we identify that variable ordering significantly impacts efficiency and optimize it for constructing ROBDDs, resulting in much smaller representations of investigated functions. Lastly, we present the algorithm of \textsf{Prover}, which efficiently verifies the security and uniformity of masked implementations in probing model with or without the presence of glitches. Experimental results demonstrate that our proposed tool \textsf{Prover} offers a superior balance between efficiency and accuracy compared to other state-of-the-art tools (CocoAlma, maskVerif, and SILVER). It successfully verifies a design that SILVER could not complete within the allocated time, whereas CocoAlma and maskVerif encounter issues with false positives.