This directory contains support files to formally verify the masking employed inside AES unit using the tool Alma: Execution-aware Masking Verification.
Note that this flow is experimental. It has been developed using Yosys 0.9+4306 (git sha1 3931b3a03) and sv2v v0.0.9-24-gf868f06. Other tool versions might not be compatible.
Download the Alma tool
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
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
After downloading the Alma tool, installing dependencies and synthesizing AES, the masking can finally be formally verified.
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.
Enter the directory where you have downloaded Alma and load the virtual Python environment
source dev/bin/activate
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
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.
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
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
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
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
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.