Navigating Homomorphic Evaluation through Gates and Lookups

Overview

HELM is a framework for evaluating synthesizable HDL designs in the encrypted domain that is designed for multi-core CPU evaluation. Users can choose between evaluating circuits composed of standard Boolean gates, low-precision LUTs, or high-precision arithmetic operations. In all cases, both sequential and combinational circuits are supported with the exception of arithmetic circuits (which only support combinational logic).

How to cite this work

The preprint can be accessed here; you can cite this work as follows:

@Misc{EPRINT:GouMouTso23helm,
    author       = "Charles Gouert and
                    Dimitris Mouris and
                    Nektarios Georgios Tsoutsos",
    title        = "{HELM: Navigating Homomorphic Encryption through Gates and Lookup Tables}",
    year         = 2023,
    howpublished = "Cryptology ePrint Archive, Paper 2023/1382",
    note         = "\url{https://eprint.iacr.org/2023/1382}",
}

Build & Run

1) Clone, build, and run the tests:

git clone --recurse-submodules git@github.com:TrustworthyComputing/helm.git
cd helm
cargo build --release
cargo test --release

1.B) Optionally run all CPU + GPU tests:

cargo test --features gpu --release

2) HELM Command Line Arguments

  -v, --verilog <FILE>              Verilog input file to evaluate
  -w, --input-wires <STRING> <STRING> <[NUM]> Input wire values (-w wire1 value1 [width1] -w wire2 value2 [width2]...)
  -i, --input-wires-file <FILE>     CSV file that contains the input wire values (wire, value)
  -o, --output-wires-file <FILE>    CSV file to write the output wires (wire, value)
  -c, --cycles <NUMBER>             Number of cycles for sequential circuits [default: 1]
  -a, --arithmetic <TYPE>           Precision for arithmetic mode [possible values: u8, u16, u32, u64, u128]
  -p, --verbose                     Turn verbose printing on
  -h, --help                        Print help

3) HELM Modes of Operation

HELM has three modes: "gates"-mode, "LUTs"-mode, and "Arithmetic"-mode. HELM automatically distinguishes between LUTs and gates circuit depending on the cells utilized in the structural Verilog. Below are two examples:

3.1) Gates/Boolean Mode

Example in "gates"-mode:

cargo run --bin helm --release -- \
    --verilog ./hdl-benchmarks/processed-netlists/s27.v
cargo run --bin helm --release -- \
    --verilog ./hdl-benchmarks/processed-netlists/2-bit-adder.v \
    --input-wires-file ./hdl-benchmarks/test-cases/2-bit-adder.inputs.csv

You can also pass the input wire values as:

cargo run --bin helm --release -- \
    --verilog ./hdl-benchmarks/processed-netlists/2-bit-adder.v \
    -w a[0] 1 -w a[1] 0 -w b[0] 0 -w b[1] 1 -w cin 0

Or equivalently as wire_name hex_value wire_width

cargo run --bin helm --release -- \
    --verilog ./hdl-benchmarks/processed-netlists/2-bit-adder.v \
    -w a 1 2 -w b[0] 0 -w b[1] 1 -w cin 0

The above expands a to a[0] = 1 and a[1] = 1.

Similarly:

cargo run --bin helm --release -- \
    --verilog ./hdl-benchmarks/processed-netlists/2-bit-adder.v \
    -w a 1 2 -w b 2 2 -w cin 0

3.2) Lookup Tables (LUT) Mode

Example in "LUTs"-mode:

cargo run --bin helm --release -- \
    --verilog ./hdl-benchmarks/processed-netlists/8-bit-adder-lut-3-1.v \
    --input-wires-file hdl-benchmarks/test-cases/8-bit-adder.inputs.csv

3.3) Arithmetic Mode

Example of an Arithmetic circuit. This mode operates directly on behavioral Verilog files that include only arithmetic operations. There is no need to invoke Yosys to perform any logic synthesis.

cargo run --bin preprocessor --release  \
    --manifest-path=./hdl-benchmarks/Cargo.toml --  \
    --input ./hdl-benchmarks/designs/chi_squared.v \
    --output ./hdl-benchmarks/processed-netlists/chi_squared_arith.v \
    --arithmetic
cargo run --bin helm --release -- --arithmetic u32 \
    --verilog ./hdl-benchmarks/processed-netlists/chi_squared_arith.v \
    --input-wires-file ./hdl-benchmarks/test-cases/chi_squared_arith_1.inputs.csv

Example of an ISCAS'85 circuit

If a circuit is in the netlists directory but not in the processed-netlists, run the preprocessor and then helm as following:

cargo run --bin preprocessor --release  \
    --manifest-path=./hdl-benchmarks/Cargo.toml --  \
    --input ./hdl-benchmarks/netlists/c880.v \
    --output ./hdl-benchmarks/processed-netlists/c880.v
cargo run --bin helm --release -- --verilog ./hdl-benchmarks/processed-netlists/c880.v

Acknowledgments

This work was supported by the National Science Foundation (Award #2239334).