Model Checking and Program Analysis for Quantifying Interference

用于量化干扰的模型检查和程序分析

基本信息

批准号：
EP/F023766/1
负责人：
Pasquale Malacaria
金额：
$ 14.02万
依托单位：
Queen Mary University of London
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2008
资助国家：
英国
起止时间：
2008 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FF023766%2F1
关键词：
Model Checking Program Analysis Quantifying

项目摘要

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.

为了量化干扰（或安全泄漏），信息论和程序分析中的概念被用来判断程序可以向攻击者泄露多少机密数据。这解决了安全基础核心的一个基本概念问题：问题是“安全”程序确实会泄漏少量信息。一个例子是受密码保护的访问控制，它本质上会泄漏数据，毕竟它必须告诉您是否输入了正确的密码。大多数基于语言的安全性研究都基于定性概念，主要关注点不干涉。粗略地说，当软件系统中的两个组件中一个组件的更改影响另一个组件的行为时，就会发生干扰。 P.Ryan、J. McLean、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）。事实是分析是精确的，但需要一些独创性。该提案的目的是通过开发目标部分所述的自动化分析工具来消除大多数情况下对独创性的需求。