发表机构
University of Sussex; Montanarius Ltd（萨塞克斯大学; 蒙塔纳里乌斯有限公司）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究行锤攻击这一硬件漏洞，提出概率性小步操作语义及通用故障模型，形式化一种防御方法并证明定理，开发安全信息流理论，且开发过程在Lean中用mathlib完全机械化。
AI 中文摘要
行锤攻击是动态随机存取存储器（DRAM）中的一种硬件漏洞，对攻击者行的重复访问可导致受害者行中的位翻转。这一现象违反了传统编程语言语义的核心假设。目前尚无将行锤故障与程序行为联系起来的形式框架。本文为受行锤式故障影响的理想化命令式语言提出了一种概率性小步操作语义。该语义从DRAM内部和半导体物理中抽象出来，通过一个通用的概率故障模型进行参数化。通过概率计算的标准单子结构在程序中传播结果分布。作为案例研究，形式化了一种将程序变量在物理内存中放置得足够远以防止干扰的防御方法，并证明了一个与分布无关的语义崩溃定理。还开发了一种基于观察参数的安全信息流理论。在Lean中使用mathlib对整个开发过程进行了完全机械化。
英文摘要
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.
CommentsSubmitted
