More about my current research can be found on my research page. The following paragraphs describe the evolution of my research interests from logic to computer science to information security.

My undergraduate study was in Mathematics at the University of Edinburgh, during which I developed an interest in logic. I followed this with an MSc in Mathematical Logic at the University of Manchester. My dissertation was entitled Proof Theory and Semantics of Some Classical and Intuitionistic Modal Logics. A partial synopsis in a technical report Semantics and Proof Theory of an Intuitionistic Modal Sequent Calculus is still occasionally cited.

I completed my PhD in the Mathematical Foundations subgroup of the Formal Methods Group in the Department of Computer Science at the University of Manchester in 2002. The thesis, entitled Modality, Topology and Computation, was principally focussed on category-theoretic and topological constructions in the semantics of intuitionistic modal logic, but also considered applications to programming language semantics and dynamic logics for reasoning about programs.

From 2003 to 2006 I worked in the Mathematical Foundations of Computation Group in the Department of Computer Science at the University of Bath. The position was on an EPSRC-funded project Bunched ML, under the direction of David Pym with whom I have now collaborated for many years, and also in collaboration with Peter O' Hearn, Edmund Robinson and Josh Berdine at Queen Mary, University of London. The project investigated applications of logics for resource reasoning (bunched logics and separation logics) in the theory of functional programming. With Pym and Robinson, I developed a new form of substructural polymorphic type theory. Publications arising from this work appeared at the Computer Science Logic and Mathematical Foundations of Programming Semantics conferences, at workshops, and in the journal Mathematical Structures in Computer Science.

I moved to Hewlett-Packard Laboratories in Bristol in 2006. I worked initially as a research programmer, coding model-checkers for concurrent systems using functional programming languages. My position was in the Trusted Systems Lab (later renamed the Systems Security Lab) and the intended application was formal verification of security properties. At the same time, this led to a number of developments in the theory of process calculus and the theory of concurrency, again building on resource logics. The process calculus was further applied to formal modelling of access control and authentication.

Alongside the formal modelling work, it was necessary to provide tools and techniques in support of enterprise security decision-making, particularly at the strategic and investment level (for example, considered by Chief Information Security Officers). In that world, the time value of decisions is critical, but the relevant underlying systems detail remains complex, so we moved to the development of simulation tools. My colleagues and I designed and built a simulation system, Gnosis, with this in mind. In order to make reasoning about models relatively simple and unconfusing, this was designed to have a quite simple semantics, building on the process calculus ideas, and implemented in the functional language OCAML.

The Gnosis system additionally supports economic decision-making encapsulating stakeholder preferences regarding outcomes of models. The system was develped alongside a TSB-funded project Trust Economics with a number of academic collaborators. It has been applied to security modelling for real corporate security decisions, and was used as the main modelling tool in the Security Analytics service offered to customers by HP Enterprise Security. The opportunity to work with experienced security researchers, business security professionals and economists was very valuable. Parts of the work were reported at the International Conference on Simulation Tools and Techniques (Simutools) conference, and in the journals Formal Aspects of Computing, the Journal of Logic and Computation, and Mathematical Structures in Computer Science. The work is summarized in a book A Discipline of Mathematical Systems Modelling.

discipline

I moved to Aberdeen to take up a permanent appointment as a lecturer in 2010. I have continued to work on aspects of logic, developing with colleagues a logic for reasoning about layered graphs, and applications of this to access control policy models.

From 2011-2014 I participated as an investigator in the RCUK/TSB-funded grant Trust Domains looking at security considerations for organizational information sharing, with various academic and industrial partners. For more information see here.

From 2012-2015, I was an invesigator on the EU FP7 grant Socio-economics Meets Security (Seconomics). This project was highly interdisciplinary and involved a number of industrial and academic partners. My own work involved the design and analysis of economic, game-theoretic models of security policy, and computational visualization tools. The particular policy question that was my main focus regarded the consequences of cyber-security regulation in critical infrastructure. Formulation of the models was done in close collaboration with the information security team at National Grid and my colleague Julian Williams. A synopsis is to appear in IEEE Security & Privacy.

secon

Recent PhD students (with shared supervision in the Aberdeen model) include:

  • Kevin McDonald, University of Aberdeen, 2010-2014, graduated 2014. Thesis title: Modelling Multi-layered Network and Security Architectures using Mathematical Logic. Funding: EPSRC Doctoral Training Grant and RCUK Digital Economy programme.
  • Barry Taylor, University of Aberdeen, 2010-2014, graduated 2015. Thesis title: Identifying Vulnerabilities and Controls in Complex Composite Security Architectures. Funding: EPSRC Doctoral Training Grant and RCUK Digital Economy programme.
  • Robert (Bob) A.K. Duncan, University of Aberdeen, 2011-2016, thesis successfully defended 2016. Thesis title: Accounting for Stewardship in the Cloud. Bob's work has gone on to win best paper awards at cloud computing conferences, see IARIA Cloud Computing 2016 and Enterprise Security 2015 at IEEE CloudCom 2015 .

A description of my current work can be found on my research page.