AutoPRAC: Automating Attack Discovery for PRAC-Based Rowhammer Defenses using Model Checkers
For hardware security researchers, AutoPRAC provides automated attack discovery for PRAC defenses, addressing the lack of formal verification in this domain.
AutoPRAC is the first automated technique using model checkers to test the security of PRAC-based Rowhammer defenses. It uncovered a previously unreported flaw in MOAT allowing up to 34 undetected activations above the Rowhammer threshold.
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.