CT-ISG: New Foundations for Quantitative Information Flow

保护敏感信息的机密性和完整性是可信计算的核心。这个项目集中在问题的一个方面，即，开发软件，满足关键信息流属性的困难。安全信息流分析的方法是在执行程序之前对程序进行静态分析，通常以类型系统的形式，目的是证明它不会从高输入到低输出泄漏任何信息;这被形式化为称为不干扰的属性。但人们普遍认为，不干涉在实践中限制太多--我们经常需要低产出，而这依赖于高投入。在实现中，可以通过显式解密构造来允许这种故意的信息泄漏，该构造的功能类似于类型转换以规避类型规则。但解密虽然是权宜之计，却让人质疑分析所能确保的是什么。一种有希望的放松不干涉的方法是发展一种信息流的定量理论，让我们谈论“有多少”信息被泄露。这种定量理论正在各种背景下进行研究，包括安全信息流，匿名协议和侧信道分析，并且正在形成共识，将这些理论建立在香农熵和互信息的概念基础上。但是，一个有用的定量信息流理论必须提供适当的安全保证：如果该理论说，一次攻击泄露了x比特的秘密信息，那么x在计算最终威胁的范围时应该是有用的。不幸的是，标准理论实际上不能提供这样的保证，因为一个随机变量可以有任意大的香农熵，即使它是非常容易被猜测。因此，本项目将探索一个替代基础的定量信息流的基础上的概念的脆弱性（密切相关的贝叶斯风险）和衡量不确定性使用Renyi？s最小熵，而不是香农熵。目标是在理论和实践上发展新的基础。主要的技术挑战将是开发基于类型的静态分析，可以用来保证程序满足所需的定量信息流政策。更广泛地说，该项目旨在帮助实现具有保证信息流属性的软件的纪律开发，并教育学生关于安全信息流的编程。

Protecting the confidentiality and integrity of sensitive information is central to trustworthy computing. This project focuses on one aspect of the problem, namely, the difficulty of developing software that satisfies critical information flow properties. The approach of secure information flow analysis is to do a static analysis, usually in the form of a type system, on a program prior to executing it, with the goal of proving that it does not leak any information from its high inputs to its low outputs; this is formalized as a property called noninterference. But noninterference is widely recognized to be too restrictive in practice -- often we need to have low output that depends on high input. In implementations, such deliberate leaks of information can be allowed through an explicit declassify construct, which functions like a type cast to circumvent the typing rules. But declassification, while expedient, throws into question what is then ensured by the analysis.One promising disciplined approach to relaxing noninterference is to develop a quantitative theory of information flow that lets us talk about "how much" information is leaked. Such quantitative theories are being studied in a variety of contexts, including secure information flow, anonymity protocols, and side-channel analysis, and there is an emerging consensus to base such theories on the concepts of Shannon entropy and mutual information. But a useful theory of quantitative information flow must provide appropriate security guarantees: if the theory says that an attack leaks x bits of secret information, then x should be useful in calculating bounds on the resulting threat. Unfortunately, it can be argued that the standard theories actually fail to provide such guarantees, because a random variable can have arbitrarily large Shannon entropy even if it is highly vulnerable to being guessed.This project will therefore explore an alternative foundation for quantitative information flow based on a concept of vulnerability (closely related to Bayes risk) and which measures uncertainty using Renyi?s min-entropy, rather than Shannon entropy. The goal is to develop the new foundation both theoretically and practically. The main technical challenge will be to develop type-based static analyses that can be used to guarantee that programs satisfy desired quantitative information flow policies. More broadly, this project aims to help to enable the disciplined development of software with guaranteed information flow properties, and to educate students about programming for secure information flow.