Controller-Datapath Aware Verification of Masked Hardware Generated via High-Level Synthesis

From bibtex.

Abstract

Masking is a countermeasure against Power Side-Channel Attacks (PSCAs) in both software and hardware implementations of cryptographic algorithms. Compared to software masking, implementing masked hardware is time-consuming and error prone. Recent approaches, therefore, rely on High-Level Synthesis (HLS) tools to automatically generate masked Register-Transfer Level (RTL) hardware from verified masked software, significantly reducing design effort. Since HLS was never developed for security, HLS optimizations may impact PSCA security of the generated RTL. As a result, verifying the PSCA-security of HLS-generated masked RTL is crucial. Existing hardware masking verification tools can verify masked hardware, but may produce false positives when applied to HLS-generated designs with controller-datapath architectures obtained due to resource-shared datapath obtained via HLS. This work proposes a hardware masking verification strategy for HLS-generated masked hardware. Our toolflow MaskedHLSVerif performs state-wise formal verification of controller-datapath RTL obtained via HLS, thereby avoiding false positives caused by resource-shared datapaths. Our tool flow correctly verifies standard cryptographic benchmarks, consisting of cascaded masked gadgets and the PRESENT S-box masked with gadgets, where existing tools like REBECCA report false positives. The proposed tool-flow is able to detect masking flaws induced by HLS-optimizations as well.