Professor David J. Pym, MA (Cambridge), PhD (Edinburgh), ScD (Cambridge), FIMA, CMath, FBCS, CITP, CSci
6th Century Chair in Logic, and SICSA Professor of Computing Science
University of Aberdeen. Honorary Professor in Heriot-Watt's School of Mathematical and Computer Sciences.

University of Aberdeen
King's College
Aberdeen AB24 3UE
Scotland, U.K.

Room: 235 Meston
Email: David Pym
Telephone: +44 (0)1 224 27 4577
Fax: +44 (0)1 224 27 2943

Director of Cyber-security Research, National Grid.

• Recent Publications and Manuscripts

My latest book, a research monograph entitled A Discipline of Mathematical Systems Modelling, co-authored with Matthew Collinson and Brian Monahan, has just been published by the open-access publisher College Publications.

Preface

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.

Other Monographs

• Reductive Logic and Proof-search: Proof Theory, Semantics, and Control, joint work with Eike Ritter, published by Oxford University Press in its Oxford Logic Guides series. Here is the page for its Errata and Remarks.
• The Semantics and Proof Theory of the Logic of Bunched Implications, together with its Errata and Remarks (also here), published by Springer. Here is the home page for BI, the Logic of Bunched Implications. Here is a link to a movie about BI.

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 and EU Digital Library, ISBN: 978-963-9799-87-5

published at SIMUTools 2010.

Research Interests

My research interests can be usefully organized into three groups.

• Security, security management, and the economics of information security and information ecosystems is concerned with conceptual, economic, and mathematical modelling of the incentives, costs, and values of information security policies, processes, and technologies. As such, it requires, social, economic, cognitive, and technological questions to be addressed and integrated.

  The following are currently key topics for my research:

  • conceptual and mathematical models of security architectures;
  • security policy and security management;
  • information stewardship, a notion that extends core security concepts to address issues such as sustainability and resilience, and which is given sharp focus by the development of, for example, cloud-based services ecosystems and other complex systems of information flows;
  • information stewardship economics;
  • utility- and logic-based models of trust in systems models; and
  • dynamic modelling and game-theoretic modelling of attack--defence postures.

• Logic may be seen as the study of the structure and communication of information, and logicians study reasoning about the structure and communication of information, and its formal representation. Mathematicians study abstract structure and the modelling of conceptual and physical systems. Computer engineers study and build systems that are able to represent models of conceptual and physical systems and which are able to communicate with other systems. Philosophers study the nature of ideas, of language, of entities, and of artefacts. My research involves something of all these things, and includes ideas from semantics/model theory, proof theory, category theory, and computation theory. It draws upon ideas from, and contributes to, classical, constructive, intuitionistic, substructural, modal, and process logic.

  Applications to information flow and trust, to systems modelling, to the semantics of computation, and to economics-based reasoning about systems and behaviour.

• Systems thinking and systems modelling using rigorous methods --- empirical, experimental, and mathematical --- to understand the design and behaviour of information systems, including users, and including policies. Particular focus on mathematical systems modelling, on modelling security, information flow, and trust concepts in this context, and on integrating mathematical and economic (e.g., utility-theoretic) systems modelling. In this context, techniques from algebra, logic, and probability theory are particularly important.

  Applications to utility computing (e.g., cloud) and security (information and physical, design, and policy).

I am currently interested in, and interested in supervising PhD students in, the following areas (in no particular order):

• Conceptual and mathematical, compositional, models of security architectures;
• Security policy and security management;
• Mathematical systems modelling, using algebraic, logical, and stochastic methods, with applications in information security;
• The mathematical structure of complex systems;
• The economics of systems thinking;
• The economics of information security;
• Topics connecting logic (substructural, modal; process algebra) and utility theory;
• Topics in security related to information flow and trust domains;
• Topics in logic related to information flow and trust domains;
• Airport/transport security;
• Topics related to information security, information stewardship, and cloud computing;
• Topics in logic related to the theory of search spaces.

Current Funded Projects

• Cloud Stewardship Economics: Securing the New Business Infrastructure (TSB funding, scientific leader, consultant to HP Labs). This project is concerned with economics of cloud computing. In particular, it is concerned with the economics of information stewardship in cloud computing ecosystems. Partners in the project are HP Labs (lead site; Simon Shiu, Project Manager), the University of Aberdeen's Business School, the University of Bath, Validsoft, Sapphire, and Marmalade Box.

• Trust Domains (TSB and RCUK Digital Economy Programme funding). Our partners are HP Labs, Bristol (lead site; Adrian Baldwin, Project Manager), Perpetuity Group, University of Birmingham, and University of Oxford. 3 years from 1 April, 2011.

  Here is HP Labs' flyer for the Trust Domains project.

• SECONOMICS (EU FP7 funding; with Julian Williams, Fabio Massacci, Robert Coles, and others). Socio-economic aspects of security policy. Various European partners including National Grid.

• SeRTES (EPSRC funding, joint with Warwick, LSE, City, Edinburgh, and Newcastle). Sense-making representations of technologically-enabled ecosystems. IT-as-a-Utility pilot project, 12 months from 1 April, 2012.

• Productive Security (EPSRC Funding, part of the GHCQ Research Institute in the Science of Security, joint with Angela Sasse at UCL). Modelling of systems and behaviour to support reasoning and decision-making in security policy design. 42 months from 1 October, 2012.

• Algebra and Logic for Policy and Utility in Information Security (ESRC/EPSRC CEReS Call funding, joint with Guy McCusker at Bath). 42 months from 1 October, 2013.

Recent Funded Projects (see Recent Publications and Manuscripts for associated papers)

• Trust Economics (TSB Funding, Project Manager and scientific leader, consultant to HP Labs). This project takes a whole-systems view of information security, including economic, human, and technologicial issues. Partners in the project are HP Labs, the Universities of Bath and Newcastle, and UCL. National Grid is closely associated with the project.
• The Semantics of Classical Proofs (EPSRC funding, with Martin Hyland and Edmund Robinson). This project developed categorical models for the (propositional) classical sequent calculus, establishing soundness and completeness results, and making connections with proof nets, the Geometry of Interaction, and related ideas. Richard McKinley's (Bath) PhD thesis (supervised by Pym and Führmann) extended the ideas to classical predicate logic and made some connections with the calculus of structures and classical model theory.
• Bunched ML (EPSRC funding, with Peter O'Hearn and Edmund Robinson). This project developed type systems and categorical models for ML-like languages with type systems using the substructural constructs of bunched logic. Compared to languages using the usual ML-like type systems, such languages have cleaner treatments of concepts in memory management such as locations, regions, allocation, and disposal.