Local Memory via Layout Randomisation

Speaker(s): Dr Julian Rathke
Organiser:
Time: 26/10/2011 13:00-14:00
Location: B53/4025

Abstract

Randomisation is used in computer security as a tool to introduce unpredictability into the software infrastructure. In this talk, I'll discuss the use of randomization to achieve secrecy and integrity guarantees for local memory.

Following the approach set out by Abadi and Plotkin (CSF 2010) I'll consider two related idealised languages: in the first, attackers simply cannot access local addresses of the user program. In the second, attackers may attempt to guess allocated memory locations and thus, with small probability, gain access to the local memory of the user program.

Our contribution to the Abadi and Plotkin program is to enrich the idealised languages with dynamic memory allocation, first class and higher order references and call/cc-style control. On the one hand, these enhancements allow us to directly model a larger class of system hardening principles. On the other hand, the class of opponents is also enhanced since our enriched language permits natural and direct encoding of attacks that alter the control flow of programs.

Our main technical result is, in the presence of randomised layouts, a proof that contextual equivalence is preserved (up to a small probability) when moving from one language to the other. Thus the attacker gains no real power from being able to guess local references of the user program.