A practical testing framework for isolating hardware timing channels

This work identifies a new formal basis for hardware information flow security by providing a method to separate timing flows from other flows of information. By developing a framework for identifying these different classes of information flow at the gate-level, one can either confirm or rule out the existence of such flows in a provable manner. To demonstrate the effectiveness of our presented model, we discuss its usage on a practical example: a CPU cache in a MIPS processor written in Verilog HDL and simulated in a scenario which accurately models previous cache-timing attacks. We demonstrate how our framework can be used to isolate the timing channel used in these attacks.