Research on certifying information flow security for sequential programs has made much progress over the last fifteen years, resulting in elegant security properties, sound verification techniques and efficient analysis tools. It would be very desirable to adopt these techniques for the analysis of concurrent programs. Analysing the security of individual threads is, however, not sufficient for ensuring the security of concurrent programs. For sound compositional reasoning, the environment of a thread must be taken into account. So far, overly conservative approximations of environments have led to rather restrictive analyses, and this imprecision constitutes a major obstacle for the migration of information flow analysis into practice.

The overall goal of our project is to lift information flow analyses for concurrent programs to a similar level of precision as analyses for sequential programs. In the talk, I will present solutions for approximating the environment of individual threads more precisely, and I will demonstrate that this substantially increases the precision of information flow analyses for concurrent programs.