I’m happy to report that Cătălin Hriţcu, Ben Karel, Benjamin Pierce, Greg Morrisett, and I submitted a paper to POPL 2013: the paper is called Exceptionally Available Dynamic IFC. Here’s the abstract:

Existing designs for fine-grained, dynamic information-flow control assume that it is acceptable to terminate the entire system when an incorrect flow is detected—i.e, they give up availability for the sake of confidentiality and integrity. This is an unrealistic limitation for systems such as long-running servers.

We identify public labels and delayed exceptions as crucial ingredients for making information-flow errors recoverable while retaining the fundamental soundness property of non-interference, and we propose two new error-handling mechanisms that make all errors recoverable. The first mechanism builds directly on these basic ingredients, using not-a-values (NaVs) and data flow to propagate errors. The second mechanism adapts the standard exception model to satisfy the extra constraints arising from information flow control, converting thrown exceptions to delayed ones at certain points. We prove both mechanisms sound. Finally, we describe a prototype implementation of a full-scale language with NaVs and report on our experience building high-availability software components in this setting.