[aes, pre_sca] Enable formal masking verification of AES with Alma
This commit adds a couple of support files and a how to for formal
verifying the masking employed inside AES using the Alma tool.
Signed-off-by: Pirmin Vogel <vogelpi@lowrisc.org>
diff --git a/hw/ip/aes/pre_sca/alma/README.md b/hw/ip/aes/pre_sca/alma/README.md
new file mode 100644
index 0000000..efcc2ac
--- /dev/null
+++ b/hw/ip/aes/pre_sca/alma/README.md
@@ -0,0 +1,176 @@
+# 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](https://github.com/IAIK/coco-alma).
+
+## 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.
+ ```sh
+ 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
+ ```sh
+ cd alma
+ ```
+ Set up a new virtual Python environment
+ ```sh
+ python3 -m venv dev
+ source dev/bin/activate
+ ```
+ And install the Python requirements
+ ```sh
+ pip3 install -r requirements.txt
+ ```
+
+1. 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
+ ```sh
+ 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`
+ ```sh
+ export LR_SYNTH_TOP_MODULE=aes
+ ```
+ to
+ ```sh
+ 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.
+
+ Then run the synthesis
+ ```sh
+ ./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
+ ```sh
+ source util/build_consts.sh
+ ```
+ in order to set up some shell variables.
+
+1. Enter the directory where you have downloaded Alma and load the virtual
+ Python environment
+ ```sh
+ source dev/bin/activate
+ ```
+
+1. 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
+ ```sh
+ ${REPO_TOP}/hw/ip/aes/pre_sca/alma/verify_aes.sh
+ ```
+ This should produce output similar to the one below:
+ ```sh
+ 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
+ ```
+
+## 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](https://github.com/IAIK/coco-alma/tree/hw-verif#usage).
+
+1. The first step involves the parsing the synthesized netlist.
+ ```sh
+ ./parse.py --top-module aes_sbox \
+ --source ${REPO_TOP}/hw/ip/aes/pre_syn/syn_out/latest/generated/aes_sbox.pre_map.v \
+ --netlist tmp/circuit.v --log-yosys
+ ```
+
+1. Then the Verilator testbench can be compiled and run required to identify
+ control signals and the like
+ ```sh
+ ./trace.py --testbench ${REPO_TOP}/hw/ip/aes/pre_sca/alma/cpp/verilator_tb_aes_sbox.cpp \
+ --netlist tmp/circuit.v -o tmp/circuit
+ ```
+
+1. Finally the verification of the masking implementation can be started.
+
+ ```sh
+ ./verify.py --json tmp/circuit.json \
+ --label ${REPO_TOP}/hw/ip/aes/pre_sca/alma/labels/aes_sbox.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.
+- `labels`: Contains the labeling files telling Alma which inputs of the DUT
+ correspond to the secret shares and which ones are used to provide randomness
+ for (re-)masking.
+- `verify_aes.sh`: Script to run the parse, trace and compile steps with
+ one single command.
diff --git a/hw/ip/aes/pre_sca/alma/cpp/testbench.h b/hw/ip/aes/pre_sca/alma/cpp/testbench.h
new file mode 100644
index 0000000..a002d59
--- /dev/null
+++ b/hw/ip/aes/pre_sca/alma/cpp/testbench.h
@@ -0,0 +1,73 @@
+// Copyright lowRISC contributors.
+// Copyright IAIK.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+#ifndef OPENTITAN_HW_IP_AES_PRE_SCA_ALMA_CPP_TESTBENCH_H_
+#define OPENTITAN_HW_IP_AES_PRE_SCA_ALMA_CPP_TESTBENCH_H_
+
+#include "verilated.h"
+#include "verilated_vcd_c.h"
+
+template <class Module>
+struct Testbench {
+ unsigned long m_tickcount;
+ Module m_core;
+ VerilatedVcdC *m_trace = NULL;
+
+ Testbench() {
+ Verilated::traceEverOn(true);
+ m_tickcount = 0ul;
+ }
+
+ ~Testbench() { closetrace(); }
+
+ void opentrace(const char *vcdname) {
+ if (!m_trace) {
+ m_trace = new VerilatedVcdC;
+ m_core.trace(m_trace, 99);
+ m_trace->open(vcdname);
+ }
+ }
+
+ void closetrace() {
+ if (m_trace) {
+ m_trace->close();
+ delete m_trace;
+ m_trace = NULL;
+ }
+ }
+
+ void reset() {
+ m_core.rst_ni = 0;
+ this->tick();
+ this->tick();
+ m_core.rst_ni = 1;
+ }
+
+ void tick() {
+ // Falling edge
+ m_core.clk_i = 0;
+ m_core.eval();
+ if (m_trace)
+ m_trace->dump(20 * m_tickcount);
+
+ // Rising edge
+ m_core.clk_i = 1;
+ m_core.eval();
+ if (m_trace)
+ m_trace->dump(20 * m_tickcount + 10);
+
+ // Falling edge settle eval
+ m_core.clk_i = 0;
+ m_core.eval();
+
+ if (m_trace)
+ m_trace->flush();
+ m_tickcount++;
+ }
+
+ bool done() { return Verilated::gotFinish(); }
+};
+
+#endif // OPENTITAN_HW_IP_AES_PRE_SCA_ALMA_CPP_TESTBENCH_H_
diff --git a/hw/ip/aes/pre_sca/alma/cpp/verilator_tb_aes_sbox.cpp b/hw/ip/aes/pre_sca/alma/cpp/verilator_tb_aes_sbox.cpp
new file mode 100644
index 0000000..61468f2
--- /dev/null
+++ b/hw/ip/aes/pre_sca/alma/cpp/verilator_tb_aes_sbox.cpp
@@ -0,0 +1,39 @@
+// Copyright lowRISC contributors.
+// Copyright IAIK.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+#include <stdio.h>
+
+#include "Vcircuit.h"
+#include "testbench.h"
+
+int main(int argc, char **argv) {
+ Verilated::commandArgs(argc, argv);
+ Testbench<Vcircuit> tb;
+ tb.opentrace("tmp.vcd");
+
+ tb.reset();
+
+ // Data signals - we don't really care about the data fed to the module.
+ // The whole tracing is really just about control signals.
+ tb.m_core.data_i = 0x12;
+ tb.m_core.mask_i = 0x34;
+ tb.m_core.prd_i = 0x56789AB;
+
+ // Control signals
+ tb.m_core.op_i = 0; // encrypt
+ tb.m_core.out_ack_i = 0;
+
+ tb.m_core.en_i = 0;
+ tb.tick();
+ tb.m_core.en_i = 1;
+ tb.tick();
+
+ while (tb.m_core.out_req_o != 1) {
+ tb.tick();
+ }
+ tb.tick();
+
+ tb.closetrace();
+}
diff --git a/hw/ip/aes/pre_sca/alma/labels/aes_sbox.txt b/hw/ip/aes/pre_sca/alma/labels/aes_sbox.txt
new file mode 100644
index 0000000..20ca272
--- /dev/null
+++ b/hw/ip/aes/pre_sca/alma/labels/aes_sbox.txt
@@ -0,0 +1,37 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+# inputs:
+clk_i = unimportant
+rst_ni = unimportant
+en_i = unimportant
+out_ack_i = unimportant
+op_i = unimportant
+data_i [7:0] = secret 7:0
+mask_i [7:0] = secret 7:0
+prd_i [7:0] = random
+# registers:
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.prd_q [27:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.count_q [2:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_prim_xilinx_flop_ab_y10.q_o [15:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_prim_xilinx_flop_ab_y_ss.q_o [7:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_mul_y1_y0.u_prim_xilinx_flop_abxz0_z1.q_o [7:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_mul_theta_y1.u_prim_xilinx_flop_abq_z0.q_o [7:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_mul_y1_y0.u_prim_xilinx_flop_ab_yz0.q_o [7:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_mul_theta_y0.u_prim_xilinx_flop_abq_z0.q_o [7:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_prim_xilinx_flop_ab_gamma10.q_o [7:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_prim_xilinx_flop_ab_gamma_ss.q_o [3:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_mul_y1_y0.gen_pipeline.u_prim_xilinx_flop_ab_xy.q_o [15:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_mul_theta_y0.gen_pipeline.u_prim_xilinx_flop_mul_abx_aby.q_o [7:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_mul_theta_y1.gen_pipeline.u_prim_xilinx_flop_mul_abx_aby.q_o [7:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_omega_gamma1.u_prim_xilinx_flop_ab_yz0.q_o [3:0] = unimportant
+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_flop_ab_yz0.q_o [3:0] = unimportant
+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_flop_abxz0_z1.q_o [3:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_omega_gamma0.u_prim_xilinx_flop_abxz0_z1.q_o [3:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_omega_gamma1.u_prim_xilinx_flop_abxz0_z1.q_o [3:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_omega_gamma0.u_prim_xilinx_flop_ab_yz0.q_o [3:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_omega_gamma0.gen_pipeline.u_prim_xilinx_flop_ab_xy.q_o [7:0] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_omega_gamma1.gen_pipeline.u_prim_xilinx_flop_ab_xy.q_o_reg[7] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_omega_gamma1.gen_pipeline.u_prim_xilinx_flop_ab_xy.q_o_reg[4] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_omega_gamma1.gen_pipeline.u_prim_xilinx_flop_ab_xy.q_o_reg[5] = unimportant
+gen_sbox_masked.gen_sbox_dom.u_aes_sbox.u_aes_dom_inverse_gf2p8.u_aes_dom_inverse_gf2p4.u_aes_dom_mul_omega_gamma1.gen_pipeline.u_prim_xilinx_flop_ab_xy.q_o_reg[6] = unimportant
diff --git a/hw/ip/aes/pre_sca/alma/verify_aes.sh b/hw/ip/aes/pre_sca/alma/verify_aes.sh
new file mode 100755
index 0000000..f5e62a5
--- /dev/null
+++ b/hw/ip/aes/pre_sca/alma/verify_aes.sh
@@ -0,0 +1,30 @@
+#!/bin/bash
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# Script to formally verify the masking of the AES unit using Alma.
+
+set -e
+
+export TOP_MODULE=aes_sbox
+
+echo "Verifying ${TOP_MODULE} using Alma"
+
+# Parse
+./parse.py --top-module ${TOP_MODULE} \
+--source ${REPO_TOP}/hw/ip/aes/pre_syn/syn_out/latest/generated/${TOP_MODULE}.pre_map.v \
+--netlist tmp/circuit.v --log-yosys
+
+# Trace
+./trace.py --testbench ${REPO_TOP}/hw/ip/aes/pre_sca/alma/cpp/verilator_tb_${TOP_MODULE}.cpp \
+--netlist tmp/circuit.v -o tmp/circuit
+
+# Verify
+./verify.py --json tmp/circuit.json \
+ --label ${REPO_TOP}/hw/ip/aes/pre_sca/alma/labels/${TOP_MODULE}.txt \
+ --top-module ${TOP_MODULE} \
+ --vcd tmp/tmp.vcd \
+ --rst-name rst_ni --rst-phase 0 \
+ --probe-duration once --mode transient \
+ --glitch-behavior loose --cycles 6
diff --git a/util/licence-checker.hjson b/util/licence-checker.hjson
index bd4bb3a..d99b53c 100644
--- a/util/licence-checker.hjson
+++ b/util/licence-checker.hjson
@@ -60,5 +60,8 @@
'sw/otbn/crypto/rsa_verify_3072.s',
# Mersenne Twister PRNG
'sw/device/sca/lib/prng.c',
+ # Alma testbench files
+ 'hw/ip/aes/pre_sca/alma/cpp/testbench.h',
+ 'hw/ip/aes/pre_sca/alma/cpp/verilator_tb_aes_sbox.cpp',
],
}
