Journal of Functional Programming




Special Issue on Language Based Security

A monadic analysis of information flow security with mutable state


KARL CRARY a1, ALEKSEY KLIGER a1 and FRANK PFENNING a1
a1 Carnegie Mellon University, 5000 Forbes Avenue Pittsburgh, PA 15213 USA (email: crary@cs.cmu.edu, aleksey@cs.cmu.edu, fp@cs.cmu.edu)

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

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 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)