Coupling Leakage in Theory and Practice
TL;DR
This work focuses on detecting (low-level) vulnerabilities in masked FPGA designs through experimental and tool-assisted evaluation and shows how to formally abstract, unveil, and mitigate such leakages, thereby enabling a security-aware FPGA design flow that spans from the behavioral to the physical level.
Abstract
With the widespread adoption of Field Programmable Gate Arrays (FPGAs) in security-critical industries such as defense and telecommunications, ensuring the confidentiality of sensitive data processed by these devices has become paramount. Side-Channel Analysis (SCA) poses a significant threat, necessitating the protection of cryptographic primitives through effective and efficient countermeasures. Within the framework of well-established formal adversary models, Boolean masking offers provable resistance to SCA by randomizing sensitive intermediate computations using Shamir’s secret sharing. However, the secure and efficient implementation of Boolean masking in hardware presents a complex and error-prone challenge. Physical effects such as glitches, transitions, and couplings can undermine essential security assumptions, potentially weakening the effectiveness of masking. Although robust masking schemes are designed to maintain their security in the presence of glitches and transitions, and their secure implementation can be verified at the gate level using a wide range of automated verification tools – albeit mostly for Application-Specific Integrated Circuits (ASICs) and not FPGAs – leakages caused by coupling effects remain undetectable by such tools, as they occur at a lower abstraction level.In this work, we focus on detecting (low-level) vulnerabilities in masked FPGA designs through experimental and tool-assisted evaluation. The flaws that we target are not detectable at the Register Transfer Level (RTL) level, and in some cases, not even at the gate level, as they arise from optimizations introduced during synthesis or implementation, or from the specific outcomes of the Place and Route (PnR) process. We demonstrate that these flaws are not only theoretically concerning, but can lead to observable leakages in practical experiments. Furthermore, we show how to formally abstract, unveil, and mitigate such leakages, thereby enabling a security-aware FPGA design flow that spans from the behavioral to the physical level. As an example, we implement all the evaluation steps presented as an extension of PROLEAD and validate its accuracy and effectiveness through practical case studies.