Time Sharing Masking (TSM)

This repository contains the supplementary materials corresponding to the paper "Time Sharing - A Novel Approach to Low-Latency Masking" accepted for publication in CHES 2024. We include the HDL source code(Verilog), corresponding netlists and formal verification results for the S-Boxes of PRINCE and AES.

Please refer to the README files in the PRINCE_SBox and AES_SBox subfolders for more information.

Instructions

To formally verify our netlist, there are two steps. First, we need to synthesize our Verilog design to generate netlists. Second, we verify the generated netlists using the formal verification tool SILVER.

Generating Netlists

The Verilog files are synthesized using NanGate 45nm Open Cell Library, with Synopsys DC Compiler v2021.06 as outlined in the paper.

• The empty folder NangateOpenCellLibrary_PDKv1_3_v2010_12 is intended to contain the files for the NanGate Open Cell Library. Due to the large size of the library, we were unable to include its contents in this artifact. You can access the Nangate library using the following OneDrive Link. Alternatively, the library is publicly available in the following GitHub repository: https://github.com/vmarribas/VerMFi, corresponding to the paper by Arribas et al. Please download the NanGate folder either from this repository or from the OneDrive link and replace the empty folder in this artifact before use.
• The synthesis script, compile.tcl, can be used as a reference for generating netlists and estimating area, maximum frequency as reported in our paper. Set the top module of the design to be synthesized using the variable TOPCELL_ENT in the compile.tcl file.
• .synopsys_dc.setup is the initialization file for dc_shell, containing the necessary environment variables for the compile.tcl script.

After making the necessary changes, synthesize the design by running the command dc_shell -f compile.tcl.

Formal Verification

To formally verify the generated netlists:
1. Build SILVER framework using the instructions in their repository: https://github.com/Chair-for-Security-Engineering/SILVER
2. Annotate the inputs and outputs of the top module in the netlist according to the guidelines in the SILVER repository. We provide some netlists in the ./PRINCE_SBox/netlist/ folder with annotated inputs and outputs, which can be used as a reference.
3. You can also find the necessary command line options to formally verify the generated netlist. An example command to verify our PRINCE S-Box is:

./bin/verify --verbose=1 --verilog=1 --verilog-design_file=$REPO_TOP/PRINCE_SBox/netlist/compile/compile_exact_map.v --verilog-module_name=PRINCE_sbox_opt

where $REPO_TOP refers to the local path where this artifact is in your computer.

Publication

D. Kumar S. V., S. Dhooghe, J. Balasch, B. Gierlichs, I. Verbauwhede "Time Sharing - A Novel Approach to Low-Latency Masking" IACR Transactions on Cryptographic Hardware and Embedded Systems (TCHES) 2024, Volume 3. link