Information flow security on persistent memory
It provides the first information flow security analysis for persistent memory architectures, addressing a gap in security verification for this emerging memory paradigm.
The paper introduces an information flow logic for an unstructured language with gotos, modeling a simple assembly language, and applies it to x86 assembly using reordering interference freedom (rif) to reason about out-of-order propagation to memory, then extends this to persistent memory.
Persistent memory is a recently proposed memory paradigm that delivers many system-wide benefits, including improved runtime efficiency and the ability of programs to recover from power outages and system crashes. While recent research has investigated techniques for proving functional correctness of programs running on related architectures, this is not the case for the orthogonal concept of information flow security. In this paper, we provide an information flow logic for an unstructured language (i.e., with gotos rather than loops) modelling a simple assembly language. We apply this logic to x86 assembly using a notion of reordering interference freedom (rif) to reason about potential out-of-order propagation of instructions to memory. We then show how this same notion of rif can be used to similarly reason about information flow on persistent memory.