Secure Information Flow as a Safety Problem

The termination insensitive secure information flow problem can be reduced to solving a safety problem via a simple program transformation. Barthe, D’Argenio, and Rezk coined the term “self-composition” to describe this reduction. This paper generalizes the self-compositional approach with a form of information downgrading recently proposed by Li and Zdancewic. We also identify a problem with applying the self-compositional approach in practice, and we present a solution to this problem that makes use of more traditional type-based approaches. The result is a framework that combines the best of both worlds, i.e., better than traditional type-based approaches and better than the selfcompositional approach.

• Type: Conference
• Year: 2005
• Where: SAS
• Authors: Tachio Terauchi, Alexander Aiken
• Keywords: Formal Methods, Information flow Problem, SAS 2005, Self-compositional Approach, Traditional Type-based Approaches