Mechanised Operational Semantics of Rowhammer

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...