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 refinement C->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 wrt 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.
Information Flow is Linear Refinement of Constancy
SPOTO, Nicola Fausto
2005-01-01
Abstract
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 refinement C->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 wrt 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.File | Dimensione | Formato | |
---|---|---|---|
InformationFlowIsLinearRefinement.pdf
solo utenti autorizzati
Tipologia:
Versione dell'editore
Licenza:
Accesso ristretto
Dimensione
612.67 kB
Formato
Adobe PDF
|
612.67 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.