Computer security in modern systems is a challenge: we routinely run third-party applications that access personal data, our security requirements often change with time, and we are surrounded by sophisticated adversaries that are capable of long-term observations and powerful inferences. To achieve security assurance in such an environment, it is crucial to use principled approaches to security. With a principled approach we can both gain an understanding of what it means for a system to be secure and develop techniques for analyzing tradeoffs between security, expressivity, and performance.

In this talk, I will present two lines of work that follow principled approaches to information security. First, I will present a formal framework for reasoning about a rich class of security requirements. The core of the framework is a notion of attacker knowledge that precisely characterizes the information deducible by an attacker based on the attacker’s observations. We will see how to use attacker knowledge to reason about secure information erasure as an example of an interesting and relevant security requirement.

The second part of the talk will focus on so-called timing channels—inadvertent leaks in complex systems that occur when an adversary can measure the time at which a system performs an observable action. I will explain how timing channels present a serious threat in computer security, and will introduce predictive mitigation—a general technique for mitigating timing channels that works by predicting timing from past behavior and public information. Rather than eliminating timing channels entirely, predictive mitigation bounds the amount of information that an adversary can learn via timing channels with a trade-off in system performance. Under reasonable assumptions, the bounds are logarithmic in the running time of the system.