International Association for Cryptologic Research

International Association
for Cryptologic Research

Transactions on Cryptographic Hardware and Embedded Systems 2025

Higher-Order Time Sharing Masking


README

Higher-Order Time Sharing Masking

This repository contains the supplementary materials for the paper "Higher-Order Time Sharing Masking", accepted for publication at CHES 2025.

Contents

HDL Source Code (Verilog)

AES S-Box Designs

We include various implementations of masked AES S-Boxes with different latencies and orders of security. Each design corresponds to specific sections of the paper:

  1. Second-Order Masked AES S-Box (latency = 2)
    Refer to Section 3.4 in the paper.

  2. Second-Order Masked AES S-Box (latency = 3)
    Refer to Section 4.5 in the paper.

  3. First-Order Masked AES S-Box (latency = 2)
    Refer to Section 4.4 in the paper.

Each of these folders contains two subfolders:
- rtl/: Contains the Verilog files with descriptive headers for each module.
- sim/: Includes self-checking testbenches that automatically validate the functional correctness of both the S-box and full AES implementations.

Indexing note: Our RTL uses one-based ranges (for example, input [80:1]). If you prefer the more common zero-based notation (for example, [79:0]), you will need to adjust the signal declarations accordingly.

Round-Based First-Order Secure AES-128

This implementation corresponds to Section 4.6 of the paper.

Dependency Structure with Module Descriptions

The design consists of source files located in the rtl folder (written in Verilog) and corresponding testbenches in the sim subfolder, used for verifying the top module.

aes_top
│
├── aes_keyschedule  // Implements the masked key schedule for AES
│
├── aes_round_function  // Implements the round function for AES with first-order Time Sharing Masking
│   ├── aes_shift_row
│   ├── AES_sbox_twocycle_firstorder  // Implements a two-cycle first-order masked AES S-Box
│   │   ├── HO_TSM1  // Time-sharing module for processing two input shares securely
│   │   │   ├── fourinput_compute_subscript0  // Computes the first phase of HO_TSM1 operation
│   │   │   └── fourinput_compute_subscript1  // Computes the second phase of HO_TSM1 operation
│   │   ├── sum_of_second_module_outputs  
│   │   ├── cross_module_multiplication  // Operates on one share from each HO_TSM1 module
│   │   ├── domain_inner  // Calculates all the inner-module terms
│   │   └── xor_module
│   ├── aes_mixcolumn  // Implements the MixColumn operation for AES
│   │   └── aes_mul2  // Implements a masked AES multiply-by-2 operation in GF(2^8)
│   ├── two_dimension_xor
│   └── two_dimension_mux
│
└── trivium_prng  // Implements the Trivium Pseudo-Random Number Generator (PRNG)

The structure above outlines the module dependencies and highlights the relationship between submodules.

Toy Examples for Formal Verification

  1. HO-TSM
    Includes a HO-TSM2 AND gate presented as a preliminary example in Section 3.1 and a HO-TSM3 AND gate.

  2. Area-Latency Trade-Off
    Implementations for the four-input Boolean function presented as a toy example in Section 4.1 for security orders d = 1 and d = 2.

Generating Netlists

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

Customizing the Synthesis Process

Before running the synthesis, ensure the following parameters are correctly set in the compile.tcl file:

  1. Ensure write permissions

    From the artifact root, run:

    chmod -R a+rwX .

    This grants read, write, and (where appropriate) execute permissions to all users on every file and directory, ensuring that dc_shell can write to generated_netlists, logfiles, reports, work, etc.

  2. Specify the Top Module
    Set the top module of the design by assigning its name to the variable <code>TOPCELL_ENT</code>. This ensures the correct module is synthesized.

  3. Define the RTL Source Directory
    Set the location of the RTL Verilog files using the following command:

    analyze -library WORK -autoread {$LOCATION} > ./logfiles/analyze.log

    Replace $LOCATION with the correct path to your design files.

  4. Specify the Output Netlist Name
    Define the name and location for the generated netlist using the following command:

    write -format verilog -hierarchy -output ./generated_netlists/$NETLIST_NAME.v

    Replace $NETLIST_NAME with the desired name for your output netlist file.

Example commands for configuring these parameters are provided in the compile.tcl script and can be adjusted according to your specific design requirements.

.synopsys_dc.setup is the initialization file for dc_shell. It contains the necessary environment variables required for running the compile.tcl script.

After configuring the parameters and making the necessary changes, synthesize the design using the following command:

dc_shell -f compile.tcl

During netlist generation, please note the following:

Note on “Can’t find lib_cells” messages
When you run compile.tcl, you may see errors like:

Error: Can’t find lib_cells matching 'NangateOpenCellLibrary/OR5*'. (UID-109)
Error: Value for list 'object_list' must have 1 elements. (CMD-036)

These occur because we proactively issue many set_dont_use [get_lib_cells …] commands (even for cells that do not exist in the Nangate library) to ensure a consistent subset of cells for downstream formal tools (SILVER and PROLEAD). Since those patterns simply match nothing, these errors are benign and can be safely ignored; they do not affect the final netlist, timing, area, or power reports.

Formal Verification

We use two formal verification tools for evaluating the security of our implementations:
- SILVER (https://github.com/Chair-for-Security-Engineering/SILVER)
- PROLEAD (https://github.com/ChairImpSec/PROLEAD)

SILVER

SILVER is used to verify the toy examples:
- HO-TSM: Includes a HO-TSM2 AND gate (Section 3.1) and a HO-TSM3 AND gate.
- Area-Latency Trade-Off: Implements a four-input Boolean function (Section 4.1) for security orders d = 1 and d = 2.

The scalability of SILVER is limited for larger designs, which is why toy examples are used for verification. Additionally, please note that the duration of the verification process increases significantly with the security order.

Setting Up SILVER for Formal Verification

To formally verify the generated netlists:

  1. Follow the instructions provided in the official SILVER repository to build the framework:
    https://github.com/Chair-for-Security-Engineering/SILVER and ensure the framework is fully set up before proceeding with the verification process.

  2. SILVER does not require any custom scripts for verification. Instead, you need to annotate the inputs and outputs of the top module in the netlist. You can follow the guidelines provided in the SILVER documentation.
    We have already annotated the inputs and outputs of the netlists for our toy examples in the ./generated_netlists/ folder. These annotated netlists can be used as a reference.

  3. The official SILVER repository provides necessary command-line options for formal verification of the generated netlist. Below is an example command for reference:

    ./bin/verify --verbose=1 --verilog=1 --verilog-design_file=$PATH_TO_TOP_MODULE --verilog-module_name=$TOP_MODULE_NAME

PROLEAD

PROLEAD is used to verify the security properties of AES S-Box designs:

For completeness, we have also included the netlist for the Second-Order Masked AES S-Box (latency = 2). However, due to the large size of this design, we did not verify it using PROLEAD, as the analysis was computationally infeasible within our evaluation setup.

Please refer to the official PROLEAD Wiki for installation instructions.

Note: This project uses a development version of PROLEAD that is 14 commits ahead of the official v2.0.0 release. As a result, there may be differences between the current documentation on their website and our instructions.

PROLEAD version used: v2.0.0 + 14 commits (commit 44a15f5a962d6063f1d1a64405e9045e3fdb9efb, authored on August 31, 2023), on branch main.

Configuration Files

PROLEAD takes a netlist as an input and requires a configuration file to customize settings specific to the implementation being tested. We provide two example configuration files in the scripts folder, which you can use as references for your own setup.

Example Command to Run PROLEAD

./release/PROLEAD -df $PATH_TO_TOP_MODULE -mn $TOP_MODULE_NAME -cf $PATH_TO_CONFIG_FILE

Verification Results

We provide screenshots of the SILVER verification results, which indicate whether the implementation has passed probing security, Non-Interference (NI), Strong Non-Interference (SNI), and Probe-Isolating Non-Interference (PINI) tests. Each screenshot reflects the outcome under both standard and robust probing models.

The PROLEAD verification results include the console output along with detailed reports generated after each simulation step.

Publication

Dilip Kumar S. V., Siemen Dhooghe, Josep Balasch, Benedikt Gierlichs, and Ingrid Verbauwhede,
“Higher-Order Time Sharing Masking,”
IACR Transactions on Cryptographic Hardware and Embedded Systems (TCHES), Volume 2025, Issue 2.
https://tches.iacr.org/index.php/TCHES/article/view/12047

Repository

Complete source code and development history are available at:
https://github.com/KULeuven-COSIC/TSM