Optimality and condensing of information flow through linear refinement

AbstractDetecting 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 C expressing constancy of program variables. We then apply Giacobazzi and Scozzari’s linear refinement to build a domain C→C which contains all input/output dependences between the constancy of program variables. We show that C→C 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 C→C has the same precision as a non-compositional, input-driven analysis. Moreover, we show that C→C 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 C→C coincides with Genaim, Giacobazzi and Mastroeni’s IF domain for information flows and with Amtoft and Banerjee’s Independ domain for independence. This lets us extend to IF and Independ the properties that we proved for C→C: optimality, condensing and representation in terms of Boolean formulas. As a secondary result, it lets us conclude that IF and Independ are actually the same abstract domain, although completely different static analyses have been based on them