Model Checking and Program Analysis for Quantifying Interference

为了量化干扰（或安全泄漏），信息论和程序分析中的概念被用来告诉一个程序可以向攻击者泄露多少机密数据。这解决了一个基本的概念问题，它是安全基础的核心：问题是“安全”程序确实会泄漏少量信息。一个例子是密码保护的访问控制，它本质上会泄漏数据，毕竟它必须告诉你你是否输入了正确的密码。大多数基于语言的安全性研究都是基于定性概念，主要关注的是不干扰。粗略地说，软件系统中的两个组件会相互干扰，因为对一个组件的更改会影响另一个组件的行为。P.Ryan、J.姆克林、J.Millen和V. Gilgor已经优雅地指出了这些方法的问题：在大多数非干扰模型中，即使一个比特是所有丢失的，一个比特的泄露信息也会被标记为安全违规。要认真对待，违反不干涉原则应意味着更重大的损失。甚至...在那里，时间是不可用的，每毫秒一位与每两周一位是无法区分的。折衷了无限信息量的信道与不能折衷的信道有很大的不同。由于前面的评论，我们认为定性方法有基础问题和有限的适用性。我们的总体目标是测量干扰，然后使用此数量来评估程序的安全风险。为了说明，考虑以下包含安全变量h和公共变量l的程序：l=20; while（h < l）{l=l-1}该程序对秘密h的值执行有界搜索。这个程序是安全威胁吗？有人可能会说，这个决定应该取决于秘密的大小;秘密越大，它就越安全。如何给这个论点一个确切的含义？如果h是一个10位变量，那么前面的程序是安全的吗？答案不应该也取决于攻击者对输入分布的了解吗？例如，如果她/他知道0是h比任何其他值更有可能的值？第一个重要贡献是发展了一种理论，这种问题可以数学解决。在这个方向上的一个重要步骤是PI开发了第一个（据我们所知）精确的，循环结构的信息理论语义（POPL 2007）。语义是定量的：结果是衡量程序安全属性的真实的数字。这项工作第一次为测量"真实的世界程序的干扰打开了大门，最近PI和Han Chen将其扩展到量化多线程程序的泄漏（PLAS 2007）。然而，分析的精确性需要一些独创性。该提案的目的是在大多数情况下消除对独创性的需要，通过开发工具来实现分析的自动化，如目标部分所述。

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.