Qualitative and quantitative information flow analysis for multi-threaded programs

In today's information-based society, guaranteeing information security plays an important role in all aspects of life: communication between citizens and governments, military, companies, financial information systems, web-based services etc. With the increasing popularity of computer systems with multiple CPUs, and CPUs with multiple cores, applications implemented in a multi-threaded fashion - containing multiple activities that can be executed concurrently - are becoming the standard. However, there are many challenges related to how to keep private information processed by multi-threaded systems secure in the best way. Firstly, during the execution of a multi-threaded program, data behave in an unpredictable way; and thus, it is difficult to predict what an attacker is able to observe. Secondly, with the help of more powerful computing techniques, the attackers are more and more powerful. Most existing approaches are not sufficient to guarantee confidentiality for multi-threaded programs. The goal of this thesis is to propose more suitable and practically efficient methods to analyze information flow of multi-threaded programs. Firstly, we formalize two qualitative confidentiality properties: (1) for non-deterministic programs, where we do not take into account the probabilistic behavior of programs; and (2) for probabilistic programs, where we assume to have knowledge about the probability of scheduling events. We propose verification methods to verify these information flow properties. These techniques not only give precise and efficient verification of confidentiality properties, but also are relevant outside the security context. We also develop a tool which implements these techniques, and demonstrate its practical application on some case studies. Secondly, for programs that leak secret information, it is also interesting to know the quantity of information that has been revealed. We define and investigate quantitative security policies that offer a richer security policy than the traditional qualitative properties, since the amount of leakage can be used to decide whether we can tolerate the minor leakage. We propose two novel models of quantitative information flow analysis: (1) for a program where the attacker is able to influence the initial values of public data; and (2) for a program where the attacker is able to control the ordering of executed threads.