Layout Randomization and Nondeterminism

Abstract. In security, layout randomization is a popular, effective at-tack mitigation technique. Recent work has aimed to explain it rigor-ously, 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 del-icate 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 probabilis-tic powerdomain.