Model Checking and Program Analysis for Quantifying Interference

点击翻译按钮获取中文摘要

To quantify interference (or security leakage) concepts from Information Theory and Program Analysis are used to tell how much confidential data a program can reveal to an attacker. This addresses a basic conceptual issue that lies at the heart of the foundations of security: The problem is that ``secure'' programs do leak small amounts of information. An example is password protected access control which leaks data by its nature, after all it has to tell you whether you entered the correct password or not.Most research on language-based security has been based on qualitative concepts, with the main focus being on non-interference. Roughly speaking, two components in a software system interfere when changes to one affects the behaviour of the other. The problem with these approaches has elegantly been stated by P.Ryan, J. McLean, J.Millen and V. Gilgor: In most non-interference models, a single bit of compromised information is flagged as a security violation, even if one bit is all that is lost. To be taken seriously, a non-interference violation should imply a more significant loss. Even ... where timings are not available, and a bit per millisecond is not distinguishable from a bit per fortnight ... a channel that compromises an unbounded amount of information is substantially different from one that cannot. Because of the previous remark we believe that qualitative approaches have foundational problems and limited applicability. Our overall aim is instead to measure interference and then use this quantity to assess the security risk of a program. To illustrate, consider the following program containing a secure variable h and a public variable l: l=20; while ( h < l) {l=l-1}The program performs a bounded search for the value of the secret h. Is this program a security threat? One could argue that the decision should depend on the size of the secret; the larger the secret the more secure it becomes. How to give a precise meaning to this argument? Is the previous program secure if h is a 10-bit variable?And shouldn't the answer depend also on the attacker's knowledge of the distribution of inputs e.g. if she/he knew that 0 is a much more likely value for h than any other value? A first important contribution is the development of a theory where this kind of questions can be mathematically addressed. A major step in this direction has been the development by the PI of the first (to the best of our knowledge) precise, information theoretical semantics of looping constructs (POPL 2007). The semantics is quantitative: outcomes are real numbers measuring security properties of programs. This work opens the door, for the first time, to measuring interference of ``real world programs, and more recently it has been extended by the PI and Han Chen to quantify leakage of multi-threaded programs (PLAS 2007).The fact that the analysis is precise requires however some ingenuity. The aim of this proposal is to eliminate in most cases the need for the ingenuity by developing tools for an automation of the analysis as described in the objectives section.