AutoPRAC: Automating Attack Discovery for PRAC-Based Rowhammer Defenses using Model Checkers

Gururaj Saileshwar; Joyce Qu

arxiv: 2606.23905 · v1 · pith:PNTV2TTRnew · submitted 2026-06-22 · 💻 cs.CR

AutoPRAC: Automating Attack Discovery for PRAC-Based Rowhammer Defenses using Model Checkers

Joyce Qu , Gururaj Saileshwar This is my paper

Pith reviewed 2026-06-26 07:35 UTC · model grok-4.3

classification 💻 cs.CR

keywords AutoPRACPRACRowhammermodel checkingMOATcounter-reset policyDDR5security verification

0 comments

The pith

AutoPRAC uses model checkers on bounded state machines to find a flaw in MOAT that permits up to 34 undetected activations above the Rowhammer threshold.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

AutoPRAC is an automated technique that models PRAC implementations as bounded state machines and verifies their security properties against a worst-case attacker oracle using model checkers. When a safety property fails, the system produces a concrete counterexample trace that corresponds to a successful attack sequence. Applied to the state-of-the-art MOAT defense, this process identifies an unreported flaw in the counter-reset policy. A sympathetic reader would care because current PRAC security evaluations rely on manual attack patterns, and this approach replaces them with systematic, automated detection of implementation flaws.

Core claim

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, a previously unreported flaw is uncovered in MOAT's counter-reset policy that allows up to 34 activations to go undetected above the Rowhammer threshold.

What carries the argument

Bounded state-machine model of a PRAC implementation checked by a model checker against a worst-case attacker oracle to detect violations of safety properties and generate counterexample attack traces.

If this is right

PRAC designs can be checked for security properties before hardware implementation rather than after.
Subtle flaws in counter-reset logic become detectable without relying on human-crafted attack patterns.
Concrete attack traces can be produced automatically to demonstrate specific violations.
Model checking serves as an early-stage design aid that flags issues in PRAC mitigations.
Security evaluation of future PRAC variants can be performed systematically rather than manually.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same modeling approach could apply to other per-row tracking mechanisms in emerging DRAM standards.
Design teams could run AutoPRAC-style checks as part of routine verification flows to catch reset-policy errors early.
The 34-activation gap points to a broader need for tighter coupling between activation thresholds and reset conditions in any counter-based defense.
Automated trace generation may shorten the time between defense proposal and discovery of its edge-case weaknesses.

Load-bearing premise

The bounded state-machine model of the PRAC implementation and the worst-case attacker oracle accurately capture the behaviors that matter for real hardware security.

What would settle it

Running the concrete counterexample trace generated by AutoPRAC on actual DDR5 hardware implementing MOAT and observing that it fails to produce 34 undetected activations above the Rowhammer threshold.

Figures

Figures reproduced from arXiv: 2606.23905 by Gururaj Saileshwar, Joyce Qu.

**Figure 3.** Figure 3: MOAT’s counter reset policy on refresh [ [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

AutoPRAC automates attack discovery on PRAC defenses and surfaces a counter-reset issue in MOAT, but the finding rests on an unvalidated model of the hardware.

read the letter

AutoPRAC is the first attempt to use model checkers to hunt for attacks on PRAC Rowhammer mitigations instead of relying on hand-written patterns, and it reports a flaw in MOAT's counter-reset policy that lets 34 activations go undetected. That is the main point.

The authors model the defense as a bounded state machine and run it against a worst-case attacker oracle. When a safety property fails, the tool returns a concrete trace. This is a clear improvement over manual search for this class of defenses, and the framework is described plainly enough that others could adapt it.

The soft spot is exactly the one flagged in the stress test. The 34-activation result only matters if the state machine matches the actual DDR5 PRAC counter-reset behavior in the spec and in silicon. The abstract gives no evidence of cross-checking the model against the JEDEC document, a vendor implementation, or cycle-accurate RTL. Without that step, it is hard to know whether the discovered trace would work on real hardware or is an artifact of how the reset transitions were encoded. State-space size and bounding choices are also not discussed, so the completeness of the search is unclear.

The paper is for hardware-security researchers who evaluate memory mitigations and for people who want to apply formal tools to similar low-level policies. A reader already working on Rowhammer or formal verification of hardware would get practical value from the method, once the modeling assumptions are tightened.

It deserves peer review. The core idea is useful and the concrete output makes it worth referee time, even if the current version needs more work on model validation before the specific MOAT claim can be trusted.

Referee Report

1 major / 0 minor

Summary. The paper presents AutoPRAC, an automated framework that models PRAC-based Rowhammer defenses as bounded state machines and uses model checkers to verify security properties against a worst-case attacker oracle. If a property is violated, it produces a concrete counterexample trace. The central result is the discovery of a previously unreported flaw in MOAT's counter-reset policy that permits up to 34 activations above the Rowhammer threshold to go undetected.

Significance. If the models are faithful to the implementations, AutoPRAC supplies a systematic, automated method for finding subtle flaws in hardware mitigations that goes beyond manual attack construction. The production of falsifiable counterexample traces is a concrete strength that could aid early-stage PRAC design.

major comments (1)

[Abstract and modeling description] Abstract and modeling section: The headline claim of a flaw allowing 34 undetected activations rests entirely on the accuracy of the bounded state-machine model of MOAT's counter-reset policy. No independent validation is reported (e.g., direct comparison to the JEDEC DDR5 PRAC specification, a vendor reference implementation, or cycle-accurate RTL simulation) confirming that the modeled reset transitions match actual hardware behavior.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for highlighting the need for explicit model validation. We address this concern directly below and will revise the manuscript accordingly.

read point-by-point responses

Referee: [Abstract and modeling description] Abstract and modeling section: The headline claim of a flaw allowing 34 undetected activations rests entirely on the accuracy of the bounded state-machine model of MOAT's counter-reset policy. No independent validation is reported (e.g., direct comparison to the JEDEC DDR5 PRAC specification, a vendor reference implementation, or cycle-accurate RTL simulation) confirming that the modeled reset transitions match actual hardware behavior.

Authors: Our MOAT model is constructed strictly from the counter-reset policy described in the original MOAT publication. The 34-activation counterexample is produced by the specific reset logic (periodic reset on a subset of rows without full activation tracking) as stated in that work. Because MOAT is a proposed algorithmic defense rather than a deployed RTL implementation, cycle-accurate simulation against vendor hardware is not feasible. We will add an appendix that (1) enumerates every state transition in our bounded model with a direct citation to the corresponding sentence in the MOAT paper and (2) cross-references the modeled behavior against the JEDEC DDR5 PRAC specification for the aspects that overlap. This mapping will allow independent verification of fidelity without requiring unavailable RTL. revision: yes

Circularity Check

0 steps flagged

No circularity; result is model-checker counterexample on independently constructed FSM

full rationale

The paper's central claim is the discovery of a counter-reset flaw in MOAT via AutoPRAC, which produces a concrete attack trace from an external model checker (NuSMV or similar) run on a bounded state-machine model of the PRAC implementation. No equations, fitted parameters, or self-citations appear as load-bearing steps in the derivation. The modeling step is an explicit construction of the FSM from the PRAC specification, and the output (the 34-activation trace) is not equivalent to any input by construction. The result is therefore self-contained against the model checker as an external oracle.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that the abstract state-machine model is faithful to hardware; no free parameters or invented physical entities are introduced.

axioms (1)

domain assumption The bounded state-machine abstraction of PRAC logic and the worst-case attacker oracle faithfully represent relevant hardware behaviors for security analysis.
Invoked when the framework is described as modeling PRAC implementations to check safety properties.

pith-pipeline@v0.9.1-grok · 5728 in / 1251 out tokens · 22049 ms · 2026-06-26T07:35:18.592491+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

19 extracted references · 6 canonical work pages

[1]

(2024) JESD79-5C

JEDEC. (2024) JESD79-5C. https://www.jedec.org/document_search?search_api_ views_fulltext=jesd79-5c

2024
[2]

Flipping bits in memory without accessing them: an experimental study of dram disturbance errors,

Y. Kim, R. Daly, J. Kim, C. Fallin, J. H. Lee, D. Lee, C. Wilkerson, K. Lai, and O. Mutlu, “Flipping bits in memory without accessing them: an experimental study of dram disturbance errors, ” inProceeding of the 41st Annual International Symposium on Computer Architecuture, ser. ISCA ’14. IEEE Press, 2014, p. 361–372

2014
[3]

Panopticon: A complete in-dram rowhammer mitigation,

T. Bennett, S. Saroiu, A. Wolman, and L. Cojocar, “Panopticon: A complete in-dram rowhammer mitigation, ” inWorkshop on DRAM Security (DRAMSec), 2021

2021
[4]

Qprac: Towards secure and practical prac-based rowhammer mitigation using priority queues,

J. Woo, S. C. Lin, P. J. Nair, A. Jaleel, and G. Saileshwar, “Qprac: Towards secure and practical prac-based rowhammer mitigation using priority queues, ” in2025 IEEE International Symposium on High Performance Computer Architecture (HPCA), 2025, pp. 1021–1037

2025
[5]

Moat: Securely mitigating rowhammer with per-row activation counters,

M. Qureshi and S. Qazi, “Moat: Securely mitigating rowhammer with per-row activation counters, ” inProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1, ser. ASPLOS ’25. New York, NY, USA: Association for Computing Machinery, 2025, p. 698–714. [Online]. Available: https://d...

work page doi:10.1145/3669940.3707278 2025
[6]

Un- derstanding the security benefits and overheads of emerging industry solutions to dram read disturbance,

O. Canpolat, A. G. Yağlıkçı, G. F. Oliveira, A. Olgun, O. Ergin, and O. Mutlu, “Un- derstanding the security benefits and overheads of emerging industry solutions to dram read disturbance, ” inWorkshop on DRAM Security (DRAMSec), 2024

2024
[7]

Chronus: Understanding and securing the cutting-edge industry solutions to dram read disturbance,

O. Canpolat, A. G. Yağlıkçı, G. F. Oliveira, A. Olgun, N. Bostanci, I. E. Yüksel, H. Luo, O. Ergin, and O. Mutlu, “Chronus: Understanding and securing the cutting-edge industry solutions to dram read disturbance, ”2025 IEEE International Symposium on High Performance Computer Architecture (HPCA), pp. 887–905, 2025. [Online]. Available: https://api.semanti...

2025
[8]

Mopac: Efficiently mitigating rowhammer with probabilistic activation counting,

S. Vittal, S. Qazi, P. Das, and M. Qureshi, “Mopac: Efficiently mitigating rowhammer with probabilistic activation counting, ” inProceedings of the 52nd Annual International Symposium on Computer Architecture, ser. ISCA ’25. New York, NY, USA: Association for Computing Machinery, 2025, p. 723–738. [Online]. Available: https://doi.org/10.1145/3695053.3730997

work page doi:10.1145/3695053.3730997 2025
[9]

Counterpoint: One-hot counting for prac-based rowhammer mitigation,

S.-L. Lu, J. Woo, and P. J. Nair, “Counterpoint: One-hot counting for prac-based rowhammer mitigation, ”DRAMSec, 2025

2025
[10]

Per-row activation counting on real hardware: Demystifying performance overheads,

J. Kim, S. Baek, M. Wi, H. Nam, M. J. Kim, S. Lee, K. Sohn, and J. H. Ahn, “Per-row activation counting on real hardware: Demystifying performance overheads, ”IEEE Computer Architecture Letters, 2025

2025
[11]

CBMC: C bounded model checker,

Diffblue, “CBMC: C bounded model checker, ” https://github.com/diffblue/cbmc
[12]

Pensieve: Microarchitectural modeling for security evaluation,

Y. Yang, T. Bourgeat, S. Lau, and M. Yan, “Pensieve: Microarchitectural modeling for security evaluation, ” inProceedings of the 50th Annual International Symposium on Computer Architecture, ser. ISCA ’23. New York, NY, USA: Association for Computing Machinery, 2023. [Online]. Available: https: //doi.org/10.1145/3579371.3589094

work page doi:10.1145/3579371.3589094 2023
[13]

Ramulator 2.0: A modern, modular, and extensible dram simulator,

H. Luo, Y. C. Tuğrul, F. N. Bostancı, A. Olgun, A. G. Yağlıkçı, and O. Mutlu, “Ramulator 2.0: A modern, modular, and extensible dram simulator, ”IEEE Computer Architecture Letters, vol. 23, no. 1, pp. 112–116, 2024

2024
[14]

CaDiCaL: Simplified long clause solver,

A. Biere, “CaDiCaL: Simplified long clause solver, ” https://github.com/arminbiere/ cadical. 6
[15]

The model checker SPIN,

G. J. Holzmann, “The model checker SPIN, ”IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279–295, 1997. [Online]. Available: https://doi.org/10.1109/32.588521

work page doi:10.1109/32.588521 1997
[16]

Salt: Track-and-mitigate subarrays, not rows, for blast-radius-free rowhammer defense,

M. K. Qureshi, “Salt: Track-and-mitigate subarrays, not rows, for blast-radius-free rowhammer defense, ” in2026 IEEE International Symposium on High Performance Computer Architecture (HPCA), 2026, pp. 1–16

2026
[17]

Pvac: A rowhammer mitigation architecture exploiting per-victim-row counting,

J. Kim, S. Baek, H. Nam, M. Wi, N. S. Kim, and J. H. Ahn, “Pvac: A rowhammer mitigation architecture exploiting per-victim-row counting, ” 2026. [Online]. Available: https://arxiv.org/abs/2604.20576

Pith/arXiv arXiv 2026
[18]

Rowpress: Amplifying read disturbance in modern dram chips,

H. Luo, A. Olgun, A. G. Yağlıkçı, Y. C. Tuğrul, S. Rhyner, M. B. Cavlak, J. Lindegger, M. Sadrosadati, and O. Mutlu, “Rowpress: Amplifying read disturbance in modern dram chips, ” inProceedings of the 50th Annual International Symposium on Computer Architecture, ser. ISCA ’23. New York, NY, USA: Association for Computing Machinery, 2023. [Online]. Availab...

work page doi:10.1145/3579371.3589063 2023
[19]

Columndisturb: Understanding column-based read disturbance in real dram chips and implications for future systems,

I. E. Yuksel, A. Olgun, N. Bostanci, H. Luo, A. G. Yaglikci, and O. Mutlu, “Columndisturb: Understanding column-based read disturbance in real dram chips and implications for future systems, ” inProceedings of the 58th IEEE/ACM International Symposium on Microarchitecture, ser. MICRO ’25. New York, NY, USA: Association for Computing Machinery, 2025, p. 97...

work page doi:10.1145/3725843.3756022 2025

[1] [1]

(2024) JESD79-5C

JEDEC. (2024) JESD79-5C. https://www.jedec.org/document_search?search_api_ views_fulltext=jesd79-5c

2024

[2] [2]

Flipping bits in memory without accessing them: an experimental study of dram disturbance errors,

Y. Kim, R. Daly, J. Kim, C. Fallin, J. H. Lee, D. Lee, C. Wilkerson, K. Lai, and O. Mutlu, “Flipping bits in memory without accessing them: an experimental study of dram disturbance errors, ” inProceeding of the 41st Annual International Symposium on Computer Architecuture, ser. ISCA ’14. IEEE Press, 2014, p. 361–372

2014

[3] [3]

Panopticon: A complete in-dram rowhammer mitigation,

T. Bennett, S. Saroiu, A. Wolman, and L. Cojocar, “Panopticon: A complete in-dram rowhammer mitigation, ” inWorkshop on DRAM Security (DRAMSec), 2021

2021

[4] [4]

Qprac: Towards secure and practical prac-based rowhammer mitigation using priority queues,

J. Woo, S. C. Lin, P. J. Nair, A. Jaleel, and G. Saileshwar, “Qprac: Towards secure and practical prac-based rowhammer mitigation using priority queues, ” in2025 IEEE International Symposium on High Performance Computer Architecture (HPCA), 2025, pp. 1021–1037

2025

[5] [5]

Moat: Securely mitigating rowhammer with per-row activation counters,

M. Qureshi and S. Qazi, “Moat: Securely mitigating rowhammer with per-row activation counters, ” inProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1, ser. ASPLOS ’25. New York, NY, USA: Association for Computing Machinery, 2025, p. 698–714. [Online]. Available: https://d...

work page doi:10.1145/3669940.3707278 2025

[6] [6]

Un- derstanding the security benefits and overheads of emerging industry solutions to dram read disturbance,

O. Canpolat, A. G. Yağlıkçı, G. F. Oliveira, A. Olgun, O. Ergin, and O. Mutlu, “Un- derstanding the security benefits and overheads of emerging industry solutions to dram read disturbance, ” inWorkshop on DRAM Security (DRAMSec), 2024

2024

[7] [7]

Chronus: Understanding and securing the cutting-edge industry solutions to dram read disturbance,

O. Canpolat, A. G. Yağlıkçı, G. F. Oliveira, A. Olgun, N. Bostanci, I. E. Yüksel, H. Luo, O. Ergin, and O. Mutlu, “Chronus: Understanding and securing the cutting-edge industry solutions to dram read disturbance, ”2025 IEEE International Symposium on High Performance Computer Architecture (HPCA), pp. 887–905, 2025. [Online]. Available: https://api.semanti...

2025

[8] [8]

Mopac: Efficiently mitigating rowhammer with probabilistic activation counting,

S. Vittal, S. Qazi, P. Das, and M. Qureshi, “Mopac: Efficiently mitigating rowhammer with probabilistic activation counting, ” inProceedings of the 52nd Annual International Symposium on Computer Architecture, ser. ISCA ’25. New York, NY, USA: Association for Computing Machinery, 2025, p. 723–738. [Online]. Available: https://doi.org/10.1145/3695053.3730997

work page doi:10.1145/3695053.3730997 2025

[9] [9]

Counterpoint: One-hot counting for prac-based rowhammer mitigation,

S.-L. Lu, J. Woo, and P. J. Nair, “Counterpoint: One-hot counting for prac-based rowhammer mitigation, ”DRAMSec, 2025

2025

[10] [10]

Per-row activation counting on real hardware: Demystifying performance overheads,

J. Kim, S. Baek, M. Wi, H. Nam, M. J. Kim, S. Lee, K. Sohn, and J. H. Ahn, “Per-row activation counting on real hardware: Demystifying performance overheads, ”IEEE Computer Architecture Letters, 2025

2025

[11] [11]

CBMC: C bounded model checker,

Diffblue, “CBMC: C bounded model checker, ” https://github.com/diffblue/cbmc

[12] [12]

Pensieve: Microarchitectural modeling for security evaluation,

Y. Yang, T. Bourgeat, S. Lau, and M. Yan, “Pensieve: Microarchitectural modeling for security evaluation, ” inProceedings of the 50th Annual International Symposium on Computer Architecture, ser. ISCA ’23. New York, NY, USA: Association for Computing Machinery, 2023. [Online]. Available: https: //doi.org/10.1145/3579371.3589094

work page doi:10.1145/3579371.3589094 2023

[13] [13]

Ramulator 2.0: A modern, modular, and extensible dram simulator,

H. Luo, Y. C. Tuğrul, F. N. Bostancı, A. Olgun, A. G. Yağlıkçı, and O. Mutlu, “Ramulator 2.0: A modern, modular, and extensible dram simulator, ”IEEE Computer Architecture Letters, vol. 23, no. 1, pp. 112–116, 2024

2024

[14] [14]

CaDiCaL: Simplified long clause solver,

A. Biere, “CaDiCaL: Simplified long clause solver, ” https://github.com/arminbiere/ cadical. 6

[15] [15]

The model checker SPIN,

G. J. Holzmann, “The model checker SPIN, ”IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279–295, 1997. [Online]. Available: https://doi.org/10.1109/32.588521

work page doi:10.1109/32.588521 1997

[16] [16]

Salt: Track-and-mitigate subarrays, not rows, for blast-radius-free rowhammer defense,

M. K. Qureshi, “Salt: Track-and-mitigate subarrays, not rows, for blast-radius-free rowhammer defense, ” in2026 IEEE International Symposium on High Performance Computer Architecture (HPCA), 2026, pp. 1–16

2026

[17] [17]

Pvac: A rowhammer mitigation architecture exploiting per-victim-row counting,

J. Kim, S. Baek, H. Nam, M. Wi, N. S. Kim, and J. H. Ahn, “Pvac: A rowhammer mitigation architecture exploiting per-victim-row counting, ” 2026. [Online]. Available: https://arxiv.org/abs/2604.20576

Pith/arXiv arXiv 2026

[18] [18]

Rowpress: Amplifying read disturbance in modern dram chips,

H. Luo, A. Olgun, A. G. Yağlıkçı, Y. C. Tuğrul, S. Rhyner, M. B. Cavlak, J. Lindegger, M. Sadrosadati, and O. Mutlu, “Rowpress: Amplifying read disturbance in modern dram chips, ” inProceedings of the 50th Annual International Symposium on Computer Architecture, ser. ISCA ’23. New York, NY, USA: Association for Computing Machinery, 2023. [Online]. Availab...

work page doi:10.1145/3579371.3589063 2023

[19] [19]

Columndisturb: Understanding column-based read disturbance in real dram chips and implications for future systems,

I. E. Yuksel, A. Olgun, N. Bostanci, H. Luo, A. G. Yaglikci, and O. Mutlu, “Columndisturb: Understanding column-based read disturbance in real dram chips and implications for future systems, ” inProceedings of the 58th IEEE/ACM International Symposium on Microarchitecture, ser. MICRO ’25. New York, NY, USA: Association for Computing Machinery, 2025, p. 97...

work page doi:10.1145/3725843.3756022 2025