A monadic analysis of information flow security with mutable state

摘要: We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic information flow derived from lax and monadic metalanguage. Thus, our deals mutation explicitly, impurity reflected in types, contrast to most higher-order languages, which deal implicitly via side-effects. More importantly, we also take store-oriented view security, wherein security levels are associated elements store. This matches closely operational semantics low-level imperative where expressed by operations An interesting feature lies its treatment upcalls (low-security computations that include high-security ones), employing an “informativeness” judgment indicating under what circumstances type carries useful information.