Termination-Insensitive Noninterference Leaks More Than Just a Bit (2009)
Aslan Askarov, Sebastian Hunt, Andrei Sabelfeld, David S
Abstract. Current tools for analysing information flow in programs build upon ideas going back to Denning’s work from the 70’s. These systems enforce an imperfect notion of information flow which...
David Clark, Sebastian Hunt, Pasquale Malacaria
static analysis for quantifying information flow
Just Forget It The Semantics and Enforcement of Information Erasure (2008)
Abstract. There are many settings in which sensitive information is made available to a system or organisation for a specific purpose, on the understanding that it will be erased once that purpose...
On Flow-Sensitive Security Types (2006)
This article investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice...
The PER model of abstract non-interference (2005)
Sebastian Hunt, Isabella Mastroeni
Abstract. In this paper, we study the relationship between two models of secure information flow: the PER model (which uses equivalence relations) and the abstract non-interference model (which uses...
Quantitative Information Flow, Relations and Polymorphic Types (2005)
Clark, David, Hunt, Sebastian, Malacaria, Pasquale
This paper uses Shannon's information theory to give a quantitative definition of information flow in systems that transform inputs to outputs. For deterministic systems, the definition is shown to...
Quantified interference: information theory and information flow (2004)
David Clark, Sebastian Hunt, Pasquale Malacaria
Abstract. The paper investigates which of Shannon’s measures (entropy, conditional entropy, mutual information) is the right one for the task of quantifying information flow in a programming...
Non-interference for weak observers (2004)
David Clark, Sebastian Hunt, Pasquale Malacaria
We consider transformational programs, i.e. those which transform inputs into outputs, with two levels of confidentiality: high and low. Inspired by Giacobazzi and Mastroeni [GM04], we consider...
ABSTRACT Quantified Interference for a While Language (2003)
David Clarke, Sebastian Hunt, Pasquale Malicaria, David Clark
Safety of Strictness Analysis via Term Graph Rewriting (2000)
David Clark, Chris Hankin, Sebastian Hunt
. A safe abstraction is presented for a restricted form of term graph rewriting. This abstraction can be seen as a formalisation of the rewrite system employed by the strictness analyser in the...
Possibilistic Information Flow is safe for Probabilistic Non-Interference (2000)
David Clark, Chris Hankin, Sebastian Hunt, Rajagopal Nagarajan
) David Clark 1 , Chris Hankin 1 , Sebastian Hunt 2 , and Rajagopal Nagarajan 1 1 Introduction Recently there has been considerable interest in analysing programs for the existence of probabilistic...
Binding Time Analysis: A New PERspective (1991)
Given a description of the parameters in a program that will be known at partial evaluation time, a binding time analysis must determine which parts of the program are dependent solely on these known...
Abstract Interpretation of Functional Languages: From Theory to Practice (1991)
Abstract interpretation is the name applied to a number of techniques for reasoning about programs by evaluating them over non-standard domains whose elements denote properties over the standard...
PERs Generalise Projections for Strictness Analysis (1990)
) Sebastian Hunt Department Of Computing Imperial College London SW7 2BZ Abstract We show how Wadler and Hughes's use of Scott projections to describe properties of functions ("Projections...