Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa

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 reports false positives. The proposed tool-flow is able to detect masking flaws induced by HLS-optimizations as well.

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

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 reports false positives. The proposed tool-flow is able to detect masking flaws induced by HLS-optimizations as well.
Paper Structure (26 sections, 2 theorems, 4 equations, 6 figures, 12 tables, 1 algorithm)

This paper contains 26 sections, 2 theorems, 4 equations, 6 figures, 12 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Motivation
  3. background
  4. Masking
  5. The Extended Probing Model
  6. Formal Verification of Masked Hardware
  7. REBECCA
  8. REBECCA overall flow
  9. Fourier Expansion of a Boolean Function
  10. Label in REBECCA
  11. Complexity of REBECCA
  12. Using High-Level Synthesis to generate Masked Hardware
  13. Impact of HLS on masking
  14. HLS front-end
  15. HLS back-end
  16. ...and 11 more sections

Key Result

Lemma 1

The state-wise splitting constructs state-wise designs $D_0, D_1, \ldots, D_n$ such that for any execution trace $T$ of the design $D$, every operation occurring in $T$ is captured by at least one of the state-wise designs $D_x$, $x \in \{0, n\}$.

Figures (6)

  • Figure 1: Motivating example for state-based verification of masked hardware
  • Figure 2: Label propagation through logic gates in the verification circuit.
  • Figure 3: HLS-output controller and datapath for the C-design in Listing \ref{['lst:resourceallocation']} with resource constraints of two MULT per clock cycle.
  • Figure 4: Intuition Example: Unrolled datapath over four-cycles of the cascaded masked multiplier of Figure \ref{['fig:intuition0']} corresponding to HLS-input of Listing \ref{['lst:resourceallocation']} (with a resource constraint of at-most two MULT (multiplier units) per cycle; depicted with operations corresponding to each state
  • Figure 5: Proposed MaskedHLSVerif Verification flow (In this work, the Hardware Masking Verification Tool used is REBECCA rebeccabloem2018formal)
  • ...and 1 more figures

Theorems & Definitions (4)

  • Lemma 1: Soundness of State-wise Split
  • proof
  • Lemma 2: Soundness of MaskedHLSVerif
  • proof