A different perspective on libraries for information-flow control


There is a long line of research on how to control information flow in pure programming languages. In Haskell, for instance, the MAC library [Russo 2015] provides IFC primitives that allows programmers to write (statically) secure programs. MAC enforces security by controlling the interaction of an indexed monad for print effects, MAC, and a type for labeling data, Labeled. In this talk, I will present a different point in the design space of IFC libraries which in some sense refines MAC. The starting point will be a pure language where the monad for print effects—think of IO in Haskell restricted to print—keeps track of the output channels within the type. Looking at MAC in this setting, we see that one can safely embed effectful computations into the MAC monad. It appears that in this extended setting the MAC monad is redundant in the sense that we can express its interface in terms of indexed IO and Labeled. Arguably, this refinement yields a library which is: conceptually cleaner; more compositional; and it allows more programs to typecheck. This talk is based on a paper that Alejandro Russo and I are currently preparing for submission.

Jun 4, 2021 1:15 PM