bibliography.bib

@inproceedings{HST11,
  author = {Filippo Del Tedesco and
               Sebastian Hunt and
               David Sands},
  title = {A Semantic Hierarchy for Erasure Policies},
  booktitle = {ICISS},
  year = {2011},
  pages = {352-369},
  ee = {http://dx.doi.org/10.1007/978-3-642-25560-1_24},
  crossref = {ICISS11},
  pdf = {http://staff.city.ac.uk/~sj353/papers/ICISS-2011-proofs.pdf},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  abstract = {We consider the problem of logical data erasure, contrasting with physical erasure in the same way that end-to-end information flow control contrasts with access control. We present a semantic hierarchy for erasure policies, using a possibilistic knowledge-based semantics to define policy satisfaction such that there is an intuitively clear upper bound on what information an erasure policy permits to be retained. Our hierarchy allows a rich class of erasure policies to be expressed, taking account of the power of the attacker, how much information may be retained, and under what conditions it may be retained. While our main aim is to specify erasure policies, the semantic framework allows quite general information-flow policies to be formulated for a variety of semantic notions of secrecy.}
}

@proceedings{ICISS11,
  editor = {Sushil Jajodia and
               Chandan Mazumdar},
  title = {Information Systems Security - 7th International Conference,
               ICISS 2011, Kolkata, India, December 15-19, 2011, Procedings},
  booktitle = {ICISS},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7093},
  year = {2011},
  isbn = {978-3-642-25559-5},
  ee = {http://dx.doi.org/10.1007/978-3-642-25560-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{HS11,
  author = {Sebastian Hunt and David Sands},
  title = {From Exponential to Polynomial-Time Security Typing via Principal Types},
  booktitle = {ESOP},
  year = {2011},
  pages = {297-316},
  ee = {http://dx.doi.org/10.1007/978-3-642-19718-5_16},
  crossref = {ESOP11},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  pdf = {http://staff.city.ac.uk/~sj353/papers/esop11.pdf},
  abstract = {Hunt and Sands (POPL'06) studied a flow sensitive type (FST) system
for multi-level security, parametric in the choice of lattice of
security levels. Choosing the powerset of program variables as the
security lattice yields a system which was shown to be equivalent
to Amtoft and Banerjee's Hoare-style independence logic (SAS'04).
Moreover, using the powerset lattice, it was shown how to derive
a principal type from which all other types (for all choices of
lattice) can be simply derived.
%
Both of these earlier works gave ``algorithmic'' formulations of the
type system/program logic, but both algorithms are of exponential
complexity due to the iterative typing of While loops. Later work
by Hunt and Sands (ESOP'08) adapted the FST system to provide an
erasure type system which determines whether some input is correctly
erased at a designated time. This type system is inherently
exponential, requiring a double typing of the erasure-labelled input command.
%
In this paper we start by developing the FST work in two key ways:
(1) We specialise the FST system to a form which only derives
principal types; the resulting type system has a simple algorithmic
reading, yielding principal security types in polynomial time.
(2) We show how the FST system can be simply extended to check for
various degrees of termination sensitivity (the original FST system
is completely termination insensitive, while the erasure type system
is fully termination sensitive).
%
We go on to demonstrate the power of these techniques by combining
them to develop a type system which is shown to correctly implement
erasure typing in polynomial time. Principality is used in an
essential way to reduce type derivation size from exponential to
linear.}
}

@proceedings{ESOP11,
  editor = {Gilles Barthe},
  title = {Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr{\"u}cken, Germany, March 26-April 3, 2011. Proceedings},
  booktitle = {ESOP},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6602},
  year = {2011},
  isbn = {978-3-642-19717-8},
  ee = {http://dx.doi.org/10.1007/978-3-642-19718-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{HC08,
  author = {David Clark and Sebastian Hunt},
  pdf = {http://staff.city.ac.uk/~sj353/papers/fast08-preproc.pdf},
  title = {Non-Interference for Deterministic Interactive Programs},
  year = {2008},
  booktitle = {Proc. 5th International Workshop on Formal Aspects in Security and Trust (FAST2008)},
  address = {Malaga, Spain},
  month = {October},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  abstract = {We consider the problem of defining an appropriate notion of
non-interference (NI) for deterministic interactive programs. Previous
work on the security of interactive programs by O'Neill, Clarkson
and Chong (CSFW 2006) builds on earlier ideas due to Wittbold and
Johnson (Symposium on Security and Privacy 1990), and argues for a
notion of NI defined in terms of strategies modelling the behaviour
of users. We show that, for deterministic interactive programs, it
is not necessary to consider strategies and that a simple stream
model of the users' behaviour is sufficient. The key technical
result is that, for deterministic programs, stream-based NI implies
the apparently more general strategy-based NI (in fact we consider
a wider class of strategies than those of O'Neill et al). We give
our results in terms of a simple notion of Input-Output Labelled
Transition System, thus allowing application of the results to a
large class of deterministic interactive programming languages.}
}

@inproceedings{AHSS08,
  author = {Aslan Askarov and Sebastian Hunt and Andrei Sabelfeld and David Sands},
  pdf = {http://staff.city.ac.uk/~sj353/papers/esorics08.pdf},
  title = {Termination-Insensitive Noninterference Leaks More Than Just a Bit},
  year = {2008},
  booktitle = {Proc. 13th European Symposium on Research in Computer Security (ESORICS'08)},
  address = {Malaga, Spain},
  month = {October},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {5283},
  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 has become
known as \emph{termination-insensitive noninterference}. Under this
version of noninterference, information leaks are permitted if they
are transmitted purely by the program's termination behaviour (i.e.,
whether it terminates or not).  This imperfection is the price to
pay for having a security condition which is relatively liberal
(e.g. allowing while-loops whose termination may depend on the value
of a secret) and easy to check.  But what is the price exactly? We
argue that, in the presence of output, the price is higher than the
``one bit'' often claimed informally in the literature, and
effectively such programs can leak all of their secrets.  In this
paper we develop a definition of termination-insensitive
noninterference suitable for reasoning about programs with
outputs. We show that the definition generalises ``batch-job'' style
definitions from the literature and that it is indeed satisfied by a
Denning-style program analysis with output. Although more than a bit
of information can be leaked by programs satisfying this condition,
we show that the best an attacker can do is a brute-force attack,
which means that the attacker cannot reliably (in a technical sense)
learn the secret in polynomial time in the size of the secret. If we
further assume that secrets are uniformly distributed, we show that
the advantage the attacker gains when guessing the secret after
observing a polynomial amount of output is negligible in the size of
the secret.}
}

@unpublished{HS08a,
  author = {Sebastian Hunt and David Sands},
  pdf = {http://staff.city.ac.uk/~sj353/papers/erasure-full.pdf},
  title = {Just Forget It: The Semantics and Enforcement of Information Erasure},
  note = {Extended version of \cite{HS08} including proofs},
  year = {2008},
  month = {April}
}

@inproceedings{HS08,
  author = {Sebastian Hunt and David Sands},
  title = {Just Forget It: The Semantics and Enforcement of Information Erasure},
  booktitle = {Proc. 17th European Symposium on Programming (ESOP'08)},
  address = {Budapest, Hungary},
  month = {March},
  year = {2008},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {4960},
  pdf = {http://staff.city.ac.uk/~sj353/papers/erasure-preprint.pdf},
  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 has been
fulfilled.  A familiar example is that of online credit card
transactions: a customer typically provides credit card details to a
payment system on the understanding that the following promises are
kept: (i) Noninterference (NI): the card details may flow to the bank
(in order that the payment can be authorised) but not
to other users of the system;
(ii) Erasure: the payment system will not retain any record
of the card details once the transaction is complete.
This example shows that
we need to reason
about NI and erasure in combination, and that we need to consider
interactive systems: the card details are used in the interaction
between the
principals,
and then erased;
without the interaction, the card details could be dispensed with
altogether and erasure would be unnecessary.  The contributions of
this paper are as follows.
(i) We show that an end-to-end erasure property can be encoded
as a ``flow sensitive'' noninterference property.
(ii) By a judicious choice of language construct to support erasure policies, we
successfully adapt this result to an interactive setting.
(iii) We use this result to design a type system which guarantees that well
typed programs are properly erasing.
Although erasure policies have been discussed in earlier papers,
this appears to be the first static analysis to enforce erasure.}
}

@article{CHM07,
  author = {David Clark and Sebastian Hunt and Pasquale Malacaria},
  title = {A static analysis for quantifying information flow in a simple imperative language},
  journal = {Journal of Computer Security},
  year = {2007},
  volume = 15,
  number = 3,
  pages = {321--371},
  pdf = {http://staff.city.ac.uk/~sj353/papers/jcs2007.pdf},
  abstract = {We propose an approach to quantify interference in a simple imperative
language that includes a looping construct.  In this paper we focus on a
particular case of this definition of interference: leakage of information
from private variables to public ones via a Trojan Horse attack.  We quantify
leakage in terms of Shannon's information theory and we motivate our
definition by proving a result relating this definition of leakage and the
classical notion of programming language interference.  The major contribution
of the paper is a quantitative static analysis based on this definition for
such a language. The analysis uses some non-trivial information theory results
like Fano's inequality and ${\cal L}_1$ inequalities to provide reasonable
bounds for conditional statements.  While-loops are handled by integrating a
qualitative flow-sensitive dependency analysis into the quantitative analysis.}
}

@unpublished{CH07,
  author = {David Clark and Sebastian Hunt},
  pdf = {http://staff.city.ac.uk/~sj353/papers/plid07talk.pdf},
  title = {Non-Interference For Interactive Programs},
  note = {Presented at Third International Workshop on Programming Language Interference and Dependence (PLID'07),
satellite workshop of SAS'07},
  year = {2007},
  month = {August},
  address = {Kongens Lyngby, Denmark},
  url = {http://www.dcs.kcl.ac.uk/pg/cmu/plid07}
}

@inproceedings{HS06,
  author = {Sebastian Hunt and David Sands},
  title = {On Flow-Sensitive Security Types},
  booktitle = {Proc. Principles of Programming Languages, 33rd Annual ACM SIGPLAN - SIGACT Symposium (POPL'06)},
  pages = {79--90},
  address = {Charleston, South Carolina, USA},
  month = {January},
  year = {2006},
  publisher = {ACM Press},
  pdf = {http://staff.city.ac.uk/~sj353/papers/floatingX.pdf},
  abstract = {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 of flow lattice.

By choosing the flow lattice to be the powerset of program variables,
we obtain a system which, in a very strong sense, subsumes all other
systems in the family (in particular, for each program, it allows
one particular ``polymorphic'' derivation from which all others may
be inferred).  This distinguished system is shown to be equivalent
to, though more simply described than, Amtoft and Banerjee's
Hoare-style independence logic (SAS'04).

In general, some lattices are more expressive than others but,
despite this, we show that no type system in the family can give
better results for a given choice of lattice than the type system
for that lattice itself.

Finally, for any program typeable in one of these systems, we show
how to construct an equivalent program which is typeable in a simple
flow-insensitive system.  We argue that this general approach could
be useful in a proof-carrying-code setting.}
}

@inproceedings{HM05,
  author = {Sebastian Hunt and Isabella Mastroeni},
  title = {The PER model of Abstract Non-Interference},
  booktitle = {Proc. Static Analysis, 12th International Symposium (SAS'05)},
  editor = {R. Giacobazzi},
  year = {2005},
  series = {Lecture Notes in Computer Science},
  volume = {3184},
  pdf = {http://staff.city.ac.uk/~sj353/papers/sas05.pdf},
  pages = {100--115},
  publisher = {Springer-Verlag}
}

@article{CHM05b,
  author = {David Clark and Sebastian Hunt and Pasquale Malacaria},
  title = {Quantitative Information Flow, Relations and Polymorphic Types},
  journal = {Journal of Logic and Computation, Special Issue on Lambda-calculus, type theory and natural language},
  year = {2005},
  volume = 18,
  number = 2,
  pages = {181--199},
  pdf = {http://logcom.oupjournals.org/cgi/reprint/15/2/181?ijkey=56At7mt7JtZw6&keytype=ref},
  abstract = {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 specialise to a simpler form
when the information source and the known inputs jointly determine the inputs.
For this special case,
the definition is related to the classical security condition of non-interference
and an equivalence is established between non-interference and
independence of random variables.
Quantitative information flow for deterministic systems is then presented in relational form.
With this presentation, it is shown how
relational parametricity can be used to derive upper and lower bounds on information
flows through families of functions defined in the second order lambda calculus.}
}

@article{CHM05a,
  author = {David Clark and Sebastian Hunt and Pasquale Malacaria},
  url = {http://www.sciencedirect.com/science/journal/15710661},
  pdf = {http://staff.city.ac.uk/~sj353/papers/qapl04.pdf},
  title = {Quantified Interference for a While Language},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = 112,
  year = 2005,
  month = {January},
  pages = {149--166},
  note = {Proceedings of the Second Workshop on Quantitative Aspects of Programming Languages (QAPL 2004)},
  abstract = {We show how an information theoretic approach can quantify
interference in a simple imperative language that includes a looping
construct.  In this paper we focus on a particular case of this
definition of interference: leakage of information from private
variables to public ones in While language
programs.  The major result of the paper is a quantitative analysis
for this language that employs a use-definition graph to calculate
bounds on the leakage into each variable.}
}

@unpublished{CHM04b,
  author = {David Clark and Sebastian Hunt and Pasquale Malacaria},
  pdf = {http://staff.city.ac.uk/~sj353/papers/plid04-talk.pdf},
  title = {Non-Interference For Weak Observers},
  note = {Presented at First International Workshop on Programming Language Interference and Dependence (PLID'04),
satellite workshop of SAS'04},
  year = {2004},
  month = {August},
  address = {Verona, Italy},
  url = {http://profs.sci.univr.it/~mastroen/noninterference.html}
}

@unpublished{CHM04a,
  author = {David Clark and Sebastian Hunt and Pasquale Malacaria},
  pdf = {http://staff.city.ac.uk/~sj353/papers/wits04.pdf},
  title = {Quantified Interference: Information Theory and Information Flow},
  note = {Presented at Workshop on Issues in the Theory of Security (WITS'04)},
  year = {2004},
  month = {April}
}

@techreport{CHM03b,
  author = {David Clark and Sebastian Hunt and Pasquale Malacaria},
  title = {Quantified Interference for a {While} Language},
  institution = {Department of Computer Science, King's College London},
  year = {2003},
  number = {TR-03-07},
  month = {October},
  url = {http://www.dcs.kcl.ac.uk/technical-reports/papers/TR-03-07.ps}
}

@unpublished{CHM03a,
  author = {David Clark and Sebastian Hunt and Pasquale Malacaria},
  pdf = {http://staff.city.ac.uk/~sj353/papers/dagstuhl03.pdf},
  url = {http://www.dagstuhl.de/03411/},
  title = {Quantitative Analysis of Leakage of Confidential Information},
  note = {Presented at Dagstuhl Seminar 03411: Language Based Security},
  year = {2003},
  month = {October},
  abstract = {Programs whose high-inputs have no effect on their low-outputs are said
to satisfy the non-interference condition. We address the question
of what more can be said about programs which do not satisfy
non-interference.  We show how Shannon's information theory can be used
to define a measure of how much information a program
transmits from its high-inputs to its outputs.
We describe a quantitative analysis for a While language; the analysis
calculates bounds on the leakage into each variable under worst-case assumptions
of the choice of low-inputs.}
}

@article{CHH02,
  author = {David Clark and Chris Hankin and Sebastian Hunt},
  title = {Information flow for Algol-like languages},
  journal = {Computer Languages},
  volume = 28,
  number = 1,
  year = 2002,
  abstract = {In this paper we present an approach to information flow analysis
for a family of languages.  We start with a simple imperative language.
We present an information flow analysis using a {\em flow logic}.  The
paper contains detailed correctness proofs for this analysis.  We next
extend the analysis to a restricted form of Idealised Algol,
a call-by-value higher-order extension of the
simple imperative language (the key restriction being the lack of recursion).
The paper concludes with a discussion
of further extensions, including a probabilistic extension of Idealised
Algol.}
}

@article{CHM02,
  author = {David Clark and Sebastian Hunt and Pasquale Malacaria},
  url = {http://dx.doi.org/10.1016/S1571-0661(04)00290-7},
  pdf = {http://staff.city.ac.uk/~sj353/papers/qapl02.pdf},
  note = {QAPL'01, Quantitative Aspects of Programming Laguages (Satellite Event for PLI 2001)},
  title = {Quantitative Analysis of the Leakage of Confidential Data},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = 59,
  number = 3,
  year = 2002,
  month = {November},
  pages = {1--14},
  abstract = {Basic information theory is used to analyse the amount
of confidential information which may be leaked by programs
written in a very simple imperative language.
In particular, a detailed analysis is given of the possible leakage
due to equality tests and \texttt{if} statements.
The analysis is presented as a set of syntax-directed inference
rules and can readily be automated.}
}

@inproceedings{CHH00,
  author = {David Clark and Chris Hankin and Sebastian Hunt},
  ps = {http://staff.city.ac.uk/~sj353/papers/sas2000.ps.gz},
  title = {Safety of Strictness Analysis via Term Graph Rewriting},
  booktitle = {Proc. Static Analysis, 7th International Symposium, SAS 2000},
  address = {Santa Barbara, California, USA},
  month = {June},
  year = 2000,
  pages = {95--114},
  editor = {Jens Palsberg},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = 1824,
  abstract = {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 Concurrent
Clean compiler. Programs written in a core functional language are
interpreted as graph rewriting systems using a form of equational term
graph rewriting due to Ariola and Arvind.  Abstract graphs are defined
by extending the signature of ordinary graphs and it is shown how to
extend a rewriting system on ordinary graphs to one on abstract graphs.
An abstraction relation between abstract graphs is used to define
a notion of safety with respect to a variant of Ariola and Arvind's
direct approximation semantics, and this notion of safety is shown to
be adequate for strictness analysis. Abstract reduction is defined as
the union of the extended rewrite system with additional `heuristic'
reductions and shown to be safe.}
}

@techreport{HHR96,
  author = {John Hughes and Sebastian Hunt and Colin Runciman},
  pdf = {http://staff.city.ac.uk/~sj353/papers/space-monster.pdf},
  title = {Higher-order functions as decision trees: taming a space monster},
  institution = {City University},
  year = 1996,
  type = {Computer Science Technical Report Series},
  number = {1996/04}
}

@inproceedings{JJG96,
  author = {Michael Jampel and Jean-Marie Jacquet and David Gilbert and Sebastian Hunt},
  title = {Transformations between HCLP and PCSP},
  booktitle = {Proc. CP96: Second International Conference on Principles and Practice of Constraint Programming},
  address = {Cambridge, Massachusetts, USA},
  month = {August},
  year = 1996,
  pages = {252--266},
  editor = {Eugene C. Freuder},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science}
}

@inproceedings{JH95,
  author = {Michael Jampel and Sebastian Hunt},
  title = {Composition in Hierarchical CLP},
  booktitle = {Proc. IJCAI'95: International Joint Conference on Artificial Intelligence},
  pages = {640--645},
  publisher = {Morgan Kaufman},
  year = 1995
}

@article{HH94,
  author = {Chris Hankin and Sebastian Hunt},
  title = {Approximate fixed points in abstract interpretation},
  journal = {Science of Computer Programming},
  pages = {283--306},
  volume = 22,
  number = 3,
  year = 1994
}

@inproceedings{HH92,
  author = {Chris Hankin and Sebastian Hunt},
  title = {Approximate fixed points in abstract interpretation},
  booktitle = {Proc. ESOP'92: 4th European Symposium on Programming},
  pages = {219--232},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = 582,
  year = 1992
}

@article{HH91,
  author = {Chris Hankin and Sebastian Hunt},
  title = {Fixed points and frontiers: a new perspective},
  journal = {Journal of Functional Programming},
  number = 1,
  volume = 1,
  year = 1991
}

@inproceedings{HS91,
  author = {Sebastian Hunt and David Sands},
  ps = {http://staff.city.ac.uk/~sj353/papers/pepm91.ps.gz},
  title = {Binding time analysis: a new PERspective},
  booktitle = {Proc. PEPM'91: Symposium on Partial Evaluation and Semantics-Based Program Manipulation},
  publisher = {ACM Press},
  year = 1991
}

@phdthesis{Hun91a,
  author = {Sebastian Hunt},
  ps = {http://staff.city.ac.uk/~sj353/papers/thesis.ps.gz},
  title = {Abstract Interpretation of Functional Languages: From Theory to Practice},
  school = {Department of Computing, Imperial College of Science Technology and Medicine},
  year = 1991
}

@inproceedings{Hun91b,
  author = {Sebastian Hunt},
  ps = {http://staff.city.ac.uk/~sj353/papers/ullapool90.ps.gz},
  title = {PERs generalise projections for strictness analysis (extended abstract)},
  booktitle = {Proc. 1990 Glasgow Workshop on Functional Programming},
  address = {Ullapool},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  year = 1991
}

@inproceedings{Hun89,
  author = {Sebastian Hunt},
  ps = {http://staff.city.ac.uk/~sj353/papers/fpca89.ps.gz},
  title = {Frontiers and open sets in abstract interpretation},
  booktitle = {Proc. FPCA'89: 4th Conference on Functional Programming Languages and Computer Architectures},
  publisher = {ACM Press},
  year = 1989
}