[hmac] Wipe secret assertions and spec update #25674
Conversation
martin-velay
commented
Dec 17, 2024
martin-velay
commented
- related to issue [hmac,dv] Various assertions #23563
- update spec to be aligned with the RTL
- add assertions to check the effect of wipe secret operation
- fix doc to be aligned with the RTL as the FSMs are not affected by the wipe secret triggering. But this is not a security issue. Signed-off-by: Martin Velay <[email protected]>
- 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]>
|
@andreaskurth, as discussed the doc update should fall into the |
| @@ -420,7 +420,7 @@ | |||
| { name: "WIPE_SECRET", | |||
| desc: '''Clear internal secret registers. | |||
|
|
|||
| If CPU writes a value into the register, the value is used to clear the internal variables such as the secret key, internal state machine, or hash value. | |||
| If CPU writes a value into the register, the value is used to clear the internal variables such as the secret key, intermediate hash results, digest and the internal message scheduling array. | |||
There was a problem hiding this comment.
This looks good but it might be worth fixing the grammar slightly since we're touching the line. We probably want an article before CPU ("If the CPU ..." or "If a CPU ...") and we've got a spare one before "internal". The sentence is trying to say that we use the value to clear some of the internal variables. Putting "the" in makes it sound like we're wiping the whole lot of them.
| // 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)}})) |
There was a problem hiding this comment.
I love the computed replication constant! (and it's neater than just putting in an integer. Nice!)
| // 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)}})) |
There was a problem hiding this comment.
I'd probably drop the ,1. That's the default behaviour of $past and it might be marginally more obvious? (Similarly in 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 | |||
There was a problem hiding this comment.
I don't think we need the ifndef VERILATOR around assertions like this? (I think it's needed in hmac.sv because of the use of property)
| @@ -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 | |||
There was a problem hiding this comment.
I'd probably make this more descriptive than prescriptive :-) Maybe "When wipe_secret is high, sensitive internal variables are cleared by ..." ?
