Securing Interactive Programs
This paper studies the foundations of information flow security for interactive programs. Previous research assumes that the environment is total, that is, it must always be ready to feed new inputs into programs. However, programs secure under this assumption can leak the presence of input. Such leaks can be magnified to whole-secret leaks in the concurrent setting. The authors propose a framework that generalizes previous research along two dimensions: first, the framework breaks away from the totality of the environment and, second, the framework features fine-grained security types for communication channels, where they distinguish between the security level of message presence and message content. They show that the generalized framework features appealing compositionality properties: parallel composition of secure program results in a secure thread pool.