This repository contains source code for the verification tool implemented for the Combined Indistinguishability Analysis paper. The tool implements estimation of random probing leakage under random faults, leveraging indistinguishability analysis based on MTBDDs.
The repository directory structure is organized as follows:
├── case-studies/ # Case study netlist files and configs
├── cell/ # Gate libraries and parsing utilities
├── inc/
└── src/
├── analyzer # Core components performing verification via indistinguishability analysis
├── context # Global context objects such as configuration settings
├── cudd # Cudd extensions/wrappers
├── netlist # Netlist related abstractions
├── parser # Parsing components
├── partitioner # Partitioning strategies
└── preprocessor # Preprocessing strategies
The following instructions have been tested on Ubuntu 24.04.03 LTS with the following library versions:
- Boost: 1.83.0
- Cudd: 3.0.0
- Install required libs/packages/binaries:
$ sudo apt install build-essential automake autoconf libtool libboost-all-dev. - Clone the repository with submodules:
$ git clone --recurse-submodules <repo-url>. If you already cloned without submodules, run$ git submodule update --init.
- Switch directory and compile release build with:
$ cd /path/to/cia && make release. This will automatically build Cudd from the submodule on the first run. - Run CIA with:
$ ./bin/release/cia -c path/to/config. To run the case-studies used in the paper, run thestart-case-studies-<ciphers, gadgets, sboxes>.shscripts.
- Install nix-shell (instructions).
- Switch directory and run nix-shell:
$ nix-shell. The nix shell manages Cudd and Boost automatically; no submodule initialization is needed.
- Build CIA with:
$ cia-release. - Run CIA with:
$ ./bin/release/cia -c path/to/config. Again, to run the case-studies used in the paper, run thestart-case-studies-<ciphers, gadgets, sboxes>.shscripts.
| Key | Value | Description |
|---|---|---|
| general.verbose | {1, 2, 3} | Verbosity level. |
| general.cores | <0, .., n> | Amount of cores for parallel execution. Setting this to 0 specifies using all available cores. |
| general.memory | <1, .., n> | Amount of memory provided to DD managers. |
| general.netlist.file | "/path/to/file" | Path to gatelevel netlist to analyse with CIA. |
| general.library.file | "/path/to/file" | Path to cell library file. |
| general.library.name | "libname" | Name of cell library. |
| general.annotation.file | "/path/to/file" | Path to netlist annotation file. This file contains share annotations for the gate level netlist. |
| general.annotation.apply | {true, false} | Enable/disable annotation application. |
| combined.strategy | {"random", "threshold"} | Specifies security model to perform verification in. |
| combined.interrupt | {true, false} | Enable/disable interrupts once a leaking probe/fault combination have been found. |
| combined.partitioning | {true, false} | Enable/disable partitioning optimization. |
| combined.probing.count | <0, .., n> | Amount of probes to be set in the circuit. For verification in the random combined model, setting the probe count to 0 specifies exhaustive probing. |
| combined.probing.samples | <0, .., n> | Amount of samples for random combined model without exhaustive probing. |
| combined.probing.glitches | {true, false} | Enable/disable glitches (threshold only). |
| combined.probing.copy-gates | {"none", "software", "hardware"} | Enable/disable insertion of copy gates. |
| combined.probing.probability | <0.0, .., 1.0> | Wire leakage probability (random only). |
| combined.faulting.enable | {true, false} | Enable/disable faults. |
| combined.faulting.count | <0, .., n> | Amount of faults to be inserted in the circuit. For verification in the random combined model, setting the fault count to 0 specifies all fault combinations. |
| combined.faulting.location | {"sequential", "combinational"} | Specifies whether faults are inserted into combinational or sequential gates. |
| combined.faulting.inputs | {true, false} | Enable/disable input faults. |
| combined.faulting.model | {"set", "reset", "bitflip"} | Specifies fault model, i.e., types of injected faults. |
| combined.faulting.probability | <0.0, .., 1.0> | Fault injection probability (random only). |
An example for a working and complete configuration can be found here.
----------------------------------------------------------------------------------------------------
CIA - COMBINED INDISTINGUISHABILITY ANALYSIS
Research Group on Computer-Aided Verification of Physical Security Properties (CAVE)
Armand Schinkel (armand.schinkel@rub.de),
Pascal Sasdrich (pascal.sasdrich@rub.de)
Copyright (c) 2026,
Armand Schinkel,
Pascal Sasdrich
All rights reserved.
----------------------------------------------------------------------------------------------------
TIME [s] SERVICE CONFIGURATION INFO: CELL LIBRARY
----------------------------------------------------------------------------------------------------
0.000 PARSER CELLLIB source: cell/nang45.txt
0.001 PARSER CELLLIB Parsed cell library with 14 gate type(s).
----------------------------------------------------------------------------------------------------
0.001 PARSER CELLLIB SUCCESS
TIME [s] SERVICE CONFIGURATION INFO: DESIGN UNDER TEST
----------------------------------------------------------------------------------------------------
0.019 PARSER VERILOG source: case-studies/01-gadgets/cini-cpc/design/and-cini-cpc-d1-k1.v
0.019 PARSER VERILOG module(s) : 1
0.019 PARSER VERILOG gate(s) : 96
0.019 PARSER VERILOG - comb. : 78
0.019 PARSER VERILOG - seq. : 18
0.019 PARSER VERILOG wire(s) : 113
0.019 PARSER VERILOG pin(s) : 332
0.019 PARSER VERILOG WARNING: detected 21 unconnected pins!
----------------------------------------------------------------------------------------------------
0.019 PARSER VERILOG SUCCESS
TIME [s] SERVICE CONFIGURATION INFO: ANNOTATIONS
----------------------------------------------------------------------------------------------------
0.023 PREPROCESSOR ANNOTATION 3 input wires were tagged as clock input.
0.023 PREPROCESSOR ANNOTATION WARNING: 2 wires could not be tagged as clock input in the MUT.
0.023 PREPROCESSOR ANNOTATION clock_3
...
0.027 PREPROCESSOR ANNOTATION io_o1_s3_d6
----------------------------------------------------------------------------------------------------
0.027 PREPROCESSOR ANNOTATION SUCCESS
TIME [s] SERVICE CONFIGURATION INFO
----------------------------------------------------------------------------------------------------
0.027 PREPROCESSOR MULTI-THREADING cores: 20
0.027 PREPROCESSOR MULTI-THREADING memory: 320 GB
----------------------------------------------------------------------------------------------------
0.027 PREPROCESSOR MULTI-THREADING SUCCESS
TIME [s] SERVICE CONFIGURATION INFO: MODEL POSTPROCESSING
----------------------------------------------------------------------------------------------------
0.028 PREPROCESSOR MODEL POSTPROCESSING Removed clock tree from netlist (3 wires were removed).
0.028 PREPROCESSOR MODEL POSTPROCESSING No control signals were found.
0.028 PREPROCESSOR MODEL POSTPROCESSING Removed 21 unconnected pins.
0.028 PREPROCESSOR MODEL POSTPROCESSING Removed 0 unconnected wires.
----------------------------------------------------------------------------------------------------
0.028 PREPROCESSOR MODEL POSTPROCESSING SUCCESS
TIME [s] SERVICE CONFIGURATION INFO: PROPERTIES
----------------------------------------------------------------------------------------------------
0.030 PREPROCESSOR MODEL PROPERTIES Determined 2 shared inputs.
0.030 PREPROCESSOR MODEL PROPERTIES Minimum number of shares: 2
0.030 PREPROCESSOR MODEL PROPERTIES Identified stage(s):
0.030 PREPROCESSOR MODEL PROPERTIES logic : 3
0.030 PREPROCESSOR MODEL PROPERTIES register : 2
----------------------------------------------------------------------------------------------------
0.030 PREPROCESSOR MODEL PROPERTIES SUCCESS
TIME [s] SERVICE CONFIGURATION INFO: PROBE/FAULT LOCATIONS
----------------------------------------------------------------------------------------------------
0.030 PREPROCESSOR PROBE/FAULT LOCATIONS Determined 180 probe positions.
----------------------------------------------------------------------------------------------------
0.030 PREPROCESSOR PROBE/FAULT LOCATIONS SUCCESS
TIME [s] SERVICE CONFIGURATION INFO: MODULE ELABORATION
----------------------------------------------------------------------------------------------------
0.153 PREPROCESSOR ELABORATE module : And_gate
0.153 PREPROCESSOR ELABORATE inputs : 14
0.153 PREPROCESSOR ELABORATE outputs : 6
0.153 PREPROCESSOR ELABORATE wires : 110
0.153 PREPROCESSOR ELABORATE Elaborated on core 0
----------------------------------------------------------------------------------------------------
0.153 PREPROCESSOR ELABORATE SUCCESS
TIME [s] SERVICE CONFIGURATION INFO: ANALYSIS REPORT
----------------------------------------------------------------------------------------------------
0.365 ANALYZER RANDOM COMBINED module : And_gate
0.365 ANALYZER RANDOM COMBINED probing :
0.365 ANALYZER RANDOM COMBINED probe locations : 180
0.365 ANALYZER RANDOM COMBINED sim. copy gates : hardware
0.366 ANALYZER RANDOM COMBINED leakage probability : p = 9.765625e-04
0.366 ANALYZER RANDOM COMBINED module (min.) : p = 2.852470e-03
0.366 ANALYZER RANDOM COMBINED module (max.) : p = 2.852470e-03
----------------------------------------------------------------------------------------------------
0.366 ANALYZER RANDOM COMBINED SUCCESS
TIME [s] SERVICE CONFIGURATION INFO
----------------------------------------------------------------------------------------------------
0.366 INDIANA COMBINED DONE!
The tool outputs information on each step of the workflow. Each type of information is labeled with a time stamp (relative to the execution start point), which service or component provided the information and which specific configuration the service or component used. The information itself depends on what configuration was used to run the tool. Generally, the tool first provides some information on the used cell library, circuit statistics, annotation info and properties (after postprocessing). The generally most relevant information about the verification results can be found under ANALYSIS REPORT, where the leakage probabilities are listed. The tool also notifies when it is done, as when partitioning is enabled, multiple analysis passes have to be executed.
Most of the examples in the repository are generated with Synopsis Design Compiler using the standard cell library NANG45. The following commands should be used for the synthesis script in order to generate a Verilog gate-level netlist that can be processed by VERICA.
set_dont_use [get_lib_cells NangateOpenCellLibrary/FA*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/HA*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/AOI*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/OAI*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/MUX*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/CLKBUF*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/OR3*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/OR4*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/OR5*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/NOR3*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/NOR4*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/NOR5*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/XNOR3*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/XNOR4*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/XNOR5*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/XOR3*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/XOR4*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/XOR5*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/AND3*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/AND4*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/AND5*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/NAND3*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/NAND4*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/NAND5*]
set_dont_use [get_lib_cells NangateOpenCellLibrary/BUF*]
Additionally, you can use the flowing commands to force the synthesizer to compile, keep the hierarchy and make a flattened netlist of the design.
compile -map_effort medium -area_effort medium
compile_ultra -no_autoungroup
ungroup -all -flatten
The license file can be found here.