VeriPRAC (CCS 2026 Artifact)

VeriPRAC is an artifact for evaluating formal PRAC contracts using EchoTrail attack instances. It takes compact PRAC contract descriptions as input, automatically generates the EchoTrail instance, runs the instance against a PRAC-based mitigation, and reports the largest row activation count that the attack can achieve.

The repository supports two reproducibility tracks from the paper:

1. EchoTrail theoretical computations for Figures 8, 10, and 12.
2. VeriPRAC Figure 15 plots covering M_basic, MOAT, and QPRAC.

---

Table of Contents

• All Commands in a Glance
• System Requirements
• Directory Layout
• Build
• Reproduce Paper Figures
  • Figures 8, 10, and 12: EchoTrail Formulas
  • Figure 15: Contract Satisfaction
• Configuration Files
• Contract Format
• Outputs
• Adding a New Mitigation Plugin
• Troubleshooting
• Citation

---

All Commands in a Glance

Assumes CMake, a C++17 compiler, Python 3, NumPy, and Matplotlib are installed.

# 1) Install Python plotting/formula dependencies
python3 -m pip install numpy matplotlib

# 2) Build VeriPRAC
mkdir -p build
cd build
cmake ..
make
cd ..

# 3) Reproduce Figures 8, 10, and 12
python3 scripts/reproduce_formula_figures.py \
  --output-dir output/formula-figures

# 4) Reproduce Figure 15 VeriPRAC plots
./scripts/run-basic-mitigation-sweep.sh
./build/veriprac configs/moat.json
./build/veriprac configs/qprac.json

For MOAT and QPRAC, the terminal output and veriprac-satisfaction.csv report whether the intended contract is satisfied or violated.

---

System Requirements

VeriPRAC has no special hardware requirements. It is a software model and does not run Rowhammer attacks on real memory.

Validated setup:

• OS: macOS and Linux
• Compiler: any C++17-compatible compiler
• CMake: 3.16 or newer
• Python: Python 3

Python packages:

python3 -m pip install numpy matplotlib

The C++ JSON dependency is vendored under external/, so no C++ package manager is required.

---

Directory Layout

.
|-- src/                         # VeriPRAC C++ source
|   |-- base/                    # EchoTrail contracts, results, timing specifications
|   |-- dram_model/              # DRAM command/timing model
|   |-- mitigation/              # Generic mitigation interface and plugins
|   `-- verifier/                # Contract loading, execution, aggregation
|-- configs/                     # Contract files and mitigation run configs
|-- scripts/                     # Contract generation and plotting scripts
|-- external/                    # Vendored dependencies
|-- output/                      # Generated outputs
|-- CMakeLists.txt
`-- README.md

---

Build

Build from the repository root:

mkdir -p build
cd build
cmake ..
make
cd ..

The executable is written to:

build/veriprac

For faster iteration over only the 128 and 1024 thresholds:

./build/veriprac configs/basic-mitigation-smoke.json
./build/veriprac configs/moat-smoke.json
./build/veriprac configs/qprac-smoke.json

---

Reproduce Paper Figures

Figures 8, 10, and 12: EchoTrail Formulas

Figures 8, 10, and 12 are theoretical EchoTrail results.

Run:

python3 scripts/reproduce_formula_figures.py \
  --output-dir output/formula-figures

Main outputs:

output/formula-figures/figure8a-prac-base-heatmap.pdf
output/formula-figures/figure8b-prac-base-breakdown.pdf
output/formula-figures/figure10a-prac-fine-metrics.pdf
output/formula-figures/figure10b-prac-fine-breakdown.pdf
output/formula-figures/figure12-all-contracts.pdf

The script also writes:

output/formula-figures/all-configs.csv
output/formula-figures/sanity-check-symmetric.csv

By default, this script uses the following ALERT thresholds:

64, 128, 256, 512, 1024, 2048, 4096, 8192, 16368, 32768

To regenerate the JSON contracts used by VeriPRAC for Figure 15:

python3 scripts/generate_contracts.py \
  --thresholds 32,64,128,256,512,1024,2048 \
  --output configs/contracts-all.json \
  --summary-csv output/generated-contracts-summary.csv

Figure 15: Contract Satisfaction

Figure 15 is produced by running EchoTrail contract instances against the implemented mitigations. M_basic reports the VeriPRAC weakest bound directly; MOAT and QPRAC additionally compare the weakest bound with the implementation's intended bound.

Run M_basic:

./scripts/run-basic-mitigation-sweep.sh

Run MOAT:

./build/veriprac configs/moat.json

Run QPRAC:

./build/veriprac configs/qprac.json

The outputs are written to:

output/basic-mitigation/
output/moat/
output/qprac/

Each directory contains the raw CSV files, the all-contracts plot, and the weakest-contract plot. MOAT and QPRAC also write the intended-vs-VeriPRAC contract satisfaction plot.

---

Configuration Files

The run configuration is a JSON file passed as the only argument to the veriprac executable:

./build/veriprac configs/qprac.json

Example:

{
  "totalRows": 65536,
  "timingParameters": "TimingParametersDDR5PRAC",
  "contractsFile": "configs/contracts-all.json",
  "outputDirectory": "output/qprac",
  "generatePlots": true,
  "mitigationType": "QPRAC",
  "dram_debug": false,
  "engine_debug": true,
  "mitigation_debug": false,
  "intendedContract": {
    "bounds": {
      "32": 71,
      "64": 101,
      "128": 163,
      "256": 288,
      "512": 542,
      "1024": 1052,
      "2048": 2073
    }
  }
}

Fields:

• totalRows: number of DRAM rows available for automatic row allocation.
• timingParameters: DRAM timing model. Current public configs use TimingParametersDDR5PRAC.
• contractsFile: compact EchoTrail contract collection.
• outputDirectory: directory where CSV files and plots are written.
• generatePlots: set to false to generate CSV files only.
• mitigationType: mitigation plugin selected by the factory.
• dram_debug, engine_debug, mitigation_debug: debug verbosity controls.
• intendedContract: optional claim to check after VeriPRAC identifies the weakest contract.

Built-in mitigation names:

• BasicMitigation
• MOAT
• QPRAC

BasicMitigation implements the baseline M_basic design from the paper: basic counting, fine resetting, and an ideal unlimited priority queue. MOAT models the original vulnerable MOAT behavior: complete counting and fine resetting, but RFM-induced activations do not update the queue and mitigation completion invalidates the queued state. QPRAC uses complete counting, a 4-entry priority queue, and an onMitigation counter resetting.

Intended Contracts

VeriPRAC supports two styles of intended contract.

Name-based claim:

{
  "intendedContract": "PRAC-complete"
}

This is satisfied at a threshold when the named family is one of the weakest families found by VeriPRAC. Exact ties satisfy all tied families.

Explicit-bound claim:

{
  "intendedContract": {
    "bounds": {
      "64": 99,
      "128": 183,
      "1024": 1079
    }
  }
}

This is satisfied when VeriPRAC's weakest maximum ACT count is less than or equal to the provided bound at each threshold. Missing bounds are reported as unsatisfied.

---

Contract Format

Contracts are stored in JSON files such as configs/contracts-all.json. Each entry describes one EchoTrail instance. Contract files provide counts and phase parameters only; VeriPRAC generates the target, trigger, and decoy rows automatically.

Example:

{
  "name": "PRAC-coarse",
  "Athresh": 128,
  "num_decoys": 26581,
  "indirect_rounds": 0,
  "num_decoys1": 24590.1165,
  "num_decoys2": 1991.3248
}

Semantics:

• name: contract family label.
• Athresh: mitigation ALERT threshold for this instance.
• num_decoys: total number of decoy rows. The target row is additional.
• indirect_rounds: number of indirect EchoTrail rounds.
• num_decoys1, num_decoys2: optional split between two EchoTrail decoying segments (e.g., needed for PRAC-coarse contracts).
• direct_activations: optional shared direct-phase target ACT count. Defaults to Athresh - 1. Direct-only contracts such as PRAC-fifoQ set this to the computed number of target activations feasible in one refresh window.
• direct_activations1, direct_activations2: optional per-segment overrides for the direct target ACT counts.

Counts are floored. If the split fields are missing, VeriPRAC uses:

num_decoys1 = num_decoys
num_decoys2 = 0

The floored split counts must add up to the floored total. VeriPRAC then generates one target row, one adjacent trigger row for indirect activation, and the required distinct decoy rows automatically.

Row selection is deterministic. VeriPRAC places rows in cyclic refresh order and consumes decoys that are closer to their natural refresh deadline earlier in the decoying phase.

---

Outputs

Every verification run writes:

• veriprac-results.csv: one row per contract instance.
• veriprac-weakest.csv: weakest contract family per threshold.
• veriprac-contracts.pdf: threshold versus maximum-ACT plot for all contract families.
• veriprac-contracts.svg: editable vector version of the same plot.
• veriprac-weakest-contract.pdf: threshold versus the VeriPRAC weakest maximum-ACT bound.
• veriprac-weakest-contract.svg: editable vector version of the same plot.

If intendedContract is configured, the run also writes:

• veriprac-satisfaction.csv: satisfaction/violation table.
• veriprac-intended-contract.pdf: VeriPRAC weakest bound versus intended bound.
• veriprac-intended-contract.svg: editable vector version of the same plot.

The weakest contract at a threshold is the family whose EchoTrail instance achieves the highest global physical activation count. VeriPRAC also prints a per-contract progress table to the terminal when engine_debug is enabled.

---

Adding a New Mitigation Plugin

Mitigations are implemented as C++ plugins under:

src/mitigation/plugin/

The DRAM model is mitigation-generic. A plugin only needs to implement the Mitigation interface in src/mitigation/Mitigation.hpp.

In the following, we provide a step-by-step guideline to implement a new PRAC mitigation within VeriPRAC.

1. Create a plugin directory

For a mitigation called MyMitigation, create:

src/mitigation/plugin/MyMitigation/MyMitigation.hpp
src/mitigation/plugin/MyMitigation/MyMitigation.cpp

Use src/mitigation/plugin/MOAT/ or src/mitigation/plugin/QPRAC/ as a starting point.

2. Implement the interface

Your class must derive from Mitigation:

#include "../../Mitigation.hpp"

class MyMitigation : public Mitigation {
public:
    MyMitigation(std::uint32_t threshold, bool debug);

    void reset() override;
    MitigationRequest informACT(int row) override;
    MitigationRequest informREF(int refreshedRow) override;
    MitigationRequest informRFM(int refreshedRow) override;
    void respondRequest(bool accepted, int row) override;
    void informMitigationDone(int row) override;
    bool queuingMechanism(int row) override;
    int getQueuingMechanismCandidate() override;
    void countingMechanism(bool isACT, int row) override;
    void resettingMechanism(int row) override;
    void primeRows(
        const std::vector<int>& rows,
        std::uint32_t activationCount) override;
};

The important callbacks are:

• reset(): clear all plugin state. The DRAM model calls this at the start of each EchoTrail execution.
• informACT(row): called when the DRAM model issues an explicit ACT to row. Update the mitigation's counters/queue and return an ALERT request if the mitigation wants reactive mitigation.
• informREF(row): called when a normal REF command physically activates row. For fine-reset designs, this row is the refreshed victim row for adjacent aggressor counters; do not interpret it as the aggressor whose counter should be reset.
• informRFM(row): called when an RFM/reactive mitigation refreshes and physically activates row.
• respondRequest(accepted, row): called when the DRAM model accepts or rejects an ALERT request. Requests are accepted only when the DRAM model is in a mode that can enter the ALERT/RFM sequence, following the PRAC ALERT Back-Off (ABO) protocol.
• informMitigationDone(row): called after the DRAM model completes reactive mitigation for row.
• primeRows(rows, activationCount): sets the mitigation's internal counters for EchoTrail priming. This is how VeriPRAC models decoys that are already close to the alert threshold before the measured target window starts.

MitigationRequest is defined in src/base/MitigationRequest.hpp:

struct MitigationRequest {
    bool ALERT = false;
    std::vector<int> rowsToMitigate;
};

To request mitigation, return:

MitigationRequest request;
request.ALERT = true;
request.rowsToMitigate.push_back(candidateRow);
return request;

Return the default {} when no mitigation is requested.

3. Add the source file to CMake

Edit CMakeLists.txt and add your .cpp file to VERIPRAC_CORE_SOURCES:

set(VERIPRAC_CORE_SOURCES
    src/base/EchoTrail.cpp
    src/dram_model/DRAMModel.cpp
    src/mitigation/plugin/BasicMitigation/BasicMitigation.cpp
    src/mitigation/plugin/MOAT/MOAT.cpp
    src/mitigation/plugin/QPRAC/QPRAC.cpp
    src/mitigation/plugin/MyMitigation/MyMitigation.cpp
    src/verifier/VerificationEngine.cpp
)

4. Register the mitigation in the factory

Edit src/main.cpp:

#include "mitigation/plugin/MyMitigation/MyMitigation.hpp"

Then extend createMitigation:

if (mitigationType == "MyMitigation") {
    return std::make_shared<MyMitigation>(threshold, debug);
}

If your mitigation needs the total DRAM row count, use the existing MOAT constructor pattern:

return std::make_shared<MyMitigation>(threshold, debug, totalRows);

5. Create a run configuration

Use an existing config (e.g., configs/qprac.json), and just edit the mitigation name (i.e., "mitigationType") and the output directory (i.e., "outputDirectory").

Keep contractsFile, totalRows, and timingParameters unchanged unless you are intentionally changing the experiment.

6. Build and run

./build/veriprac configs/my-mitigation.json

Plugin correctness checklist

• Counters are updated consistently on ACT, REF, and RFM according to the mitigation design.
• reset() clears all state that should not carry across contract runs.
• primeRows() initializes both per-row counters and any queue/summary state that depends on those counters.
• The plugin handles invalid or negative row IDs defensively.
• respondRequest(false, row) does not accidentally reset state for a request that the DRAM model rejected.
• informMitigationDone(row) performs the same counter reset/invalidation that the real mitigation would perform after a completed RFM.
• The full sweep creates a fresh mitigation instance for each contract point and then calls reset() before execution; do not rely on cross-run state.

---

Troubleshooting

How do I check whether an intended contract was violated?

When intendedContract is configured, VeriPRAC prints a satisfaction table and writes:

veriprac-satisfaction.csv
veriprac-intended-contract.pdf

inside the configured output directory. The status column reports satisfied, violated, or a missing-contract/missing-bound condition.

---

Citation

Please cite the VeriPRAC paper if you use this artifact:

@inproceedings{hajiabadi_veriprac_2026,
  title     = {{VeriPRAC: Verifiable Formal Contracts for Secure Per Row Activation Counting}},
  booktitle = {{CCS}},
  author    = {Hajiabadi, Ali and Niederer, Silvan and Razavi, Kaveh},
  year      = {2026}
}