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