Identifying Potential Timing Leakages from Hardware Design with Precondition Synthesis
摘要
Computer systems operate on hardware that does not execute in constant time. Timing leakage, which refers to information leakage through this timing variability, enables even remote attackers to steal secrets from production systems. The significance of timing leakage necessitates mechanisms to identify, understand, and prevent potential timing leakage at design time for hardware modules. This work proposes a mechanism that automatically identifies potential timing leakages from hardware design by synthesizing the precondition that confines the timing channel. Our mechanism, LeakSynth, obtains this precondition by gathering examples of initial states exhibiting variable or constant execution times. Specifically, LeakSynth synthesizes the predicate that distinguishes these examples and interprets it to produce a precondition under which the hardware module’s timing leakage is confined to a subset of its internal registers. Our evaluation using nine hardware modules, including four processors, demonstrates that LeakSynth can quickly synthesize the preconditions. We also show that the preconditions can be used to automatically produce annotations for existing constant-time verification tools. Not to mention that such annotations must be written manually without the help of LeakSynth, the automatically generated annotations are more relaxed, i.e., encompass more initial states.