This directory contains support files to formally verify the OTBN core using the tool Alma: Execution-aware Masking Verification.
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
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]
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 \ --cycles 25 \ --excluded-signals u_otbn_core.u_otbn_controller.rf_bignum_intg_err_i[0] \ --glitch-behavior loose \ --dbg-signals otbn_cycle_cnt_o \ --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