Pasquale Malacaria. Risk Assessment of Security Threats for Looping Constructs. Journal of Computer Security 2010.
Download paper: Lagrange Multipliers and Maximum Information Leakage in Different Observational Models
[Proceedings of the 2008 workshop on Programming languages and analysis for security PLAS '08
Publisher: ACM Press]
What is this about?
This paper explores two fundamental issues in Language based security. The first is to provide a quantitative definition of information leakage valid in several attacker's models.
We consider attackers with different capabilities; the strongest one is able to observe the value of the low variables at each step during the execution of a program; the weakest one can only observe a single low value at some stage of the execution.
We will provide a uniform definition of leakage, based on Information Theory, that will allow us to formalize and prove some intuitive relationships between the amount leaked by the same program in different models.
The second issue is Channel Capacity, which in security terms amounts to answering the questions: given a program and an observational model, what is the maximum amount that the program can leak? And which input distribution causes the maximum leakage?
To answer those questions we will introduce techniques from constrained non-linear optimization, mainly Lagrange multipliers and we will show how they provide a workable solution in all observational models considered. In the simplest setting, i.e. under minimal constraints, we will show that channel capacity is achieved by any input distribution which induces a uniform distribution on the observables.
Download paper: Quantitative Analysis of Leakage for Multi-threaded Programs.
[Proceedings of the 2007 workshop on Programming languages and analysis for security PLAS '07
Publisher: ACM Press]
What is this about?
We present a quantitative
analysis of information flow for a multi-threaded language based on a
probabilistic scheduler.
The analysis consists of two steps. First multi-threaded programs are translated into a single loop with a probabilistic choice. Then an information theoretical semantics of loops with probabilistic operators
is used to derive the leakage.
Using this analysis classical examples of multi-threaded programs are revisited: it is shown how the analysis is able to deal with, among other, probabilistic leakage, internally observable timing leakage and leakage originated by observing intermediate states of computation.
Download paper: A static analysis for quantifying information flow in a simple imperative language.
[Journal of Computer Security 1 to 3 of 3
Issue: Volume 15, Number 3 / 2007]
Download paper:Assessing security threats of looping constructs.
What is this about?
[POPL2007]
There is a clear intuitive connection between the notion of leakage of information in a program
and concepts from information theory. This intuition has not been satisfactorily pinned down, until now.
In particular, previous information-theoretic models of programs are imprecise, due to their overly conservative treatment of looping constructs. In this paper we provide the first precise information-theoretic semantics of looping constructs. Our semantics describes both the amount and rate of leakage;
if either is small enough, then a program might be deemed ``secure''.
Using the semantics we provide an
investigation and classification of bounded and unbounded covert channels.
Download paper: Quantitative information flow, relations and polymorphic types.
What is this about?
[Journal of Logic and Computation, Special Issue on Lambda-calculus, type theory and natural language, 18(2):181-199, 2005.]
Shannon's information theory is used to give a quantitative definition of information flow in inputs/outputs systems. This 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.
Download paper: Quantitative Analysis of the Leakage of Confidential Data (pdf).
What is this about?
[Vol. 59, No.3 of Electronic Notes in Theoretical Computer Science, 2002] 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.
Download paper: David Clark, Sebastian Hunt, and Pasquale Malacaria. Quantified interference for a while language.
Presented at 2nd Workshop on Quantitative Aspects of Programming Languages (QAPL'04); to appear in Electronic Notes in Theoretical Computer Science, March 2004.
Download paper: 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.
Other publications on information theory, non intereference and security are available from the Publications section here
Game Semantics and Program Analysis:
Download paper: Full Abstraction for PCF (ps) .
Full Abstraction for PCF (pdf) .
What is this about?
In this paper [Information and Computation, Volume 163, Issue 2, 15 December 2000, Pages 409-470] we build a fully abstract model for PCF based on games.
Download paper: Non-deterministic Games and Program Analysis: An application to security (ps).
Non-deterministic Games and Program Analysis: An application to security (pdf).
What is this about?
In this paper,[LICS 99, IEEE Press] is shown how program analysis can be developped by using a lax functor from a game model to a category of non-deterministic games. An application of this techniques to the analysis of security leakage is discussed.
Download paper: Generalised Flowcharts and Games (ps).
Generalised Flowcharts and Games (pdf).
What is this about?
In this paper, [ICALP 98, LNCS 1443] (an abstract) game semantics is used to build a flowchart for higher-order languages.
Download paper: A New Approach to Control Flow Analysis (ps).
A New Approach to Control Flow Analysis (pdf).
What is this about?
Here [CC98, LNCS 1383] a cubic algorithm for implementing 0-cfa is described. 0-cfa determines statically which closures a program point can jump to during evaluation.
Other Topics:
Download paper: Studying equivalence of transition systems with algebraic tools (ps).
Studying equivalence of transition systems with algebraic tools (pdf).
What is this about?
[Theoretical Computer Science 95] A category of algebra Stone dual to the category of transition systems is defined. It is then proved that subalgebra isomorphism in this category of algebras is equivalent to bisimilarity in the category of transition systems.
Download paper: Relative Definability of Boolean Functions via Hypergraphs (ps).
Relative Definability of Boolean Functions via Hypergraphs (pdf).
What is this about?
[Theoretical Computer Science Volume 278, Issues 1-2, 6 May 2002, Pages 91-110 ] A category of hypergraph is defined in which to study the degrees of parallelism of boolean functions. Every function is associated an hypergraph and is proved that if two functions have isomorphic hypergraph then they are equiparallel.