Layout Randomization and Nondeterminism

In security, layout randomization is a popular, effective attack mitigation technique. Recent work has aimed to explain it rigorously, focusing on deterministic systems. In this paper, we study layout randomization in the presence of nondeterministic choice. We develop a semantic approach based on denotational models and the induced notions of contextual public observation, characterized by simulation relations. This approach abstracts from language details, and helps manage the delicate interaction between nondeterminism and probability. In particular, memory access probabilities are not independent, but rather depend on a fixed probability distribution over memory layouts; we therefore model probability using random variables rather than any notion of probabilistic powerdomain.