OTBN Formal Masking Verification Using Alma

This directory contains support files to formally verify the OTBN core using the tool Alma: Execution-aware Masking Verification.

Prerequisites

Note that this flow is experimental. It has been developed using Yosys v0.15 (this also works: v0.9+4306 (git sha1 3931b3a03)), sv2v v0.0.9-24-gf868f06 and Verilator 4.106 (2020-12-02 rev v4.106). Other tool versions might not be compatible.

Download the Alma tool from this specific repo and check out to the coco-otbn-latest branch of the tool
```
git clone git@github.com:abdullahvarici/coco-alma.git -b coco-otbn-latest
```
Enter the directory using
```
cd coco-alma
```
Set up a new virtual Python environment
```
python3 -m venv dev
source dev/bin/activate
```
And install the Python requirements
```
pip3 install -r requirements.txt
```
Update examples/otbn/config.json to point correct locations for asm, objdump and rv_objdump.
Generate a Verilog netlist

A netlist of the DUT can be generated using the Yosys synthesis flow from the OpenTitan repository. From the OpenTitan top level, run
```
cd hw/ip/otbn/pre_syn
```
Set up the synthesis flow as described in the corresponding README. Then run the synthesis
```
./syn_yosys.sh
```

Formally verifying the masking of the OTBN core

After downloading the Alma tool, installing dependencies and synthesizing OTBN, the masking can finally be formally verified.

Enter the directory where you have downloaded Alma and load the virtual Python environment.
```
source dev/bin/activate
```
Make sure to source the build_consts.sh script from the OpenTitan repository in order to set up some shell variables.
```
source ../opentitan/util/build_consts.sh
```

Launch the Alma tool to parse, assemble, trace (simulate) and formally verify the netlist. For simplicity, a single script is provided to launch all the required steps with a single command. Simply run:

${REPO_TOP}/hw/ip/otbn/pre_sca/alma/verify_otbn.sh

This should produce output similar to the one below:

Verifying OTBN using Alma
Starting yosys synthesis...
| CircuitGraph | Total: 234238 | Linear: 22351 | Non-linear: 107502 | Registers: 21338 | Mux: 41352 |
parse.py successful (755.32s)
INSTR_LIMIT =  128
Using program file:  programs/isw_and.S
Using build directory: [build_directory]
Using netlist path: ../../tmp/circuit.v
Wrote verilator testbench to [build_directory]/verilator_tb.c
It produces output VCD at [build_directory]/circuit.vcd
1: Running verilator on given netlist
2: Compiling verilated netlist library
3: Compiling provided verilator testbench
4: Simulating circuit and generating VCD
Line 0: WDR label found - u_otbn_core.u_otbn_rf_bignum.gen_rf_bignum_ff.u_otbn_rf_bignum_inner.rf [7800] = secret 0
Line 1: WDR label found - u_otbn_core.u_otbn_rf_bignum.gen_rf_bignum_ff.u_otbn_rf_bignum_inner.rf [7488] = secret 0
Line 2: WDR label found - u_otbn_core.u_otbn_rf_bignum.gen_rf_bignum_ff.u_otbn_rf_bignum_inner.rf [7176] = secret 1
Line 3: WDR label found - u_otbn_core.u_otbn_rf_bignum.gen_rf_bignum_ff.u_otbn_rf_bignum_inner.rf [6864] = secret 1
Line 4: WDR label found - u_otbn_core.u_otbn_rf_bignum.gen_rf_bignum_ff.u_otbn_rf_bignum_inner.rf [6552] = static_random
| CircuitGraph | Total: 234238 | Linear: 22351 | Non-linear: 107502 | Registers: 21338 | Mux: 41352 |
0 nodes are ignored.
tmp/circuit.vcd:57091: [WARNING] Entry for name clk_sys already exists in namemap (clk_sys -> #33)
tmp/circuit.vcd:57110: [WARNING] Entry for name imem_wdata_i already exists in namemap (imem_wdata_i -> $33)
tmp/circuit.vcd:57111: [WARNING] Entry for name imem_we_i already exists in namemap (imem_we_i -> &33)
tmp/circuit.vcd:57112: [WARNING] Entry for name imem_wmask_i already exists in namemap (imem_wmask_i -> \'33)
tmp/circuit.vcd:57116: [WARNING] Entry for name rst_sys_n already exists in namemap (rst_sys_n -> )33)
Waiting for initial delay cycles:  139
RST value:  1
1
Building formula for cycle 0:
vars 0 clauses 0
Checking cycle 0:
Checking secret 0 [1, 2]:
Checking secret 1 [3, 4]:
RST value:  1
1
Building formula for cycle 1:
vars 16 clauses 25
Checking cycle 1:
Checking secret 0 [17, 18]:
Checking secret 1 [19, 20]:
RST value:  1
1
Building formula for cycle 2:
vars 21103 clauses 57104
Checking cycle 2:
Checking secret 0 [21427, 21104]:
Checking secret 1 [21549, 21105]:
RST value:  1
1
Building formula for cycle 3:
vars 566836 clauses 1692708
Checking cycle 3:
Checking secret 0 [630522, 652105]:
Finished in 34.31
Writing a trace with the found error to [build_directory]/dbg-label-trace-0.txt
Writing a reduced circuit to [build_directory]/tmp/dbg-circuit-0.dot
The execution is not secure, here are some leaks:
leak 0: (cycle: 3, cell: mux _10580_[0], id: 223382)
3 stable  mux _10580_[0] vars   : ['s0:0', 's0:1']
3 stable  mux _10580_[0] signals: u_otbn_core.u_otbn_rf_bignum.gen_rf_bignum_ff.u_otbn_rf_bignum_inner.rf[7800] ^ u_otbn_core.u_otbn_rf_bignum.gen_rf_bignum_ff.u_otbn_rf_bignum_inner.rf[7488]

Individual steps in detail

Below we outline the individual steps performed by the verify_otbn.sh script. This is useful if you, e.g., want to verify the masking of your own module.

For more details, please refer to the Alma tutorial

Make sure to source the build_consts.sh script from the OpenTitan repository in order to set up some shell variables.
```
source ../opentitan/util/build_consts.sh
```

The first step involves the parsing of the synthesized netlist.

python3 parse.py --keep --top-module otbn_top_coco --log-yosys \
   --source ${REPO_TOP}/hw/ip/otbn/pre_sca/alma/rtl/ram_1p.v \
   ${REPO_TOP}/hw/ip/otbn/pre_syn/syn_out/latest/generated/otbn_core.alma.v \
   ${REPO_TOP}/hw/ip/otbn/pre_sca/alma/rtl/otbn_top_coco.v

Next, run the assemble.py script to generate memory initialization file for OTBN.

program=isw_and
cd examples/otbn
python3 assemble.py --program programs/${program}.S \
   --netlist ../../tmp/circuit.v
cd ../../

Then, the Verilator testbench can be compiled and run. This step is required to identify control signals.
```
python3 trace.py --testbench tmp/verilator_tb.c \
   --netlist tmp/circuit.v \
   --c-compiler gcc \
   --make-jobs 16
```
Add -b argument to use cached object files from a previous Verilator run and save some time.
Next, the automatically generated labeling file tmp/labels.txt needs to be adapted. This file tells Alma which inputs of the DUT correspond to the secret shares and which ones are used to provide randomness for (re-)masking. It is pretty tedious to compute the actual indices for bignum register file labels. Generate it with the following command:
```
examples/otbn/labels/generate_bignum_rf_labels.py \
   -i examples/otbn/labels/${program}_labels.txt \
   -o tmp/labels_updated.txt -w 1 -s 0
```

Finally the verification of the masking implementation can be started.

python3 verify.py --json tmp/circuit.json \
   --top-module otbn_top_coco \
   --label tmp/labels_updated.txt \
   --vcd tmp/circuit.vcd \
   --checking-mode per-location \
   --rst-name rst_sys_n \
   --rst-phase 0 \
   --rst-cycles 2 \
   --init-delay 139 \
   --excluded-signals u_otbn_core.u_otbn_controller.rf_bignum_intg_err_i[0] \
   --dbg-signals otbn_cycle_cnt_o \
   --cycles 25 \
   --mode stable

Run the following command to see the waveform:

gtkwave tmp/circuit.vcd

Run the following command to see the circuit diagramm if there is a leakage:

xdot tmp/dbg-circuit-0.dot

Formally verifying the mask accelerator interface modules

After completing the prerequisites above, source the build constants, activate the Alma virtual environment and run verify_sec_add.sh with the desired gadget:

cd ${REPO_TOP}
source util/build_consts.sh
cd ~/alma
source dev/bin/activate
${REPO_TOP}/hw/ip/otbn/pre_sca/alma/verify_sec_add.sh <gadget>

where <gadget> is one of hpc2, hpc2o, hpc3, hpc3o, or sec_add. The script runs all steps (parse, label, trace, verify) automatically, using the synthesized netlist from syn_out/latest/generated/.

A passing verification produces output similar to the following (shown for hpc3):

Verifying prim_hpc3_sca_wrapper using Alma
Starting yosys synthesis...
| CircuitGraph | Total:   35 | Linear:    6 | Non-linear:    4 | Registers:    6 | Mux:    6 |
parse.py successful (1.62s)
1: Running verilator on given netlist
2: Compiling verilated netlist library
3: Compiling provided verilator testbench
4: Simulating circuit and generating VCD
| CircuitGraph | Total:   35 | Linear:    6 | Non-linear:    4 | Registers:    6 | Mux:    6 |
Building formula for cycle 0: vars 0 clauses 0
Checking cycle 0:
Building formula for cycle 1: vars 0 clauses 0
Checking cycle 1:
Building formula for cycle 2: vars 114 clauses 178
Checking cycle 2:
Checking probe (cycle 2, xor sum_o[0]): 0.00
Checking probe (cycle 2, xor sum_o[1]): 0.00
...
Finished in 0.01
The execution is secure

For hpc2, Alma reports a leak due to false positives. Alma’s verification approach based on approximated Fourier coefficients is sound but not complete, meaning it can report leaks that do not exist in practice (see Gigerl et al.). The output looks as follows:

Verifying prim_hpc2_sca_wrapper using Alma
Starting yosys synthesis...
| CircuitGraph | Total:   51 | Linear:    6 | Non-linear:    6 | Registers:   14 | Mux:   11 |
parse.py successful (1.40s)
1: Running verilator on given netlist
2: Compiling verilated netlist library
3: Compiling provided verilator testbench
4: Simulating circuit and generating VCD
| CircuitGraph | Total:   51 | Linear:    6 | Non-linear:    6 | Registers:   14 | Mux:   11 |
Building formula for cycle 0: vars 0 clauses 0
Checking cycle 0:
Building formula for cycle 1: vars 0 clauses 0
Checking cycle 1:
Building formula for cycle 2: vars 78 clauses 81
Checking cycle 2:
Building formula for cycle 3: vars 165 clauses 233
Checking cycle 3:
Checking probe (cycle 3, xor sum_o[0]): 0.00
Finished in 0.01
The execution is not secure, here are some leaks:
leak 0: (cycle: 3, cell: xor sum_o[0], id: 10)
3 stable xor sum_o[0] vars   : ['s1:0', 's1:1']
3 stable xor sum_o[0] signals: share0_i[1] ^ share1_i[1]
3 trans  xor sum_o[0] vars   : ['s1:0', 's1:1']
3 trans  xor sum_o[0] signals: share0_i[1] ^ share1_i[1]

The design can still be verified using PROLEAD, where the leakage analysis passes successfully. For this, please follow the PROLEAD README.

If a leak is found, generate a PNG of the leaking circuit with:

xdot ./tmp/dbg-circuit-0.dot