[aes] Document that the DOM S-Box has been formally verified
Using Coco-Alma, the new version of the REBECCA tool, we have been able
to formally verify that our DOM S-Box is secure against first-order SCA.
Signed-off-by: Pirmin Vogel <vogelpi@lowrisc.org>
diff --git a/hw/ip/aes/rtl/aes_sbox_dom.sv b/hw/ip/aes/rtl/aes_sbox_dom.sv
index 6843e87..5ba037a 100644
--- a/hw/ip/aes/rtl/aes_sbox_dom.sv
+++ b/hw/ip/aes/rtl/aes_sbox_dom.sv
@@ -19,6 +19,14 @@
// [2] Canright, "A very compact 'perfectly masked' S-box for AES (corrected)" available at
// https://eprint.iacr.org/2009/011.pdf
// [3] Canright, "A very compact Rijndael S-box" available at https://hdl.handle.net/10945/25608
+//
+// Using the Coco-Alma tool in transient mode, this implementation has been formally verified to be
+// secure against first-order side-channel analysis (SCA). For more information on the tool,
+// refer to the following papers:
+// [4] Gigerl, "COCO: Co-design and co-verification of masked software implementations on CPUs"
+// available at https://eprint.iacr.org/2020/1294.pdf
+// [5] Bloem, "Formal verification of masked hardware implementations in the presence of glitches"
+// available at https://eprint.iacr.org/2017/897.pdf
///////////////////////////////////////////////////////////////////////////////////////////////////
// IMPORTANT NOTE: //
