Model Checking Secure Information Flow for Concurrent Programs


The goal of a secure information flow analysis is to check whether 
sensitive information is leaked to adversaries or not. To this end, 
some information flow property should be formally specified and 
verified. Logic-based verification and model checking are promising 
methods to verify information flow properties. Various attempts for 
logical specification and verification of information flow properties 
has been made. In this talk, I will introduce model checking 
techniques proposed so far for verifying secure information flow of 
concurrent programs. I will then discuss challenges of using model 
checking techniques to verify secure information flow and propose some 
methods to solve them.

Bio
Ali A. Noroozi is a Ph.D. student of Computer Science in University of 
Tabriz, Iran. His research interests include secure information flow 
and model checking.