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

  1. 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
    
  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

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

  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.

  2. Enter the directory where you have downloaded Alma and load the virtual Python environment

    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.