Journal of Functional Programming

Special Issue on Language Based Security

A monadic analysis of information flow security with mutable state

a1 Carnegie Mellon University, 5000 Forbes Avenue Pittsburgh, PA 15213 USA (email:,,

Article author query
crary k   [Google Scholar] 
kliger a   [Google Scholar] 
pfenning f   [Google Scholar] 


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 elements of the mutable store. This view matches closely with the operational semantics of low-level imperative languages where information flow is expressed by operations on the store. An interesting feature of our analysis lies in its treatment of upcalls (low-security computations that include high-security ones), employing an “informativeness” judgment indicating under what circumstances a type carries useful information.

(Published Online March 3 2005)