Selected Publications

(bibtex data on most papers available here)





Pasquale Malacaria. Risk Assessment of Security Threats for Looping Constructs. Journal of Computer Security 2010.


Han Chen and Pasquale Malacaria. The Optimum Leakage Principle for Analyzing Multi-threaded Programs. In Proceedings of The 4th International Conference on Information Theoretic Security, December 2009, Shizuoka, Japan.


Jonathan Heusser and Pasquale Malacaria. Applied Quantitative Information Flow and Statistical Databases. In Proceedings of Workshop on Formal Aspects in Security and Trust (FAST 2009), November 2009, Eindhoven, the Netherlands.


Pasquale Malacaria and Fabrizio Smeraldi. On Adaboost and Optimal Betting Strategies. In Proceedings of the 2009 International Conference on Data Mining. July 2009, Las Vegas


Pasquale Malacaria. Program Analysis Probably Counts: Discussant Contribution for the Computer Journal Lecture by Chris Hankin. The Computer Journal, 2009; doi:10.1093/comjnl/bxp037


Han Chen and Pasquale Malacaria. Studying Maximum Information Leakage Using Karush-Kuhn-Tucker Conditions. In Proceedings of 7th International Workshop on Security Issues in Concurrency, Bologna, September 2009.


Jonathan Heusser and Pasquale Malacaria. Quantifying Loop Leakage using a Lattice of Partitions. In Proceedings of the 1st Workshop on Quantitative Analysis of Software (QA'09), June 2009 Grenoble.


Jonathan Heusser and Pasquale Malacaria. Lattice of Information and Quantitative Information Flow. In 5th International Workshop on Programming Language Interference and Dependence (PLID'09), April 2009, London


Han Chen and Pasquale Malacaria: Quantifying maximal loss of anonymity in protocols. In Proceedings of the 2009 ACM Symposium on Information, Computer and Communications Security, ASIACCS 2009, Sydney March 2009

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 paperQuantitative 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 paperQuantitative 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 paperDavid 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 paperDavid 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 paperNon-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 paperGeneralised 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 paperA 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 paperStudying 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 paperRelative 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.

Stone Duality for Stable Functions (pdf).
What is this about?
[Category Theory and Computer Science 1991] To define an algebraic structure for stable open subsets of a suitable domain; in the stable case this turn out to be a semilattice with least upper bounds of disjoint subset, the aim being to develop something similar to pointless topology, that is an algebraic insight of spaces.