International Association
for Cryptologic Research

A decisive contribution to the all-embracing protection of cryptographic software, especially on embedded devices, is the protection against SCA attacks. Masking countermeasures can usually be integrated into the software during the design phase. In theory, this should provide reliable protection against such physical attacks. However, the correct application of masking is a non-trivial task which often causes even experts to make mistakes. In addition to human-caused errors, micro-architectural CPU effects can lead even a seemingly theoretically correct implementation to fail satisfying the desired level of security in practice. This originates from different components of the underlying CPU which complicates the tracing of leakage back to a particular source and hence avoids to make general and device-independent statements about its security. In this work, we adapt PROLEAD for the evaluation of masked software, which has recently been presented at CHES 2022 and originally developed as a simulation-based tool to evaluate masked hardware designs. We enable to transfer the already known benefits of PROLEAD into the software world. These include (1) evaluation of larger designs compared to the state of the art, e.g. a full AES masked implementation, and (2) formal verification under the well-established robust probing security model. In short, together with an abstraction model for the micro-architecture, the robust probing model allows us to efficiently detect micro-architectural leakages while being independent of a concrete CPU design. As a concrete result, using PROLEAD_SW we evaluated the security of several publicly available masked software implementations and revealed multiple vulnerabilities.