Qualitative and quantitative information flow analysis for multi-threaded programs
Tri Minh Ngo · 2014
In today’s information-based society, guaranteeing information security plays an important role in all aspects of life: governments, military, companies, financial information systems, web-based services etc. With the existence of Internet, Google, and shared-information networks, it is easier than ever to access information. However, it is also harder than ever to protect the security of sensitive information. If an attacker can access important information, he can bring down a company or even harm people’s lives. Thus, there are growing challenges of how best to keep private information processed by computing systems secure. With the trend of multiple cores on a chip and parallel systems like general- purpose graphic processing units, applications implemented in a multi-threaded fashion are becoming the standard. Protecting the confidentiality of information manipulated by multi-threaded programs is an important problem, but also a challenge. Firstly, since the program execution involves the scheduler — to decide the ordering of executed threads — data behave in an unpredictable way; and thus, it is difficult to predict what an attacker can observe during the execution. Secondly, with the help of more powerful computing techniques, the attackers are more and more powerful, i.e., they can observe the traces of public data during the execution, and are even able to choose the scheduler to limit the set of possible program traces. Many researchers are concerned with this challenge, but most of the approaches are not sufficient, or very restrictive. 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) one for non-deterministic programs, where we do not take into account the probabilistic behavior of programs and schedulers, and (2) another one for probabilistic programs, where we assume to have knowledge about the probability of scheduling events. These two properties are scheduler-specific, i.e., if data traces of the program execution satisfy these properties, the program is guaranteed not to leak information under the scheduler used to deploy the program. We compare these formalizations with the existing proposals in the literature, and show that our definitions better approximate the intuitive understanding of confidentiality, which unfortunately cannot be formalized directly. Secondly, we propose verification methods to verify our information flow properties, i.e., logic-based and efficient algorithmic verification methods. These methods not only give precise and efficient verifications for confidentiality prop- erties, but also are relevant outside the security context. Our approaches have two advantages: (1) many other formalizations of confidentiality in the literature can also be verified by minor modifications of our algorithms, and (2) we can synthesize attacks for insecure programs, based on counter-example generation techniques. Since the verification is precise, if it fails, a counter-example can be produced, describing a possible attack on the security of the program. This idea of synthesizing attacks for information flow properties of multi-threaded programs has not been previously published in the literature. We also develop a tool which contains these techniques, and show its practical application on some case studies. Counter-examples give us the reasons why a program fails a confidentiality requirement. However, in same cases, it is also interesting to know the quantity of the information flow that has been revealed. A quantitative security policy offers 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. Classical quantitative information flow analysis often considers a system as an information-theoretic channel, where private data are the only input and public data are the output. First of all, this thesis extends this classical context by considering systems where the attacker is able to influence the initial values of public data, which should also be considered as an input of the channel. We adapt the classical view of information-theoretic channels in order to quantify information flow of programs that contain both private and public inputs. Additionally, we show that our measure can also be used to reason about the case where a system operator on purpose adds noise to the output, instead of always producing the correct output. The noisy outcomes are used to reduce the correlation between the output and the input, and thus to increase the remaining uncertainty of the attacker about the secret. However, even though the noisy outcomes enhance the security, they reduce the reliability of the program. We show how given a certain noisy output policy, the increase in security and the decrease in reliability can be quantified. Finally, this thesis presents a novel model of analysis for multi-threaded programs where the attacker is able to select the scheduling policy. This model does not follow the traditional information-theoretic channel setting. In this analysis, we first study what extra information an attacker can get if he knows the scheduler’s choices, and then integrate this information into the transition system modeling the program execution. Via a case study, we compare this approach with the traditional information-theoretic models, and show that this approach gives more intuitive-matching results.