Professor David J. Pym, MA (Cambridge), PhD (Edinburgh), ScD (Cambridge), FIMA, CMath, FBCS, CITP
Professor of Information, Logic, and Security at UCL
Faculty Fellow, Alan Turing Institute
David's UCL CS Page
Department of Computer Science
University College London
London WC1E 6BT
University of London
Telephone: 020 7679 0327 Internal: 30327
Email: j.savage (at) ucl.ac.uk
PhD studentships currently available
Logic for Decision Making in Security.
Main supervisor: Professor Guy McCusker, University of Bath
Second supervisor: Professor David Pym, University College London
Security breaches often arise as a result of users' failure to comply with security policies or follow good security practice, even when the implications of such behaviour are known to them. Simple examples include the use of unencrypted USB sticks for the transport of sensitive information, or connecting to public WiFi networks despite the well-known dangers of so doing. There is evidence that this failure to comply with policy arises from the perception that the benefit of compliance is outweighed by the reduction in users' ability to complete their tasks when complying. In recent work we have proposed a qualitative analysis of the concept of 'compliance budget': the idea that users have a finite budget of time and energy available for such costly compliance activities, beyond which they begin to deviate from secure behaviour. Compliance Budget Logic is a multi-modal logic incorporating a notion of preference which we use to describe and explain users' security decisions.
This PhD project will develop the theory and applications of this Compliance Budget Logic. The basic theory of the logic will be developed, followed by its application to security decision-making. For example, we may study how the interaction of multiple security policies and multiple budgets (e.g., users' own time, laptop battery life, etc.) may be described and analysed via our logic. Some of this work will be carried out in collaboration with leading security researchers at University College London.
Anticipated start date: 2 October 2017.
Anderson, G., McCusker, G. and Pym, D., 2016. A Logic for the Compliance Budget. In: Zhu, Q., Alpcan, T., Panaousis, E., Tambe, M. and Casey, W., eds. Proceedings, GameSec 2016: Decision and Game Theory for Security. Springer Verlag. Lecture Notes in Computer Science 9996: 370-381.
I have worked in a range of areas of mathematical logic and theoretical computer science, including type theory and logical frameworks, proof theory, categorical logic, substructural logic, resource semantics, and process algebra. In theses areas, I have always been particularly interested in the interplay between syntax and semantics.
In recent years, I have become engaged with mathematical systems modelling, with a particular interest in applying --- in the style of classical mathematical modelling as practised in, for example, engineering, where the control of complexity by abstraction is critically important in delivering useful models --- the ideas of compositional semantics and logic to complex systems, particularly in the social sciences and systems engineering. Computer security, system security, and information security provide excellent challenges for this approach. All this began around 2004, with an extended stay with the security research group at HP Labs, initially funded by a Royal Society Industry Fellowship.
My current research interests include the following:
Here is a link to a page about a film about the logic BI: Attack of the 50 Foot Spatial Dudes.
My latest book, a research monograph entitled A Discipline of Mathematical Systems Modelling, co-authored with Matthew Collinson and Brian Monahan, is published by the not-for-profit publisher College Publications.
The mathematization of the sciences, of engineering, and of economics has been an outstandingly successful intellectual enterprise, enabling the modern world. As the operations of the world become more and more dependent on highly interconnected, massively complex, networked systems of computational devices, the need to develop a mathematical understanding of their properties and behaviours is increasingly pressing.
Our approach, described in this monograph, is to combine the compositionality of formal specification --- using techniques from algebra, computation theory, logic, and probability theory --- with the control of level of abstraction afforded by the classical mathematical modelling method.
The first chapter provides a complete high-level view of the approach to systems modelling that is developed in the monograph. It provides both conceptual and philosophical background and introductions to the technical development. The remaining chapters develop the mathematical and computational aspects of our approach. Each chapter develops a specific mathematical or computational component, clearly integrated into the overall development. Examples, including ones based on industrial and commercial applications, are provided throughout. An implementation of a simulation engine (Core Gnosis) for executing models is available for download from HP Labs. Associated with this monograph is a website (http://www.hpl.hp.com/research/systems_security/gnosis.html) from which Core Gnosis may be obtained. This is book is about the conceptual and mathematical foundations of a modelling approach, with indications of how it can, and has been, deployed in practice. We defer to another occasion an account of the pragmatics of the deployment.
Available from Waterstones, Amazon UK, Amazon US, Amazon DE, and Amazon FR.
I am one of the designers of the Core Gnosis tool for systems and security modelling. The Core Gnosis system can be downloaded from HP Labs at http://www.hpl.hp.com/research/systems_security/gnosis.html, along with a paper
M. Collinson, B. Monahan, and D. Pym,
Semantics for Structured Systems Modelling and Simulation,
Proc. Simutools 2010, ACM Digital Library, ISBN: 978-963-9799-87-5
published at SIMUTools 2010.
Current Funded Projects
Recent Funded Projects (see Recent Publications and Manuscripts for associated papers)