Securing Interactive Programs

Abstract—This paper studies the foundations of informationflow 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. We 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 we distinguish between the security level of message presence and message content. We show that the generalized framework features appealing compositionality properties: parallel composition of secure program results in a secure thread pool. We also show that modeling environments as strategies leads to strong compositionality: various types of composition (with and...

• Type: Journal
• Year: 2012
• Where: CSFW
• Authors: Willard Rafnsson, Daniel Hedin, Andrei Sabelfeld
• Keywords: CSFW 2012, Framework Features, Parallel Composition, Secret Leaks, Security Privacy