Hardware Private Cubic Circuits

This repository contains the source code for the paper "Hardware Private Cubic Circuits".

Requirements

To synthesize, test, and formally verify the hardware modules, the following tools are required: make, yosys, the yosys-slang plugin for Yosys, iverilog, sv2v and pypy3. The repository should be cloned with submodules, i.e., git clone --recursive https://github.com/ChairImpSec/HPCC.

Quickstart

On systems with Nix installed, you can load all the required dependencies using nix develop or run the following targets directly:

nix run .#syn # synthesises HPCC and S-Box d=1,d=2,d=3 in F_2 and F_(2^4)
nix run .#test # tests the synthesised designs
nix run .#verif # verifies HPCC using VerifMSI
nix run .#prolead-verif # statistically validates HPCC using PROLEAD

Note

Verification with VerifMSI may take a few hours up to a day on consumer hardware.

Warning

PROLEAD verification takes roughly 7 days and roughly 50 GiB of maximum RAM on a 128 core @ 3.10 GHz system.

HPCC

The HPCC module masked_hpcc_mul has the following generic parameters:

• The design is instantiated at the specified security_order, i.e. will operate on security_order + 1 shares.
• The design multiplies elements of size bit_width. Note that the appropriate field multiplier must be implemented in the generic_mul module.
• num_a_mults specifies how many $A$s should be multiplied with $B C$. Normally, this should be 1, but if you want to compute $A B C$ and $A' B C$ you can achieve this with num_a_mults = 2.
• make_bc_mult adds an extra output BC to the gadget which contains just the multiplication of $B$ and $C$.

The required randomness (in bit) is given by masked_hpcc_mul_package::hpcc_num_randoms(security_order, bit_width, num_a_mults, make_bc_mult).

The module can be synthesized to the desired parameters with make NUM_SHARES=4 BIT_WIDTH=4 NUM_A_MULTS=1 MAKE_BC_MULT=0 syn_masked_hpcc_mul. Note that you must provide the number of shares to the make invocation, not the security order.

A functional testbench can be run using make NUM_SHARES=4 BIT_WIDTH=4 test_masked_hpcc_mul.

The GE area of the design can be obtained from the stats folder, by diving the reported chip area for the module by 0.798, which is the size of a NAND gate in the NANG45 library.

2-Stage AES S-Box

The 2-stage AES S-Box (masked_2stage_aes_sbox) is largely based on the implementation given in Three-Stage-AES. Note that it does not take the security order as a parameter; it uses the number of shares instead.

The module can be synthesized to the desired parameters with make NUM_SHARES=4 syn_masked_2stage_aes_sbox and tested with make NUM_SHARES=4 test_masked_2stage_aes_sbox.

VerifMSI

The PINI property of HPCC can be formally verified to the desired parameters using VerifMSI with make BIT_WIDTH=1 NUM_SHARES=2 verif.

This requires that the repository is cloned with submodules using git clone --recursive https://github.com/ChairImpSec/HPCC. Submodules can be loaded after the initial clone using git submodule update --init --recursive.

PROLEAD

Statistical verification of HPCC and the AES S-Box was performed using PROLEAD.

The configurations, netlists and results are available in the prolead directory. They can be reproduced using ./prolead/run.sh <filename_basename> <top_module> as follows:

./prolead/run.sh masked_hpcc_mul_prolead_bw1_d1 masked_hpcc_mul_prolead
./prolead/run.sh masked_hpcc_mul_prolead_bw1_d2 masked_hpcc_mul_prolead
./prolead/run.sh masked_hpcc_mul_bw1_d3 masked_hpcc_mul
./prolead/run.sh masked_2stage_aes_sbox_d1 masked_2stage_aes_sbox
./prolead/run.sh masked_2stage_aes_sbox_d2 masked_2stage_aes_sbox

License

• HPCC is original work and is licensed under the MIT License.
• The implementation of the 2-stage AES SBOX using HPCC is a derivative work of https://github.com/vedadux/Three-Stage-AES, licensed under GPL-3.0. Thus, all code in rtl/common and rtl/masked_2stage_aes_sbox is licensed under GPL-3.0.