Search papers, labs, and topics across Lattice.
This paper introduces AutoPRAC, an automated framework that utilizes model checkers to evaluate the security of Per-Row Activation Counting (PRAC) defenses against Rowhammer attacks. By modeling PRAC implementations as bounded state machines, AutoPRAC systematically checks for violations of critical safety properties under worst-case attack scenarios, revealing vulnerabilities that human-crafted patterns might miss. Notably, the framework identifies a significant flaw in the MOAT defense, allowing up to 34 activations to evade detection, underscoring the necessity for automated security validation in hardware defenses.
AutoPRAC uncovers hidden vulnerabilities in state-of-the-art Rowhammer defenses, revealing that even leading mitigations can fail under specific conditions.
Per-Row Activation Counting (PRAC) in DDR5 is a specification to mitigate Rowhammer attacks by tracking activations per row and triggering mitigative refreshes when needed. However, the security of PRAC designs is currently evaluated using human-crafted attack patterns and we lack formal verification of their security properties, or automated techniques to detect implementation flaws. In this work, we present AutoPRAC, the first automated technique to test the security of PRAC-based defenses using model checkers. AutoPRAC models PRAC implementations as bounded state machines and checks security-critical safety properties against a worst-case oracle attacker. If a property is violated, the framework produces a concrete counterexample trace corresponding to a successful attack. Using AutoPRAC, we uncover a previously unreported flaw in MOAT, a state-of-the-art PRAC defense, in its counter-reset policy that allows up to 34 activations to go undetected above the Rowhammer threshold. Our results demonstrate that AutoPRAC can automatically discover subtle security flaws in Rowhammer mitigations and serves as an early-stage design aid for attack discovery on PRAC designs.
