David Pym's research portrait

Conceptual, economic, and mathematical modelling of the incentives, costs, and values of information security policies, processes, and technologies


David Pym, Professor of Information, Logic, and Security, uses formal logic and economics to create mathematical models that make it possible to reason about security practices.

Mathematical modelling is more familiar from engineering, where it's used to study complex systems — such as a bridge or weather — and understand how they work in order to make practical decisions. For example, an engineer wishing to calculate the weight a mediaeval bridge can sustain can't take the bridge apart to study its internal design in detail. But the engineer can, based on background and experience, look at how the bridge is built and pick out the key features — such as specific pieces of wood and bolts — and estimate what they can bear. As Pym explains, some details are always left out in the interests of simplifying the model enough to be able to calculate it in a reasonable amount of time. Turning to computer science, these methods, he says, "have turned out to be quite effective for thinking about security problems". 

Pym can't name any particular impetus for choosing mathematics.

"Mathematics was always easy," he says.

He began with an undergraduate degree in general mathematics at Cambridge followed by a PhD in the mathematical theory of computation at Edinburgh. His thesis was on logic. Following a post-doc at Edinburgh, he spent a year in Birmingham before landing at Queen Mary College, where he arrived as a lecturer and left seven years later a full professor helped by support from an EPSRC Advanced Fellowship. In his next job, at Bath, Pym became involved with HP Labs in Bristol, initially supported by a Royal Society Industry Fellowship: a watershed in his thinking.

"Until I moved to Bath I was very much doing logic and theoretical computer science," he says. HP offered him the chance to test whether his ideas could be of use in large-scale systems. The experience led him into information security. "HP has one of the best security research groups anywhere, and it was natural to learn what I could in that environment." In addition, HP's customer base offered many real-world challenging problems. "It was a really beautiful environment. You could do fundamental thinking but also have access to very well-grounded problems with the company's customers."

The combination of a formal mathematics background and the security problems and systems he encountered at HP led Pym to propose the Trust Economics project (PDF), funded by the Technology Strategy Board. This work incorporates the key idea of utility theory from economics into mathematical models, based on ideas from algebra and logic, that can be used to simulate the dynamic threats and complex decision-making common to security problems.

"These are two of the major ways of thinking about the world," he says of economics and logic,"and they're very different. Logic is about the structure of things, how things are composed together, and how you build up complex things from simpler things. Economics is about understanding strategy, value, trade-offs, and preferences. Both are required to get a good understanding of reasoning when you think about trust."

A follow-up project that also began while Pym was at HP and concluded while Pym was 6th Century Chair in Logic at the University of Aberdeen, Cloud Stewardship Economics, applied these ideas to cloud computing.

In addition, he says, the process of working out what and whom to trust is a costly one. Take, for example, a bank assessing a lender: "It costs money to establish that by doing credit checks and interviews. How much of your resource are you prepared to expend to establish whether something you might want to trust is trustworthy?

Another  project, that began,  while Pym was at Aberdeen, involved HP, Perpetuity, the Universities of Birmingham and Oxford, and concluded at UCL is Trust Domains which applied ideas from logic and economics to model how agents decide to trust parts of their environments.  .

The next step is a new ESPRC/ESRC-funded four-year effort beginning in November 2013 called Algebra and Logic for Policy and Utility in Information Security (ALPUIS). This research project spans both the groups Pym participates in at UCL, the Information Security Group (and its Academic Centre of Excellence in Cyber Security) and the Programming Principles, Logic, and Verification Group, which he heads and which includes Peter O'Hearn, with whom Pym worked at Queen Mary on ideas in semantics that became the foundation for separation logic, a way of reasoning about how computer programs interact with a computer’s resources.

ALPUIS, supported by RCUK’s Global Uncertainties Programme, extends utility theory further into reasoning about security systems. In economics, utility theory is concerned with the value of the outcome of actions - how you make choices and the value to you of each possibility. But the idea of action in that context is unstructured and not analysed: "An action could be very trivial or very complex; utility theory doesn't make any kind of distinction." But, says Pym, "We know from logic and theoretical science that it's actually possible to give a completely compositional theory of what it is to be an action. We call this "process algebra". In other words, it's possible to break apart the complex structure to understand how it arises from simpler structures. So part of the ALPUIS project is "rebuilding utility theory on this compositional basis".

Pym adds, "That's important when you're trying to design policies to regulate the behaviour of complicated systems. Security is a really good example because the properties you care about are very complex and very interdependent. But they're also things people have to care about. It's a good problem to tackle."





This page was last modified on 15 Jan 2014.

Dr Emiliano De Cristofaro





+44 020 7679 0349


+44 020 3108 5040


E.DeCristofaro (at) cs.ucl.ac.uk