Pasquale Malacaria Home Page

Pasquale Malacaria, Professor of Computer Science,

School of Electronic Engineering and Computer Science

Queen Mary University of London, Mile End Road, E1 4NS

+44 020 7 8826378

p.malacaria@qmul.ac.uk

Research interests: information theory, automated security analysis, verification, decision support for cybersecurity, optimization, game theory, semantics of programming languages, program analysis.

News:

Our cybersecurity investment tool based on the project Customized and Adaptive approach for Optimal Cybersecurity Investment (EPSRC 2017-2020) is here . The paper describing the maths behind the tool is here.

A nice blog entry discussing our work on generative adversarial neural networks for pseudo random number generators.

For publications please look at this dblp page.

Old news below

2017 papers:

2016 papers:

Information Leakage Analysis of Complex C Code and its Application to OpenSSL . In Proc ISOLA 2016
Efficient Numerical Frameworks for MultiObjective Cyber Security Planning . In Proc ESORICS 2016
Relative Perfect Secrecy: Universally Optimal Strategies and Channel Design . In Proc IEEE CSF 2016
Multi-run side-channel analysis using Symbolic Execution and Max-SMT . In Proc IEEE CSF 2016
Comparing Decision Support Approaches for Cyber Security Investment. In Decision Support Systems

2015 papers:

All-Solution Satisfiability Modulo Theories: applications, algorithms and benchmarks . In proceedings of the 10th International Conference on Availability, Reliability and Security (“ARES”) 2015.
Comparing Decision Support Approaches for Cyber Security Investment. (arxiv paper, a revised version of this paper has been accepted for publication by the journal Decision Support Systems)
A Game-Theoretic Approach for Minimizing Security Risks in the Internet-of-Things: IEEE Workshop on Security and Privacy for Internet of Things and Cyber-Physical Systems (IEEE ICC 2015 - IoT/CPS Security 2015)
Algebraic foundations for quantitative information flow in Mathematical Structure in Computer Science February 2015 : Mathematical Structure in Computer Science February 2015 (an old arxiv version is here ).

2014 papers:

Relating bounded model checking and symbolic execution: "Concurrent Bounded Model Checking" in Java Pathfinder Workshop 2014.
Quantification of leakage in markov chains: "Information Leakage of Non-Terminating Processes" in Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2014).
Game theory for cyber investments: "Cybersecurity Games and Investments: A Decision Support Approach" in GameSec2014.
Using reliability analysis for security analysis: "Quantifying Information Leaks using Reliability Analysis" (SPIN 2014).
Using game theory for optimal allocation of security administrators time, "Game Theory Meets Information Security Management" (IFIP SEC 2014).
A paper about a fast algorithm for quantitative information flow using abstract model counting: "Abstract model counting: a novel approach for quantification of information leaks." (ACM ASIACCS 2014).
A short paper on using multi-objective knapsack for optimal cyber-security investment: "How to Spend it: Optimal Investment for Cyber Security" (ACySe 2014).

A short video interview about the work on the Thermodynamics of confidentiality. Is on YouTube here (paper here ).

December 2013. Just back from Costa Rica where I participated in a very exciting workshop on information and processes.

On the theme of videos here is an older one filmed in 2011 at the Bellairs institute in Barbados, is a talk on Quantitative Information Flow (an algebraic introduction). Is on YouTube here.

ETAPS 2013 in Rome. Friday the 22nd was a very special ETAPS day. In the morning we celebrated Corrado Bohm 90th birthday. He was my master's supervisor and I was glad to be part of this celebration. In the afternoon there was a special session for our colleague and friend Kohei Honda who sadly passed away last December; I gave a talk/tribute about his work on Game Semantics.

ETAPS 2015 will be here at Queen Mary, me and Nikos Tzevelekos will co-chair the local organization

Jonathan has a very nice development to bitcoin mining of the techniques we introduced in the ACSAC paper. Read about it here.

Paper accepted at VMCAI 2013 . The paper is about leakage analysis of Markovian processes with application to randomized protocols.

I am involved in the Science of Cyber Security Research Institute. My involvement is as a PI in the project Games and Abstraction: The Science of Cyber Security. The project is about the use of Game Theory for decision support in CyberSecurity.

I am also involved in the Research Institute in Automated Program Analysis and Verification. My involvement is as a PI in the project on compositional security analysis for binaries

The paper "The Thermodynamics of Confidentiality" has been accepted for the 25th IEEE Computer Security Foundations Symposium . The overall contribution of this paper can be seen as laying down in a precise sense the thermodynamic foundations of confidentiality. In a follow up paper ("Thermodynamic Aspects of Confidentiality" in Information and Computation 2013 vol. 226 ) we extend this work to side channel analysis of Brownian Computers. We found out that there are timing channels in Brownian Computers that don't exist in ordinary computers. Can you guess what they are?

I recently organized, together with Boris Koepf and Catuscia Palamidessi the Daghstul seminar on Quantitative Security Analysis . It was from the 25th to the 30th of November 2012.

Recent work: quantitative analysis of leakage of real code, e.g. quantifying leakage of confidential information in the Linux Kernel. The paper ( ACSAC 2010 ) is here . Also current interests include game theoretical analysis for security risk assessment.

( PLAS 2008 , ASIACCS 2009) addresses the problem of maximal leakage of secure information, translating it into the information theoretical problem of channel capacity. The problem is then approached using Lagrange multipliers. We also use Lagrange Multipliers to compute loss of anonymity in anonymity protocols ( ASIACCS 2009 ).

Recent invited talks

Departmental Seminar, Department of Computer Science, University of Oxford, March 2014
Workshop on Information and Processes CIAPA, Costa Rica December 15 - 18, 2013
The 19th CREST Open Workshop Software. Interference and Dependence, UCL, London, May 2012
London Institute for Mathematical Sciences. Cybersecurity conference. April 2012
The 17th CREST Open Workshop Software. Testing and Verification, UCL, London, January 2012
Information Security as a Resource workshop, Oxford University, October 2011
Quantum and Classical Information flow workshop, Bellairs Institute, Barbados, April 2011
CAV 2010 invited speaker
10th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Quantitative Aspects of Programming Languages. Bertinoro 2010
QAPL 2010 invited speaker

Recent Program Committe membership:

the Sixth International Conference on Decision and Game Theory for Security, London 2015
The Second International Workshop on Agents and CyberSecurity ACySe 2015
IEEE ICC 2015 - IEEE Workshop on Security and Privacy for Internet of Things and Cyber-Physical Systems
Mathematical Foundations of Computer Science 2012
GaLoP 2010
Twenty-fifth Conference on the Mathematical Foundations of Programming Semantics (MFPS 09)
5th International Workshop on Programming Language Interference and Dependence ( PLID'09 ) .
ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security (PLAS 2009)
Workshop on Quantitative Analysis of Software
7th International Workshop on Security Issues in Concurrency (SecCo 2009)

Recent funding informations

principal investigator in the EPSRC project EP/K032011/1 "Compositional Security Analysis for Binaries" (2013-2016)
principal investigator in the EPSRC project EP/K005820/1 "Games and Abstraction: The Science of Cyber Security" (2013-2016)
principal investigator in the EPSRC project "Quantitative Information Flow"
principal investigator in the EPSRC project "Model Checking and Program Analysis for Quantifying Interference".
co-investigator in the EPSRC platform grant "Extreme Reasoning".
Interested in a PhD? Funding available, further details click here. Applicants should be able to show some knowledge and interest in my areas of research.

Also interested in applications of information theory to machine learning in particular Adaboost. Adaboost significantly boosts the performance of classifiers, which are algorithms that allow to classify new cases based on previous cases. An example could be a program which classify if a patient has/has not cancer given the symptoms based on a database of previous cases (this database is called the training set). In this paper we related Adaboost with Kelly's theory of optimal betting and by doing so we significantly simplify the Adaboost algorithm.

Past works: Game Semantics and its algorithmic applications. Game semantics provides a very fine graded analysis of computation. It has been used to successfully answer some open questions in the semantic of programming languages (Full abstraction for PCF, see publication sections). Here are some motivations for that work.

Publications' section

Corrado Bohm supervised my master thesis on second order lambda calculus. Another remarkable scientist, Jean-Yves Girard supervised my PhD on Stone duality. Samson Abramsky has been an inspiration and a source of support all along my career.

I'm an Associate Editor for the ACM Computing Surveys

PhD Students:

Former PhD Students:

Quoc-Sang Phan
Xujing Huan
Jonathan Heusser (2011)
Han Chen (2008)
Russ Harmer (1999)