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.

为了量化信息理论和程序分析中的干扰（或安全泄漏）概念，用于判断程序可以向攻击者揭示多少机密数据。这解决了一个基础安全基础核心的基本概念问题：问题是``Secure''程序确实泄漏了少量信息。一个示例是密码受保护的访问控制，该控件泄漏了数据，毕竟它必须告诉您您是否输入了正确的密码。基于语言的安全性的大多数研究都是基于定性概念，主要重点是非干预。粗略地说，当一个变化为一个的软件系统中的两个组件会影响另一个组件。这些方法的问题优雅地由P.Ryan，J。McLean，J.Millen和V. Gilgor说：在大多数非干预模型中，即使一点点丢失了，也将一点点折衷的信息标记为违反安全性。要认真对待，违反不干预的行为应意味着更重大的损失。即使...在没有时间的情况下，每两周都无法区分每毫秒...损害无界信息的频道与不能限制的信息大不相同。由于先前的评论，我们认为定性方法存在基本问题和有限的适用性。我们的总体目的是衡量干扰，然后使用此数量来评估程序的安全风险。为了说明，请考虑包含安全变量H和公共变量L：L = 20的以下程序；而（h <l）{l = l-1}程序对秘密h的值进行有限的搜索。这个程序是安全威胁吗？有人可能会争辩说，决定应取决于秘密的规模。秘密越大，它变得越安全。如何为这个论点赋予精确的含义？如果H是10位变量，先前的程序是否安全？如果她/他知道0比其他任何值更可能是H的价值？第一个重要的贡献是发展这种问题可以在数学上解决的理论的发展。朝这个方向迈出的主要一步是PI的发展（据我们所知）（据我们所知）精确，信息理论的语义（Popl 2007）。语义是定量的：结果是测量程序安全属性的实数。这项工作首次打开了``现实世界计划的干扰''，而最近，Pi和Han Chen已将其扩展，以量化多线程程序的泄漏（Plas 2007）。分析是精确需要的事实。该提案的目的是在大多数情况下消除需要通过“目标”部分所述的分析自动化工具来消除创造力的需求。