[THS11] Filippo Del Tedesco, Sebastian Hunt, and David Sands. A semantic hierarchy for erasure policies. In Sushil Jajodia and Chandan Mazumdar, editors, ICISS, volume 7093 of Lecture Notes in Computer Science, pages 352-369. Springer, 2011. [ bib | .pdf ]
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.

[HS11] Sebastian Hunt and David Sands. From exponential to polynomial-time security typing via principal types. In Gilles Barthe, editor, ESOP, volume 6602 of Lecture Notes in Computer Science, pages 297-316. Springer, 2011. [ bib | .pdf ]
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.

[CH08] David Clark and Sebastian Hunt. Non-interference for deterministic interactive programs. In Proc. 5th International Workshop on Formal Aspects in Security and Trust (FAST2008), Lecture Notes in Computer Science, Malaga, Spain, October 2008. Springer-Verlag. [ bib | .pdf ]
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.

[AHSS08] Aslan Askarov, Sebastian Hunt, Andrei Sabelfeld, and David Sands. Termination-insensitive noninterference leaks more than just a bit. In Proc. 13th European Symposium on Research in Computer Security (ESORICS'08), volume 5283 of Lecture Notes in Computer Science, Malaga, Spain, October 2008. Springer-Verlag. [ bib | .pdf ]
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 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.

[HS08b] Sebastian Hunt and David Sands. Just forget it: The semantics and enforcement of information erasure. Extended version of [HS08a] including proofs, April 2008. [ bib | .pdf ]
[HS08a] Sebastian Hunt and David Sands. Just forget it: The semantics and enforcement of information erasure. In Proc. 17th European Symposium on Programming (ESOP'08), volume 4960 of Lecture Notes in Computer Science, Budapest, Hungary, March 2008. Springer-Verlag. [ bib | .pdf ]
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.

[CH07] David Clark and Sebastian Hunt. Non-interference for interactive programs. Presented at Third International Workshop on Programming Language Interference and Dependence (PLID'07), satellite workshop of SAS'07, August 2007. [ bib | http | .pdf ]
[CHM07] David Clark, Sebastian Hunt, and Pasquale Malacaria. A static analysis for quantifying information flow in a simple imperative language. Journal of Computer Security, 15(3):321-371, 2007. [ bib | .pdf ]
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 L1 inequalities to provide reasonable bounds for conditional statements. While-loops are handled by integrating a qualitative flow-sensitive dependency analysis into the quantitative analysis.

[HS06] Sebastian Hunt and David Sands. On flow-sensitive security types. In Proc. Principles of Programming Languages, 33rd Annual ACM SIGPLAN - SIGACT Symposium (POPL'06), pages 79-90, Charleston, South Carolina, USA, January 2006. ACM Press. [ bib | .pdf ]
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.

[HM05] Sebastian Hunt and Isabella Mastroeni. The per model of abstract non-interference. In R. Giacobazzi, editor, Proc. Static Analysis, 12th International Symposium (SAS'05), volume 3184 of Lecture Notes in Computer Science, pages 100-115. Springer-Verlag, 2005. [ bib | .pdf ]
[CHM05b] David Clark, Sebastian Hunt, and Pasquale Malacaria. Quantitative information flow, relations and polymorphic types. Journal of Logic and Computation, Special Issue on Lambda-calculus, type theory and natural language, 18(2):181-199, 2005. [ bib | http ]
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.

[CHM05a] David Clark, Sebastian Hunt, and Pasquale Malacaria. Quantified interference for a while language. Electronic Notes in Theoretical Computer Science, 112:149-166, January 2005. Proceedings of the Second Workshop on Quantitative Aspects of Programming Languages (QAPL 2004). [ bib | http | .pdf ]
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.

[CHM04a] David Clark, Sebastian Hunt, and Pasquale Malacaria. Non-interference for weak observers. Presented at First International Workshop on Programming Language Interference and Dependence (PLID'04), satellite workshop of SAS'04, August 2004. [ bib | .html | .pdf ]
[CHM04b] David Clark, Sebastian Hunt, and Pasquale Malacaria. Quantified interference: Information theory and information flow. Presented at Workshop on Issues in the Theory of Security (WITS'04), April 2004. [ bib | .pdf ]
[CHM03a] David Clark, Sebastian Hunt, and Pasquale Malacaria. Quantified interference for a While language. Technical Report TR-03-07, Department of Computer Science, King's College London, October 2003. [ bib | .ps ]
[CHM03b] David Clark, Sebastian Hunt, and Pasquale Malacaria. Quantitative analysis of leakage of confidential information. Presented at Dagstuhl Seminar 03411: Language Based Security, October 2003. [ bib | http | .pdf ]
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.

[CHM02] David Clark, Sebastian Hunt, and Pasquale Malacaria. Quantitative analysis of the leakage of confidential data. Electronic Notes in Theoretical Computer Science, 59(3):1-14, November 2002. QAPL'01, Quantitative Aspects of Programming Laguages (Satellite Event for PLI 2001). [ bib | http | .pdf ]
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 if statements. The analysis is presented as a set of syntax-directed inference rules and can readily be automated.

[CHH02] David Clark, Chris Hankin, and Sebastian Hunt. Information flow for algol-like languages. Computer Languages, 28(1), 2002. [ bib ]
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 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.

[CHH00] David Clark, Chris Hankin, and Sebastian Hunt. Safety of strictness analysis via term graph rewriting. In Jens Palsberg, editor, Proc. Static Analysis, 7th International Symposium, SAS 2000, number 1824 in Lecture Notes in Computer Science, pages 95-114, Santa Barbara, California, USA, June 2000. Springer-Verlag. [ bib | .ps.gz ]
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.

[JJGH96] Michael Jampel, Jean-Marie Jacquet, David Gilbert, and Sebastian Hunt. Transformations between hclp and pcsp. In Eugene C. Freuder, editor, Proc. CP96: Second International Conference on Principles and Practice of Constraint Programming, Lecture Notes in Computer Science, pages 252-266, Cambridge, Massachusetts, USA, August 1996. Springer-Verlag. [ bib ]
[HHR96] John Hughes, Sebastian Hunt, and Colin Runciman. Higher-order functions as decision trees: taming a space monster. Computer Science Technical Report Series 1996/04, City University, 1996. [ bib | .pdf ]
[JH95] Michael Jampel and Sebastian Hunt. Composition in hierarchical clp. In Proc. IJCAI'95: International Joint Conference on Artificial Intelligence, pages 640-645. Morgan Kaufman, 1995. [ bib ]
[HH94] Chris Hankin and Sebastian Hunt. Approximate fixed points in abstract interpretation. Science of Computer Programming, 22(3):283-306, 1994. [ bib ]
[HH92] Chris Hankin and Sebastian Hunt. Approximate fixed points in abstract interpretation. In Proc. ESOP'92: 4th European Symposium on Programming, number 582 in Lecture Notes in Computer Science, pages 219-232. Springer-Verlag, 1992. [ bib ]
[HH91] Chris Hankin and Sebastian Hunt. Fixed points and frontiers: a new perspective. Journal of Functional Programming, 1(1), 1991. [ bib ]
[HS91] Sebastian Hunt and David Sands. Binding time analysis: a new perspective. In Proc. PEPM'91: Symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM Press, 1991. [ bib | .ps.gz ]
[Hun91a] Sebastian Hunt. Abstract Interpretation of Functional Languages: From Theory to Practice. PhD thesis, Department of Computing, Imperial College of Science Technology and Medicine, 1991. [ bib | .ps.gz ]
[Hun91b] Sebastian Hunt. Pers generalise projections for strictness analysis (extended abstract). In Proc. 1990 Glasgow Workshop on Functional Programming, Workshops in Computing, Ullapool, 1991. Springer-Verlag. [ bib | .ps.gz ]
[Hun89] Sebastian Hunt. Frontiers and open sets in abstract interpretation. In Proc. FPCA'89: 4th Conference on Functional Programming Languages and Computer Architectures. ACM Press, 1989. [ bib | .ps.gz ]