
doi: 10.1007/11560647_23
handle: 11562/27187
Detecting information flows inside a program is useful to check non-interference of program variables, an important aspect of software security. Information flows have been computed in the past by using abstract interpretation over an abstract domain IF which expresses sets of flows. In this paper we reconstruct IF as the linear refinementC → C of a basic domain C expressing constancy of program variables. This is important since we also show that C → C, and hence IF, is closed w.r.t. linear refinement, and is hence optimal and condensing. Then a compositional, input-independent static analysis over IF has the same precision of a non-compositional, input-driven analysis. Moreover, we show that C → C has a natural representation in terms of Boolean formulas, efficiently implementable through binary decision diagrams.
Static Analysis; Information Flow; Abstract Interpretation; Linear Refinement
Static Analysis; Information Flow; Abstract Interpretation; Linear Refinement
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
