Search papers, labs, and topics across Lattice.
This paper presents a formal analysis of probabilistic saturating counters (PSCs) using differential privacy to address vulnerabilities in classical saturating counters against side-channel attacks. By modeling PSCs and Prime+Probe attack strategies as probabilistic Moore machines, the authors derive optimal attack strategies and quantify the attacker's distinguishing power, demonstrating that their synthesized PSCs maintain competitive prediction performance while offering formal security guarantees. The results indicate that the proposed PSCs significantly enhance security without sacrificing utility, marking a critical advancement in branch predictor design.
Synthesized probabilistic saturating counters achieve formal differential privacy guarantees while maintaining competitive prediction accuracy, addressing critical side-channel vulnerabilities in modern processors.
Branch predictors improve instruction-level parallelism in modern processors and are commonly modeled using saturating counters. However, classical saturating counters are deterministic and thus vulnerable to side-channel attacks: an attacker can manipulate the counter state and infer the branch direction of a victim process. Probabilistic saturating counters (PSCs) have been proposed to mitigate this leakage by randomizing counter updates, but existing evaluations are mainly empirical. In this paper, we give a formal analysis based on differential privacy (DP): we model PSCs and the corresponding Prime+Probe attack strategies as probabilistic Moore machines, derive optimal attack strategies, and quantify the attacker's distinguishing power through DP. Our DP guarantee applies to the PSC primitive under the Prime+Probe observation model; end-to-end security for a full branch predictor under repeated or adaptive attacks is an important direction for future work. We then synthesize parameters for an enhanced PSC that satisfies a target pure DP guarantee. To evaluate utility, we derive the stationary misprediction rate and validate the theoretical predictions on benchmark programs. Compared to deterministic and existing probabilistic saturating counters, the synthesized PSCs provide formal security guarantees while preserving competitive prediction performance.
