Information Flow for ARM


Most information-flow security for concurrent programs has implicitly
assumed a sequentially consistent memory model by assuming an
interleaving semantics for proofs and definitions.  Modern multi-core
architectures do not fulfill the assumption as they implement memory
models that enable executions that are not possible under a sequentially
consistent memory model.  In particular ARM has a memory model that
allows a lot more executions than sequential consistency.

In this talk I will discuss how I plan to model ARM's re-orderings in an
execution model that we have developed previously and give a brief
glance at what the consequences of ARM's memory model are for
information-flow security.