A monadic analysis of information flow security with mutable state

Abstract: "We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic metalanguage. Thus, our logic deals with mutation explicitly, with impurity reflected in the types, in contrast to most higher-order security typed languages, which deal with mutation implicitly via side-effects. More importantly, we also take a store-oriented view of security, wherein security levels are associated with regions of the mutable store. In contrast, most other accounts are value-oriented, in that security levels are associated with individual values. Our store-oriented viewpoint allows us to address information flow security while still using a largely conventional logic, but we show that it does not lessen the expressive power of the logic. An interesting feature of our analysis lies in its treatment of upcalls (low-security computations that include high-security ones), employing an 'informativeness' judgement indicating under what circumstances a type carries useful information."