Sharing Independence Relabeling: Efficient Formal Verification of Higher-Order Masking

The efficient verification of the security of masked hardware implementations is an important issue that hinders the development and deployment of randomness-efficient masking techniques. At EUROCRYPT 2018, Bloem et al. [6] introduced the first practical formal tool to prove the side-channel resilience of masked circuits in the probing model with glitches. Most recently Barthe et al.[2] introduced a more efficient formal tool that builds upon the findings of Bloem et al. for modeling the effects of glitches. While Barthe et al.'s approach greatly improves the first-order verification performance, it shows that higher-order verification in the probing model with glitches is still enormously time-consuming for larger circuits like a second-order AES S-box, for instance. Furthermore, the results of Barthe et al. underline the discrepancy between state-of-the-art formal security notions that allow for faster verification of circuits. Namely the strong non-interference (SNI) notion, and existing masked hardware implementations that are secure in the probing model with glitches. In this work, we extend and improve the formal approaches of Bloem et al. and Barthe et al. on manifold levels. We first introduce a so-called sharing independence notion which helps to reason about the independence of shared variables. We then show how to use this notion to test for the independence of input and output sharings of a module which allows speeding up the formal verification of circuits that do not fulfill the SNI notion. With this extension, we are for the time able to verify the security of a second-order masked DOM AES S-box which takes about 3 seconds, and up to a fifth-order AES S-box which requires about 47 days for verification. Furthermore, we discuss in which case the independence of input and output sharings lead to composability