VeriPRAC: Verifiable Formal Contracts for Secure Per Row Activation Counting

Rowhammer remains a major security concern for modern DRAM, yet no provably-secure deterministic solution has been deployed in commercial devices. To address this problem, the latest JEDEC DDR5 specification introduces Per Row Activation Counting (PRAC), a framework that combines per-row activation counters inside DRAM with a reactive mitigation protocol, called ALERT Back-Off (ABO) protocol. In principle, PRAC can comprehensively mitigate Rowhammer by detecting highly activated aggressor rows and refreshing their potential victims through ABO protocol, before bit flips occur.

However, PRAC specifies only the general framework, while leaving several security-critical design choices to the implementation of a mitigation. A PRAC implementation must decide what its per-row counters count, when those counters reset, and how critical rows are queued and selected for mitigation. Existing PRAC-based proposals make different choices and rely on ad hoc security analyses that do not necessarily capture the worst-case attack.

With VeriPRAC, we provide a formal and automated foundation for analyzing PRAC-based mitigations. VeriPRAC checks whether a concrete mitigation implementation provides the security guarantees that it claims. Our approach consists of three main components:

1. PRAC contracts, which formally specify the counting, resetting, queuing, and back-off mechanisms of a mitigation;
2. EchoTrail, a provably optimal attack structure for determining the security bound of PRAC contracts; and
3. VeriPRAC, an automated verification tool that tests a PRAC implementation against its intended contract.

Applying VeriPRAC to state-of-the-art PRAC mitigations shows that both MOAT and QPRAC violate their intended contracts. In the most severe case, VeriPRAC finds that an aggressor can reach up to 7,483 activations, despite the intended contract bounding it to only 99 activations.

What are Rowhammer and PRAC?

In a Rowhammer attack, an attacker repeatedly activates one or more aggressor rows, accelerating charge leakage in physically adjacent victim rows. If the cumulative hammer count of the victim row reaches the Rowhammer threshold ($R_\text{thresh}$) before the victim is refreshed, a bit flip may occur.

PRAC aims to detect such attacks by maintaining an activation counter for every DRAM row. Once a row’s counter reaches a critical activation threshold ($A_\text{thresh}$), the DRAM raises an ALERT signal. The memory controller then issues one or more Refresh Management (RFM) commands, giving the DRAM time to refresh the potential victim rows.

The JEDEC ALERT Back-Off (ABO) protocol controls this interaction. After an ALERT is raised, normal traffic can continue briefly before the RFM is issued (180ns). The protocol also requires a minimum number of activations before another ALERT can be raised. Consequently, even after a critical row is detected, additional rows can reach the threshold before the mitigation is completed, making the precise design of PRAC’s internal mechanisms security-critical.

Why PRAC needs formal contracts

The JEDEC specification defines the PRAC communication protocol, but it does not fully specify how a mitigation should implement its internal security mechanisms. We identify three major design choices:

1. Counting mechanism: A basic implementation counts only explicit ACT commands. A complete implementation also counts the implicit row activations caused by REF and RFM commands.
2. Counter resetting mechanism: Counters may reset only when a row is mitigated by PRAC, whenever its victim rows are naturally refreshed, or according to a coarser periodic policy. An imprecise resetting mechanism can silently discard activation history.
3. Queuing mechanism: When more critical rows exist than a single ALERT can mitigate, the implementation needs a service queue. The queue determines when to raise an ALERT and which rows are selected for mitigation.

We formalize a PRAC contract as $\text{PRAC}_c$:

$c=<Q|C|R|P>$

where Q, C, and R represent the queuing, counting, and resetting elements, and P represents the back-off protocol. The contract describes both the expected behavior of an implementation and its security bound, denoted by $A_\text{max}$: the maximum activation count that an optimal attacker can achieve on an aggressor row.

A concrete implementation satisfies its intended contract only if its worst-case activation bound is no higher than the contract’s intended bound. This provides a precise answer to the central verification question: does the implementation actually provide the security guarantee claimed by its design?

Reactive mitigations introduce silent survival strategies

Prior formal analyses focus on proactive mitigations, which periodically refresh the most heavily hammered rows. Because these mitigations are always active, an attacker must actively survive them, typically by hammering decoy rows alongside the target aggressor.

PRAC is fundamentally different. It is a reactive mitigation and raises an ALERT only after its internal state indicates that mitigation is necessary. Any gap between the state tracked by the PRAC contract and the actual activations occurring inside DRAM can therefore allow the attacker to silently continue hammering without triggering a mitigation.

We identify three new silent survival strategies, in addition to the conventional active decoy strategy:

1. Indirect activations: Under basic counting, activations induced by REF and RFM commands are not reflected in the PRAC counters. An attacker can therefore hammer a target aggressor indirectly while remaining invisible to the counting element.
2. Stealthy priming: If counters reset only when their rows are mitigated, the attacker can prepare many decoy rows at $A_\text{thresh}-1$ before the victim’s refresh window begins. These primed rows can later be used without consuming the attack’s limited activation budget.
3. Direct evasion: An imprecise queuing or ALERT-trigger mechanism may allow direct activations of the target aggressor to remain unmitigated. In an extreme case, a queue that raises an ALERT only when it becomes full can provide no security when the attacker repeatedly activates a single row.
4. Decoy activations: The attacker can also actively hammer decoy aggressors so that they are selected for mitigation instead of the target aggressor.

These strategies show why directly applying security arguments developed for proactive mitigations can underestimate the strongest attack against PRAC.

EchoTrail: a provably optimal attack structure

EchoTrail combines the applicable silent and active survival strategies into a unified attack structure. Depending on the PRAC contract, an EchoTrail attack consists of up to four phases:

1. A priming phase prepares the decoy aggressors, potentially before the victim’s refresh window;
2. A direct phase spends the most valuable activations directly on the target aggressor, up to the point at which further activations would trigger its mitigation;
3. An indirect phase uses mitigative refreshes to activate the target aggressor without increasing its tracked counter; and
4. A decoying phase continuously triggers mitigations while using primed decoys to keep the target aggressor alive until the end of the attack.

For each PRAC contract, EchoTrail determines which strategies are effective, their optimal ordering, and the optimal duration of every phase. We formally prove that the resulting EchoTrail configurations are optimal for the PRAC contracts considered in our work. This allows us to calculate mathematically proven security bounds instead of relying on ad hoc attack patterns.

VeriPRAC’s design

VeriPRAC turns the PRAC contract analysis and EchoTrail attack structure into an automated contract verification tool. Its design has three main components:

1. The verification engine systematically generates EchoTrail instances covering all applicable survival strategies and attack configurations;
2. The DRAM model executes each attack against the plugged-in PRAC implementation and precisely tracks all explicit and implicit aggressor activations; and
3. The PRAC implementation provides the concrete queuing, counting, and resetting mechanisms of the mitigation under test.

After executing all EchoTrail instances, VeriPRAC reports the maximum aggressor activation count and identifies the weakest contract satisfied by the implementation. It then compares this result with the intended contract. If the implementation permits a stronger attack than the intended contract, VeriPRAC reports a contract violation.

VeriPRAC is designed to make the integration of new PRAC implementations straightforward. A developer implements only the abstract functions corresponding to the mitigation’s queuing, counting, and resetting decisions. We provide step-by-step guidelines in our artifacts on how to integrate a custom PRAC implementation.

Verifying state-of-the-art PRAC mitigations

We integrate two state-of-the-art PRAC mitigations, MOAT (ASPLOS’25) and QPRAC (HPCA’25), into VeriPRAC. Our results show that neither implementation satisfies its intended contract.

MOAT

MOAT intends to use complete counting, where both direct ACT commands and the implicit activations induced by RFM commands are tracked. However, VeriPRAC finds that its effective security is equivalent to a weaker contract that performs only basic counting ( in the figure).

For example, with $A_\text{thresh}=64$, the original analysis reports an intended bound of 

$A_\text{max}(\text{MOAT})=99.$

VeriPRAC instead finds

$A_\text{max}(\text{MOAT})=7,483.$

The root cause is a subtle interaction between MOAT’s queuing and counting mechanisms. MOAT invalidates its queuing registers after mitigative RFMs, causing the queue to lose track of the implicit activations induced by those RFMs. In addition, counter increments caused by RFMs do not update the queuing registers (according to MOAT’s artefacts). As a result, a row can exceed the ALERT threshold without replacing the row currently stored in the queue.

VeriPRAC also makes the necessary fix clear: the implementation should avoid invalidating the queue upon mitigation and update the queuing registers for both direct and indirect activations.

QPRAC

QPRAC exhibits a smaller contract violation. For $A_\text{thresh}=512$, the original analysis reports

$A_\text{max}(\text{QPRAC})=542$

whereas VeriPRAC identifies

$A_\text{max}(\text{QPRAC})=567.$

QPRAC resets a counter only when the corresponding row is mitigated. This allows the attacker to prime decoy rows before the victim’s refresh window begins and then use the entire refresh window for the direct and decoying phases of EchoTrail. The original analysis instead assumes that decoy priming must occur within the same refresh window, leading to a sub-optimal security bound.

These findings demonstrate that even small and seemingly reasonable implementation choices can invalidate a PRAC mitigation’s claimed guarantees. VeriPRAC enables such flaws to be detected and corrected before the mitigation is deployed in future DRAM devices.

More information and artifacts

Our paper, VeriPRAC is now available and will be presented at the ACM CCS ’26 in The Hague, the Netherlands. Additionally, you can find the artifacts of our paper on GitHub and Zenodo, further supporting the community and future Rowhammer research by providing accessible and reusable tools for formal, automated security analysis.

FAQ

Does a contract violation necessarily mean that an attacker can immediately cause a bit flip?

A contract violation means that the implementation allows a larger worst-case aggressor activation count than its intended contract claims. Whether this reaches the physical Rowhammer threshold depends on the vulnerability of the DRAM device. However, configuring a mitigation using an incorrect bound (e.g., $A_\text{thresh}$) can leave a supposedly protected device vulnerable, which is why identifying the true $A_\text{max}$ is security-critical.

Can VeriPRAC be used for new PRAC mitigation proposals?

Yes. VeriPRAC provides modular interfaces for implementing the queuing, counting, and resetting mechanisms of a new mitigation. Its current guarantees apply to PRAC-based designs expressible using these contract elements and the JEDEC back-off protocol. A design that introduces fundamentally different mechanisms may require extending the contract formalization and deriving the corresponding EchoTrail configurations.

Can the flaws found by VeriPRAC be fixed?

Yes. For MOAT, VeriPRAC directly identifies the queuing behavior that causes the violation and suggests a straightforward repair: preserve the queue state across mitigative RFMs and update it for all direct and indirect activations. More generally, VeriPRAC allows debugging PRAC implementations, helping designers revise either the implementation or safely configure its claimed security bound before deployment.