\title{Abstract Interpretation and Model Checking for Checking Secure
Information Flow in Concurrent Systems }

\author{Nicoletta De Francesco \and Antonella Santone \and Luca Tesei}

\begin{abstract} 
We propose a method to check secure information flow in concurrent
programs with synchronization. The method is based on the combination
of {\em abstract interpretation} and {\em model checking}: by abstract
interpretation we build a finite representation (transition system) of
the behavior of the program.  Then we model check the the abstract
transition system with respect to the security properties, expressed
by a set of temporal logic formulae.  The approach allows certifying
more programs than previous methods do.  The main point is that we are
able to check more carefully the scope of indirect information flows.
\end{abstract}