Noninterference measurement quantifies the secret information that
might leak to an adversary from what the adversary can observe and
influence about the computation. Static and high-fidelity
noninterference measurement has been difficult to scale to complex
computations, however. This paper scales a recent framework for
noninterference measurement to the open-source RISC-V BOOM core as
specified in Verilog, through three key innovations: logically
characterizing the core's execution incrementally, applying specific
optimizations between each cycle; permitting information to be
declassified, to focus leakage measurement to only secret
information that cannot be inferred from the declassified
information; and interpreting leakage measurements for the analyst
in terms of simple rules that characterize when leakage occurs.
Case studies on cache-based side channels generally, and on specific
instances including \textsc{Spectre} attacks, show that the resulting
toolchain, called \textsc{DINoMe}, effectively scales to this modern
processor design.