# AES Formal Masking Verification Using Alma

This directory contains support files to formally verify the masking employed inside AES unit using the tool Alma: Execution-aware Masking Verification.

## Prerequisites

Note that since we are primarily interested in verifying the masking of a hardware implementation, we are using the hw-verif branch of the tool. In addition, we currently need to use a patched version of the tool, to work around a limitation.

git clone git@github.com:vogelpi/coco-alma.git alma -b fix-yosys-synth-template


The tip of this branch should be c8c7f67.

Enter the directory using

cd 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

2. 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/aes/pre_syn


Set up the synthesis flow as described in the corresponding README. Then, make sure to change the line in syn_setup.sh

export LR_SYNTH_TOP_MODULE=aes


to

export LR_SYNTH_TOP_MODULE=aes_sbox


to only synthesize an individual AES S-Box as formally verifying the entire AES unit or the AES cipher core is currently out of scope from a tool run time point of view. Alternatively, it is possible to verify aes_sub_bytes containing all 16 S-Boxes of the data path or even aes_reduced_round which besides the S-Boxes also includes the ShiftRows and MixColumns operations.

Then run the synthesis

./syn_yosys.sh


## Formally verifying the masking of the AES unit

1. Make sure to source the build_consts.sh script from the OpenTitan repository

source util/build_consts.sh


in order to set up some shell variables.

source dev/bin/activate

3. Launch the Alma tool to parse, 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/aes/pre_sca/alma/verify_aes.sh  This should produce output similar to the one below: Verifying aes_sbox using Alma File tmp/circuit.v already exists, do you want to overwrite it? (y/n) y Starting yosys synthesis... | CircuitGraph | Total: 1692 | Linear: 504 | Non-linear: 375 | Registers: 167 | Mux: 228 | parse.py successful (2.80s) 1: Running verilator on given netlist 2: Compiling verilated netlist library 3: Compiling provided verilator testbench 4: Simulating circuit and generating VCD | CircuitGraph | Total: 1692 | Linear: 504 | Non-linear: 375 | Registers: 167 | Mux: 228 | tmp/tmp.vcd:1286: [WARNING] Entry for name clk_i already exists in namemap (clk_i -> K,) tmp/tmp.vcd:1287: [WARNING] Entry for name data_i already exists in namemap (data_i -> L,) tmp/tmp.vcd:1288: [WARNING] Entry for name data_o already exists in namemap (data_o -> M,) tmp/tmp.vcd:1289: [WARNING] Entry for name en_i already exists in namemap (en_i -> N,) tmp/tmp.vcd:1381: [WARNING] Entry for name mask_i already exists in namemap (mask_i -> O,) tmp/tmp.vcd:1382: [WARNING] Entry for name mask_o already exists in namemap (mask_o -> P,) tmp/tmp.vcd:1383: [WARNING] Entry for name op_i already exists in namemap (op_i -> Q,) tmp/tmp.vcd:1384: [WARNING] Entry for name out_ack_i already exists in namemap (out_ack_i -> R,) tmp/tmp.vcd:1385: [WARNING] Entry for name out_req_o already exists in namemap (out_req_o -> S,) tmp/tmp.vcd:1386: [WARNING] Entry for name prd_i already exists in namemap (prd_i -> T,) tmp/tmp.vcd:1387: [WARNING] Entry for name rst_ni already exists in namemap (rst_ni -> U,) 0 0 Building formula for cycle 0: vars 0 clauses 0 Checking cycle 0: Building formula for cycle 1: vars 114 clauses 312 Checking cycle 1: Building formula for cycle 2: vars 3276 clauses 10534 Checking cycle 2: Checking probe (cycle 2, and _0436_[0]): 0.00 Checking probe (cycle 2, and _0378_[0]): 0.00 ... Checking probe (cycle 5, not gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_gamma1_gamma0.u_prim_xilinx_buf_mul_abx_z0.out_o[2]): 0.00 Checking probe (cycle 5, xor gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_gamma1_gamma0.u_prim_xilinx_buf_mul_abx_z0.out_o[3]): 0.00 Checking probe (cycle 5, mux _0914_[0]): 0.00 Checking probe (cycle 5, mux _0912_[0]): 0.00 Checking probe (cycle 5, mux _0925_[0]): 0.00 Checking probe (cycle 5, mux _0923_[0]): 0.00 Checking probe (cycle 5, mux _0945_[0]): 0.00 Checking probe (cycle 5, mux _0943_[0]): 0.00 Checking probe (cycle 5, mux _0898_[0]): 0.00 Checking probe (cycle 5, mux _0913_[0]): 0.00 Checking probe (cycle 5, mux _0911_[0]): 0.00 Checking probe (cycle 5, mux _0897_[0]): 0.00 Finished in 50.74 The execution is secure  By default, this script will verify the AES S-Box. But you can actually specify the top module to verify. For example, to verify a single, reduced AES round without AddKey operation, first re-run the Yosys synthesis with export LR_SYNTH_TOP_MODULE=aes_reduced_round  and then execute ${REPO_TOP}/hw/ip/aes/pre_sca/alma/verify_aes.sh aes_reduced_round


## Individual steps in detail

Below we outline the individual steps performed by the verify_aes.sh script. This is useful if you, e.g., want to verify the masking of your own module. For this how to, we focus on the most simple case, i.e., the formal verification of a single AES S-Box.

For more details, please refer to the Alma tutorial.

1. The first step involves the parsing the synthesized netlist.

./parse.py --top-module aes_sbox \
--source ${REPO_TOP}/hw/ip/aes/pre_syn/syn_out/latest/generated/aes_sbox.alma.v \ --netlist tmp/circuit.v --log-yosys  2. 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. Open the file and change the lines data_i [7:0] = unimportant mask_i [7:0] = unimportant prd_i [27:0] = unimportant  to data_i [7:0] = secret 7:0 mask_i [7:0] = secret 7:0 prd_i [27:0] = random  3. Then the Verilator testbench can be compiled and run required to identify control signals and the like ./trace.py --testbench${REPO_TOP}/hw/ip/aes/pre_sca/alma/cpp/verilator_tb_aes_sbox.cpp \
--netlist tmp/circuit.v -o tmp/circuit

4. Finally the verification of the masking implementation can be started.

./verify.py --json tmp/circuit.json \
--label tmp/labels.txt \
--top-module aes_sbox \
--vcd tmp/tmp.vcd \
--rst-name rst_ni --rst-phase 0 \
--probe-duration once --mode transient \
--glitch-behavior loose --cycles 6


## Details of the provided support files

• cpp: SystemVerilog testbench, instantiates and drives the synthesized netlist of the DUT.
• verify_aes.sh: Script to run the parse, trace and compile steps with one single command.