[hmac,dv] Wipe secret assertions

- add multiple assertions to ensure that the specified internal variables are cleared when a wipe secret operation is triggered. Signed-off-by: Martin Velay <[email protected]>
lowRISC · Dec 17, 2024 · 818af47 · 818af47
1 parent ee23638
commit 818af47
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 0 deletions.
diff --git a/hw/ip/hmac/rtl/hmac.sv b/hw/ip/hmac/rtl/hmac.sv
@@ -935,6 +935,11 @@ module hmac
   `ASSERT(ValidHmacEnConditionAssert,
           hmac_en != $past(hmac_en) |-> !in_process && !initiated)
 
+  // When wipe_secret is triggered, clear sensitive internal variables by extending the wipe
+  // value specifed in the register
+  `ASSERT(WipeSecretKeyAssert,
+          wipe_secret |=> (secret_key == {($bits(secret_key)/$bits(wipe_v)){$past(wipe_v,1)}}))
+
   // All outputs should be known value after reset
   `ASSERT_KNOWN(IntrHmacDoneOKnown, intr_hmac_done_o)
   `ASSERT_KNOWN(IntrFifoEmptyOKnown, intr_fifo_empty_o)

diff --git a/hw/ip/prim/rtl/prim_sha2.sv b/hw/ip/prim/rtl/prim_sha2.sv
@@ -178,6 +178,20 @@ module prim_sha2 import prim_sha2_pkg::*;
     // assign digest to output
     assign digest_o = digest_q;
 
+    `ifndef VERILATOR
+    `ifndef SYNTHESIS
+
+    // When wipe_secret is triggered, clear sensitive internal variables by extending the wipe
+    // value specifed in the register
+    `ASSERT(WipeHashAssert,
+            wipe_secret_i |=> (hash_q == {($bits(hash_q)/$bits(wipe_v_i)){$past(wipe_v_i,1)}}))
+    `ASSERT(WipeMsgSchArrAssert,
+            wipe_secret_i |=> (w_q == {($bits(w_q)/$bits(wipe_v_i)){$past(wipe_v_i,1)}}))
+    `ASSERT(WipeDigestAssert,
+            wipe_secret_i |=> (digest_q == {($bits(digest_q)/$bits(wipe_v_i)){$past(wipe_v_i,1)}}))
+
+    `endif // SYNTHESIS
+    `endif // VERILATOR
   end else begin : gen_256 // MultimodeEn = 0
     // datapath signal definitions for SHA-2 256 only
     sha_word32_t        shaf_rdata256;
@@ -264,6 +278,21 @@ module prim_sha2 import prim_sha2_pkg::*;
       assign digest_o[i][31:0]  = digest256_q[i];
       assign digest_o[i][63:32] = 32'b0;
     end
+
+    `ifndef VERILATOR
+    `ifndef SYNTHESIS
+
+    // When wipe_secret is triggered, clear sensitive internal variables by extending the wipe
+    // value specifed in the register
+    `ASSERT(WipeHashAssert,
+      wipe_secret_i |=> (hash256_q == {($bits(hash256_q)/$bits(wipe_v_i)){$past(wipe_v_i,1)}}))
+    `ASSERT(WipeMsgSchArrAssert,
+      wipe_secret_i |=> (w256_q == {($bits(w256_q)/$bits(wipe_v_i)){$past(wipe_v_i,1)}}))
+    `ASSERT(WipeDigestAssert,
+      wipe_secret_i |=> (digest256_q == {($bits(digest256_q)/$bits(wipe_v_i)){$past(wipe_v_i,1)}}))
+
+    `endif // SYNTHESIS
+    `endif // VERILATOR
   end
 
   // compute round counter (shared)