The implementation of L-alert in code

[zsxpdsyz]

Hello authors：

I have read your paper and code, but I have some questions about the consistency between the description of L-alert in the text and its implementation in the code.

In the article, l-alert is described as being triggered if secret information can propagate to architectural registers. However, in the code implementation, as I understand it, the code aims to prove that in this design, either a misprediction must have occurred, or the instruction corresponding to root_id was killed, or the sequence of instructions committed by the ROB (i.e., the sequence of valid signals) is equal. This seems to not use architectural registers as a security property.

SecureBOOM/Properties/upec_checker.vli

Lines 190 to 191 in d147382

	prove:
	at t+O: (!(mispred_happened_1 && mispred_happened_2) && (!root_id_killed && !root_id_already_killed) && (ROB_commit_array_1[commit_index] != ROB_commit_array_2[commit_index])) == 1'b0;

Best regards