AutoPRAC Finds 34-Undetected-Activation Flaw in MOAT Rowhammer Defense

34 activations can slip past a state-of-the-art Rowhammer defense without triggering a mitigative refresh. That’s exactly what AutoPRAC found in MOAT, a PRAC-based DDR5 protection design previously considered secure.

AutoPRAC is the first automated technique to test PRAC (Per-Row Activation Counting) defenses using model checkers. The researchers behind it model implementations as bounded state machines and check safety properties against a worst-case oracle attacker. If a property fails, AutoPRAC spits out a concrete counterexample trace - a working attack sequence.

What AutoPRAC Found in MOAT

MOAT’s counter-reset policy has a subtle timing gap. When the counter reaches a certain value and gets reset, the window for counting activations shifts in a way that an attacker can exploit. The model checker found this automatically. Human analysts had missed it.

The result: up to 34 activations above the Rowhammer threshold remain undetected. That’s not a theoretical corner case - it’s a concrete, executable attack trace generated by AutoPRAC.

Why This Matters for DDR5 Security

Current Rowhammer security evaluations rely on human-crafted attack patterns. That’s like testing a lock only with the keys you’ve already seen. AutoPRAC brings formal verification to the problem: if a property can be violated, the tool finds the shortest path to failure.

The approach is generic. It doesn’t just apply to MOAT - any PRAC implementation that can be modeled as a bounded state machine is fair game. The authors position AutoPRAC as an early-stage design aid, not a post-silicon patch tool.

The Practical Takeaway

AutoPRAC doesn’t replace hardware testing. It catches logic-level flaws before silicon spins. The MOAT flaw isn’t in the memory array - it’s in the control logic’s reset timing. That’s exactly the kind of bug that slips through human review and survives into production.

Expect PRAC verification to shift from hand-written attack sequences to automated model checking. AutoPRAC shows the path: one model checker, one counterexample, and a defense that looked solid suddenly has a 34-activation hole.

Source: AutoPRAC: Automating Attack Discovery for PRAC-Based Rowhammer Defenses using Model Checkers
Domain: arxiv.org