Modeling Information Flow Dependencies with Boolean Functions

By: Samir Genaim, Roberto Giacobazzi and Isabella Mastroeni

Samir Genaim
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
genaim@sci.univr.it

Roberto Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
giaco@sci.univr.it

Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
mastroeni@sci.univr.it

Abstract:

In this paper we describe two uses of Boolean functions in the context of secure information flow analysis. The first contribution concerns with modeling information flow with Boolean functions, which leads to an accurate information flow analysis that captures dependencies between possible flows. These dependencies are useful for debugging; refining the notion of secure information flow; and achieving efficient implementation using sophisticated data structures like Binary Decision Diagrams. The second contribution concerns with analyzing dynamic security policies. We describe how to construct a Boolean function, such that its models describe possible non-interference sets of program variables. This can be used to enforce security classes dynamically, rather than re-analyzing the program.