Optimality and condensing of information flow through linear refinement

Detecting information flows inside a program is useful to check non-interference or independence of program variables, an important aspect of software security. In this paper we present a new abstract domain expressing constancy of program variables. We then apply Giacobazzi and Scozzari’s linear refinement to build a domain which contains all input/output dependences between the constancy of program variables. We show that is optimal, in the sense that it cannot be further linearly refined, and condensing, in the sense that a compositional, input-independent static analysis over has the same precision as a non-compositional, input-driven analysis. Moreover, we show that has a natural representation in terms of Boolean formulas, which is important since it allows one to use the efficient binary decision diagrams in its implementation. We then prove that coincides with Genaim, Giacobazzi and Mastroeni’s domain for information flows and with Amtoft and Banerjee’s domain for independence. This lets us extend to and the properties that we proved for : optimality, condensing and representation in terms of Boolean formulas. As a secondary result, it lets us conclude that and are actually the same abstract domain, although completely different static analyses have been based on them.