Abstract interpretation and model checking for checking secure information flow in concurrent systems

We propose a method to check secure information flow in concurrent programs with synchronization. The method is based on the combination of abstract interpretation and 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.