Henning Sudbrock - Information Flow Analysis with the Combining Calculus using Program Transformations

 

Ort: Raum S2-02 /  E302
Datum und Zeit: Dienstag, 10. Februar 2009, 16:30-17:30 Uhr

Henning Sudbrock

This talk presents work in progress.

When giving a program access to secret information, one must ensure that the
program does not leak the secrets to untrusted sinks. The Combining Calculus
[MSK07] provides a set of rules that allow the flexible migration between
different static analysis techniques during such an information flow
analysis, thereby permitting to successfully establish the information flow
security of a larger set of programs than by using the analysis techniques
in separation.

The rules of the Combining Calculus allow one to deduce a program's
information flow security in a compositional fashion, based on the program's
syntactical structure. We illustrate how the syntactical structure of a
program affects the possibility to successfully verify that the program has
secure information flow with the Combining Calculus. As a solution to this
problem we present a semantics-preserving program transformation making
implementations more amenable to a successful verification. We furthermore
briefly present an approach to make programs accessible to a successful
verification with the Combining Calculus by using a program transformation
that changes the semantics of programs only in acceptable ways.

[MSK07] H.Mantel, H.Sudbrock, T.Kraußer. Combining different proof techniques for verifying information flow security. In Proceedings of LOPSTR 2006, vol. 4407 of LNCS, Springer, 2007.