Rowhammer fault model proves memory protection method secure
A Rowhammer attack on Fil-C's software capabilities
Programming LanguagesCryptography and Security
Summary
Rowhammer is a hardware quirk in computer memory where repeatedly accessing certain parts can accidentally flip bits in nearby parts, causing unexpected changes. This breaks a basic rule programmers rely on: that changing one spot in memory doesn’t affect another. The authors created a high-level mathematical model to describe programs when these bit-flips happen randomly. They then used this to prove that a common defense method—placing important data far apart in memory—really works to stop these accidental changes from affecting other data. They also developed a way to understand how information securely flows in such faulty conditions.
What this means in practice
- •For software security engineers: Formally verify that memory separation defenses prevent Rowhammer faults from affecting program correctness.
- •For hardware-software co-design teams: Use the probabilistic Rowhammer model to guide design of fault-resilient software and hardware memory layouts.
A theory result. No direct application yet.
Authors
Amir Naseredini, Suhas Viswanath, Martin Berger
Abstract
Rowhammer is a hardware vulnerability in dynamic random-access memory (DRAM) in which repeated accesses to one or more aggressor rows can induce bit-flips in nearby victim rows. This phenomenon violates a core assumption of conventional programming language semantics: that reading from or writing to one memory location does not modify others. Despite the security importance of this phenomenon, there is no widely established formal framework connecting Rowhammer faults with program behaviour. This makes it difficult to reason rigorously about the efficacy of proposed Rowhammer defences and the program-level guarantees they provide. To address this gap, we present a probabilistic small-step operational semantics for an idealised imperative language subject to Rowhammer-style faults. The semantics is high-level in that it 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 within a specified victim region. The resulting distributions are propagated through programs using the standard monadic structure of probabilistic computation. As a case study, we formalise physical separation, 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. Furthermore, we develop an observation-parametric account of secure information flow.