Module security 

Security Property Verification — Non-Interference

Hardware non-interference: two executions differing only in secret inputs must produce identical public outputs. Encoded as: (init_1 == init_2 on public) AND (secret_1 != secret_2) AND T_1 AND T_2 AND (public_out_1 != public_out_2) is UNSAT.

Structs

TaintedSignal

Enums

SecurityLabel

SecurityResult

Functions

check_non_interference

Check non-interference: public outputs independent of secret inputs.