← All papers
First page of Mechanised operational semantics of Rowhammer

Mechanised operational semantics of Rowhammer

Martin Berger, Amir Naseredini

cs.PL Jul 11, 2026 · v2
Mechanises in Lean with mathlib's PMF a probabilistic Rowhammer operational semantics, a physical-separation soundness theorem, and relative non-interference results.
Rowhammer is a hardware vulnerability in dynamic random-access memory (DRAM) in which repeated accesses to aggressor rows can induce bit-flips in victim rows. This phenomenon violates a core assumption of conventional programming language semantics: reading or writing one memory location does not modify others. Despite the security importance of this phenomenon, there is no formal framework connecting Rowhammer faults with program behaviour. We present a probabilistic small-step operational semantics for an idealised imperative language subject to Rowhammer-style faults. The semantics abstracts from DRAM internals and semiconductor physics. A general probabilistic fault model parameterises the semantics, representing Rowhammer-style faults by assigning probabilities to bit-flips during read or write operations. The resulting distributions are propagated through programs using the standard monadic structure of probabilistic computation. As a case study, we formalise a well-known defence that places program variables sufficiently far apart in physical memory that an access to one variable cannot disturb another. We prove a distribution-independent semantic collapse theorem: for every finite execution, including prefixes of terminating and non-terminating executions, the protected projection of the probabilistic Rowhammer semantics is the Dirac distribution of the corresponding Rowhammer-free execution. We develop an observation-parametric account of secure information flow. Non-interference is expressed as a hyperproperty comparing the distributions of low observations from low-equivalent initial memories. Consequently, physical separation preserves non-interference for every admissible fault model, while every Rowhammer non-interference violation reflects a violation already present in the Rowhammer-free semantics. The development is fully mechanised in Lean using mathlib.

Rowhammer bit-flips break the locality assumption of program semantics: accessing one memory location may modify others. No formal framework linked Rowhammer faults to program behaviour or to security properties such as non-interference.

The authors define a probabilistic small-step operational semantics for a WHILE language. Read and write transitions sample from a general fault model in which each variable has a 'blast radius' of locations that may flip. Distributions are propagated through programs with the probability monad, represented in Lean as mathlib PMFs. Physical separation of variables is formalised as a defence, and observation-parametric non-interference is defined as a hyperproperty over distributions of low observations.

Figure 4. The idea behind the fault model is that each variable x has a ’blast radius’, a set of other memory locations that may get flipped when x is accessed. Locations outside the blast radius will not be flipped. The fault model formalises the shape of each blast radius, and the flip probabilities. Unlike Figures 2 and 3 , this image does not show row shapes, because our formal model does not