Computer Science Department
School of Computer Science, Carnegie Mellon University
A Monadic Analysis of Information Flow Security
with Mutable State
Kary Crary, Aleksey Kliger, Frank Pfenning
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" judgment indicating under what circumstances a type carries useful information.