Practicing a Science of Security: A Philosophy of Science Perspective. Joint work with Jonathan Spring and Tyler Moore.
Abstract. Our goal is to refocus the question about cybersecurity research from `is this process scientific' to `why is this scientific process producing unsatisfactory results'. We focus on five common complaints that claim cybersecurity is not or cannot be scientific. Many of these complaints presume views associated with the philosophical school known as Logical Empiricism that more recent scholarship has largely modified or rejected. Modern philosophy of science, supported by mathematical modeling methods, provides constructive resources to mitigate all purported challenges to a science of security. Therefore, we argue the community currently practices a science of cybersecurity. A philosophy of science perspective suggests the following form of practice: structured observation to seek intelligible explanations of phenomena, evaluating explanations in many ways, with specialized fields (including engineering and forensics) constraining explanations within their own expertise, inter-translating where necessary. A natural question to pursue in future work is how collecting, evaluating, and analyzing evidence for such explanations is different in security than other sciences.
In Proc. New Security Paradigms Workshop, Islamorada, FL, USA, 2-4 Oct, 2017 (NSPW 2017), 18 pages. DOI: 10.475/xxx_x. Manuscript.
The U.S. Vulnerabilities Equities Process: An Economic Perspective. Joint work with Tristan Caulfield and Christos Ioannidis.
Abstract. The U.S. Vulnerabilities Equities Process (VEP) is used by the government to decide whether to retain or disclose zero day vulnerabilities that the government possesses. There are costs and benefits to both actions: disclosing the vulnerability allows the the vulnerability to be patched and systems to be made more secure, while retaining the vulnerability allows the government to conduct intelligence, offensive national security, and law enforcement activities. While redacted documents give some information about the organization of the VEP, very little is publicly known about the decision-making process itself, with most of the detail about the criteria used coming from a blog post by Michael Daniel, the former White House Cybersecurity Coordinator. Although the decision to disclose or retain a vulnerability is often considered a binary choice---to either disclose or retain---it should actually be seen as a decision about timing: to determine when to disclose. In this paper, we present a model that shows how the criteria could be combined to determine the optimal time for the government to disclose a vulnerability, with the aim of providing insight into how a more formal, repeatable decision-making process might be achieved. We look at how the recent case of the WannaCry malware, which made use of a leaked NSA zero day exploit, EternalBlue, can be interpreted using the model.
To appear, Proc. GameSec 2017, Vienna, October 2017. Manuscript.
A Stone-type duality theorem for Separation Logic via its underlying bunched logics. Joint work with Simon Docherty.
Abstract. Stone-type duality theorems, which relate algebraic and relational/topological models, are important tools in logic because --- in addition to elegant abstraction --- they strengthen soundness and completeness to a categorical equivalence, yielding a framework through which both algebraic and topological methods can be brought to bear on a logic. We give a systematic treatment of Stone-type duality theorems for the structures that interpret bunched logics, starting with the weakest systems, recovering the familiar Boolean BI, and concluding with Separation Logic. Our results encompass all the known existing algebraic approaches to Separation Logic and prove them sound with respect to the standard store-heap semantics. We additionally recover soundness and completeness theorems of the specific truth-functional models of these logics as presented in the literature. This approach synthesises a variety of techniques from modal, substructural and categorical logic and contextualises the 'resource semantics' interpretation underpinning Separation Logic amongst them. As a consequence, theory from those fields --- as well as algebraic and topological methods --- can be applied to both Separation Logic and the systems of bunched logics it is built upon. Conversely, the notion of indexed resource frame (generalizing the standard model of Separation Logic) and its associated completeness proof can easily be adapted to other non-classical predicate logics.
To appear, Proc. MFPS 2017, ENTCS. Manuscript.
Intuitionistic Layered Graph Logic. Joint work with Simon Docherty.
Abstract. Models of complex systems are widely used in the physical and social sciences, and the concept of layering, typically building upon graph-theoretic structure, is a common feature. We describe an intuitionistic substructural logic that gives an account of layering. As in other bunched systems, the logic includes the usual intuitionistic connectives, together with a non-commutative, non-associative conjunction (used to capture layering) and its associated implications. We give a soundness and completeness theorem for a labelled tableaux system with respect to a Kripke semantics on graphs. To demonstrate the utility of the logic, we show how to represent systems and security examples, illuminating the relationship between services/policies and the infrastructures/architectures to which they are applied.
Abrdiged version to appear in the IJCAI 2017 Sister Conference Best Paper Track. Manuscript.
Why Separation Logic Works. Joint work with Jonathan Spring and Peter O'Hearn.
Abstract. One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer's conceptual model of a program's manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it deploys a proof theory that meets the engineer's design goals of timely and explanatory prediction of errors. Separation Logic is an interesting case because of its widespread success in verification tools used by Facebook and others daily. For these two senses of model --- the engineering/conceptual and the logical --- to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, the development of both the logic and engineering benefit greatly. Seeking this intersection of two different senses of model provides a strategy for how computer scientists and logicians may be successful. Furthermore, the history of Separation Logic for analysing programs provides a novel case for philosophers of science of how software engineers and computer scientists develop models and the components of such models. We provide three contributions: an exploration of the extent of models merging that is necessary for success in computer science; an introduction to the technical details of Separation Logic, which can be used for reasoning about other exhaustible resources; and an introduction to (a subset of) the problems, process, and results of computer scientists for those outside the field.
Manuscript, 2017.
A logic for the compliance budget. Joint work with Gabrielle Anderson and Guy McCusker.
Abstract. Security breaches often arise as a result of users' failure to comply with security policies. Such failures to comply may simply be innocent mistakes. However, there is evidence that, in some circumstances, users choose not to comply because they perceive that the security benefit of compliance is outweighed by the cost that is the impact of compliance on their abilities to complete their operational tasks. That is, they perceive security compliance as hindering their work. The `compliance budget' is a concept in information security that describes how the users of an organization's systems determine the extent to which they comply with the specified security policy. The purpose of this paper is to initiate a qualitative logical analysis of, and so provide reasoning tools for, this important concept in security economics for which quantitative analysis is difficult to establish. We set up a simple temporal logic of preferences, with a semantics given in terms of histories and sets of preferences, and explain how to use it to model and reason about the compliance budget. The key ingredients are preference update, to account for behavioural change in response to policy change, and an ability to handle uncertainty, to account for the lack of quantitative measures of the compliance budget.
Manuscript. Proc. GameSec 2016, New York City, November 2016. LNCS 9996:370-381, 2016.
A Substructural Epistemic Resource Logic. Joint work with D. Galmiche and P. Kimmel.
Abstract. We present a substructural epistemic logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents' local resources. The new modalities can be seen as generalizations of the usual epistemic modalities. The logic combines Boolean BI's resource semantics with epistemic agency. We give a labelled tableaux calculus and establish soundness and completeness with respect to the resource semantics. We illustrate the use of the logic by discussing an example of side-channels in access control using resource tokens.
Manuscript. Revised version to appear in Proc. ICLA 2017, Kanpur, India, January 2017.
An extended version, including all proofs, is available as UCL Computer Science Research Note RN/16/08.
On the adoption of privacy-enhancing technologies. Joint work with Tristan Caulfield and Christos Ioannidis.
Abstract. We propose a model, based on the work of Brock and Durlauf, which looks at how agents make choices between competing technologies, as a framework for exploring aspects of the economics of the adoption of privacy-enhancing technologies. In order to formulate a model of decision-making among choices of technologies by these agents, we consider the following: context, the setting in which and the purpose for which a given technology is used; requirement, the level of privacy that the technology must provide for an agent to be willing to use the technology in a given context; belief, an agent's perception of the level of privacy provided by a given technology in a given context; and the relative value of privacy, how much an agent cares about privacy in this context and how willing an agent is to trade off privacy for other attributes. We introduce these concepts into the model, admitting heterogeneity among agents in order to capture variations in requirement, belief, and relative value in the population. We illustrate the model with two examples: the possible effects on the adoption of iOS devices being caused by the recent Apple--FBI case; and the recent revelations about the non-deletion of images on the adoption of Snapchat.
Manuscript. Proc. GameSec 2016, New York City, November 2016. LNCS 9996:175-194, 2016.
A substructural modal logic of utility. Joint work with Gabrielle Anderson.
Abstract. We introduce a substructural modal logic of utility that can be used to reason about optimality with respect to properties of states. Our notion of state is quite general, and is able to represent resource allocation problems in distributed systems. The underlying logic is a variant of the modal logic of bunched implications, and based on resource semantics, which is closely related to concurrent separation logic. We consider a labelled transition semantics and establish conditions under which Hennessy-Milner soundness and completeness hold. By considering notions of cost, strategy, and utility, we are able to formulate characterizations of Pareto optimality, best responses, and Nash equilibrium within resource semantics. We also show that our logic is able to serve as a logic for a fully featured process algebra and explain the interaction between utility and the structure of processes.
Manuscript. Journal of Logic and Computation, 27(5): 1421-1464. https://doi.org/doi:10.1093/logcom/exw030.
A Logic of Separating Modalities. Joint work with J.-R. Courtault and D. Galmiche.
Abstract. We present a logic of separating modalities, LSM, that is based on Boolean BI. LSM's modalities, which generalize those of S4, combine, within a quite general relational semantics, BI's resource semantics with modal accessibility. We provide a range of examples illustrating their use in a range of examples from computer science. We give a proof system based on the method of labelled tableaux with countermodel extraction, establishing its soundness and completeness with respect to the resource semantics.
Theoretical Computer Science 637, 30-58, 2016. doi: 10.1016/j.tcs.2016.04.040. Manuscript.
Contagion in Cybersecurity Attacks. Joint work with Adrian Baldwin, Iffat Gheyas, Christos Ioannidis, and Julian Williams.
Abstract. Systems security is essential for the efficient operation of all organizations Indeed, most large firms employ a designated `Chief Information Security Officer' (CISO) to coordinate the operational aspects of the organization's information security. Part of this role is in planning investment responses to information security threats against the firms corporate network infrastructure. To this end, we develop and estimate a vector equation system of threats to ten important IP services, using industry standard SANS data on threats to various components of a firm's information system over the period January 2003 to February 2011. Our results reveal strong evidence of contagion between such attacks, with attacks on ssh and Secure Web Server indicating increased attack activity on other ports. Security managers who ignore such contagious inter-relationships may underestimate the underlying risk to their systems' defence of security attributes, such as sensitivity and criticality, and thus delay appropriate information security investments.
Journal of the Operational Research Society, 2016, doi: 10.1057/jors.2016.37. Manuscript.
Ioannidis, C., Pym, D., and Williams, J. (2016) Is Public Co-Ordination of Investment in Information Security Desirable? Journal of Information Security (Special Issue on Cybersecurity Investments, L. Gordon and M. Loeb, editors), 7, 60-80. doi: 10.4236/jis.2016.72005.
Abstract. This paper provides for the presentation, in an integrated manner, of a sequence of results addressing the consequences of the presence of an information steward in an ecosystem under attack and establishes the appropriate defensive investment responses, thus allowing for a cohesive understanding of the nature of the information steward in a variety of attack contexts. We determine the level of investment in information security and attacking intensity when agents react in a non-coordinated manner and compare them to the case of the system's coordinated response undertaken under the guidance of a steward. We show that only in the most well-designed institutional set-up the presence of the well-informed steward provides for an increase of the system's resilience to attacks. In the case in which both the information available to the steward and its policy instruments are curtailed, coordinated policy responses yield no additional benefits to individual agents and in some case they actually compared unfavourably to a tomistic responses. The system's sustainability does improve in the presence of a steward, which deters attackers and reduces the numbers and intensity of attacks. In most cases, the resulting investment expenditure undertaken by the agents in the ecosystem exceeds its Pareto efficient magnitude.
Intuitionistic layered graph logic. Joint work with Simon Docherty.
Abstract. Models of complex systems are widely used in the physical and social sciences, and the concept of layering, typically building upon graph-theoretic structure, is a common feature. We describe an intuitionistic substructural logic that gives an account of layering. As in bunched systems, the logic includes the usual intuitionistic connectives, together with a non-commutative, non-associative conjunction (used to capture layering) and its associated implications. We give soundness and completeness theorems for labelled tableaux and Hilbert-type systems with respect to a Kripke semantics on graphs. To demonstrate the utility of the logic, we show how to represent a range of systems and security examples, illuminating the relationship between services/policies and the infrastructures/architectures to which they are applied.
Proc. IJCAR 2016, N. Olivetti and A. Tiwari (editors), Coimbra, Portugal, June 27-July 2, 2016. LNAI 9706:469-486, 2016. Manuscript.
Discrete Choice, Social Interaction, and Policy in Encryption Technology Adoption [Short Paper]. Joint work with Tristan Caulfield and Christos Ioannidis.
Abstract. We introduce a model for examining the factors that lead to the adoption of new encryption technologies. Building on the work of Brock and Durlauf, the model describes how agents make choices, in the presence of social interaction, between competing technologies given their relative cost, functionality, and usability. We apply the model to examples about the adoption of encryption in communication (email and messaging) and storage technologies (self-encrypting drives) and also consider our model's predictions for the evolution of technology adoption over time.
To appear: Proc. Financial Cryptography and Data Security 2016. LNCS, 2016. Preprint.
Substructural modal logic for optimal resource allocation. Joint work with Gabrielle Anderson.
Abstract. We introduce a substructural modal logic for reasoning about (optimal) resource allocation in models of distributed systems. The underlying logic is a variant of the modal logic of bunched implications, and based on the same resource semantics, which is itself closely related to concurrent separation logic. By considering notions of cost, strategy, and utility, we are able to formulate characterizations of Pareto optimality, best responses, and Nash equilibrium within resource semantics.
Paper 5, Proc. Strategic Reasoning 2015, St. Catharine's College, Oxford, September 21-22, 2015. Strategic Reasoning 2015.
Hennessy-Milner Completeness in Resource-Process Calculus. Joint work with Gabrielle Anderson and James Brotherston.
Abstract We consider the problem of obtaining Hennessy-Milner soundness and completeness --- the coincidence of logical equivalence and bisimilarity --- in the setting of transition systems with synchronous concurrent composition. Starting from a richly expressive modal logic, motivated by resource semantics and distributed systems modelling, including both additive and multiplicative propositional connectives and also additive and multiplicative action modalities, as well as certain first-order quantifiers, we establish sufficient conditions for Hennessy--Milner soundness and completeness to hold. We develop two examples in detail. First, using the propositional part of the logic, we consider a calculus of resources and processes, explaining how the semantics may be refined to give a familiar equational theory. Second, employing a first-order, arithmetic theory, we consider a calculus with utilities that is able to express optimality and equilibria in resource allocation.
Technical report, RN/15/05, University College London, 2015: http://www.cs.ucl.ac.uk/fileadmin/UCL-CS/research/Research_Notes/RN- 15- 05.pdf.
Completeness via canonicity for distributive substructural logics: a coalgebraic perspective. Joint work with Fredrik Dahlqvist.
Abstract. We prove strong completeness of a range of substructural logics with respect to their relational semantics by completeness-via-canonicity. Specifically, we use the topological theory of canonical (in) equations in distributive lattice expansions to show that distributive substructural logics are strongly complete with respect to their relational semantics. By formalizing the problem in the language of coalgebraic logics, we develop a modular theory which covers a wide variety of different logics under a single framework, and lends itself to further extensions.
Proc 15th Int. Conf. on Relational and Algebraic Methods in Computer Science (RAMiCS 2015), LNCS 9348: 119-135, 2015.
Modelling and Simulating Systems Security Policy. Joint work with Tristan Caulfield.
Abstract. Security managers face the challenge of designing security policies that deliver the objectives required by their organizations. We explain how a rigorous modelling framework and methodology---grounded in semantically justified mathematical systems modelling, the economics of decision-making, and simulation---can be used to explore the operational consequences of their design choices and help security managers to make better decisions. The methodology is based on constructing executable system models that illustrate the effects of different policy choices. Models are compositional, allowing complex systems to be expressed as combinations of smaller, complete models. They capture the logical and physical structure of systems, the choices and behaviour of agents within the system, and the security managers' preferences about outcomes. Utility theory is used to describe the extent to which security managers' policies deliver their security objectives. Models are parametrized based on data obtained from observations of real-world systems that correspond closely to the examples described.
In Proc SIMUTools 2015, ACM Digital Library, SIMUtools 2015. doi: 10.4108/eai.24-8-2015.2260765.
The julia package used for creating system models may be obtained from GitHub here.
A Calculus and Logic of Bunched Resources and Processes. Joint work with Gabrielle Anderson.
Abstract. Mathematical modelling and simulation modelling are fundamental tools of engineering, science, and social sciences such as economics, and provide decision-support tools in management. Mathematical models are essentially deployed at all scales, all levels of complexity, and all levels of abstraction. Models are often required to be executable, as a simulation, on a computer. We present some contributions to the process-theoretic and logical foundations of discrete-event modelling with resources and processes. Building on previous work in resource semantics, process calculus, and modal logic, we describe a process calculus with an explicit representation of resources in which processes and resources co-evolve. The calculus is closely connected to a substructural modal logic that may be used as a specification language for properties of models. In contrast to earlier work, we formulate the resource semantics, and its relationship with process calculus, in such a way that we obtain soundness and completeness of bisimulation with respect to logical equivalence for the naturally full range of logical connectives and modalities. We give a range of examples of the use of the process combinators and logical structure to describe system structure and behaviour.
Theoretical Computer Science 614:63-96, 2016: http://www.sciencedirect.com/science/article/pii/S0304397515011214.
Improving Security Policy Decisions with Models. Joint work with Tristan Caulfield.
Abstract. Security managers face the challenge of designing security policies that deliver the objectives required by their organizations. We explain how a rigorous methodology, grounded in mathematical systems modelling and the economics of decision-making, can be used to explore the operational consequences of their design choices and help security managers to make better decisions. The methodology is based on constructing executable system models that illustrate the effects of different policy choices. Models are designed to be composed, allowing complex systems to be expressed as combinations of smaller, complete models. They capture the logical and physical structure of systems, the choices and behavior of agents within the system, and the security managers' preferences about outcomes. Models are parameterized from observations of the real world and the effectiveness of different security policies is explored through simulation. Utility theory is used to describe the extent to which security managers' policies deliver their security objectives.
Preprint. Published version: IEEE Security and Privacy, 13(5), 34-41, September/October 2015.
The julia package used for creating system models may be obtained from GitHub here.
Resilience in Information Stewardship. Joint work with Christos Ioannidis, Julian Williams, and Iffat Gheyas.
Abstract. Information security is concerned with protecting the confidentiality, integrity, and availability of information systems. System managers deploy their resources with the aim of maintaining target levels of these attributes in the presence of reactive threats. Information stewardship is the challenge of maintaining the sustainability and resilience of the security attributes of (complex, interconnected, multi-agent) information ecosystems. In this paper, we present, in the tradition public economics, a model of stewardship which addresses directly the question of resilience. We model attacker-target-steward behaviour in a fully endogenous Nash equilibrium setting. We analyse the occurrence of externalities across targets and assess the steward's ability to internalize these externalities under varying informational assumptions. We apply and simulate this model in the case of a critical national infrastructure example.
In: WEIS 2014, Penn State University, 23-24 June, 2014: paper, slides.
Compositional Security Modelling: Structure, Economics, and Behaviour. Joint work with Tristan Caulfield and Julian Williams.
Abstract. Security managers face the challenge of formulating and implementing policies that deliver their desired system security postures --- for example, their preferred balance of confidentiality, integrity, and availability --- within budget (monetary and otherwise). In this paper, we describe a security modelling methodology, grounded in rigorous mathematical systems modelling and economics, that captures the managers' policies and the behavioural choices of agents operating within the system. Models are executable, so allowing systematic experimental exploration of the system-policy co-design space, and compositional, so managing the complexity of large-scale systems.
Proceedings of the Foundations, Tools, and New Concepts in Trusted Computing track of the 2nd International Conference on Human Aspects of Information Security, Privacy and Trust, HCI International 2014, Heraklion, June 2014. LNCS 8533: 233--245, 2014.
Layered Graph Logic as an Assertion Language for Access Control Policy Models. Joint work with Matthew Collinson and Kevin McDonald.
Abstract. We describe a uniform logical framework, based on a bunched logic that combines classical additives and very weak multiplicatives, for reasoning compositionally about access control policy models. We show how our approach takes account of the underlying system architecture, and so provides a way to identify and reason about how vulnerabilities may arise (and be removed) as a result of the architecture of the system. We consider, using frame rules, how local properties of access control policies are maintained as the system architecture evolves.
Manuscript. Journal of Logic and Computation, 2015. doi: 10.1093/logcom/exv020. First published online: June 12, 2015.
Trust Domains in system models: algebra, logic, utility, and combinators. Joint work with Gabrielle Anderson.
Abstract. Understanding the boundaries of trust is a key aspect of accurately modelling multi-agent systems with heterogeneous motivating factors. Reasoning about these boundaries in highly interconnected, information-rich ecosystems is complex, and dependent upon modelling at the correct level of abstraction. Building on an established mathematical framework, which incorporates both logical and cost-based descriptions of systems, and a formal characterization of trust domains in terms of the above, we develop techniques for the combination and substitution of trust domains.
Manuscript. Journal of Logic and Computation, 2015: doi: 10.1093/logcom/exv030. First published online: June 15, 2015.
Sustainability in Information Stewardship: Time Preferences, Externalities, and Social Co-ordination. Joint work with Christos Ioannidis and Julian Williams.
Abstract. The concept of stewardship in environmental economics is an established tool for environmental and natural resource management and the mitigation of risk from climate change. Similar concepts are well-established in accounting and management. Despite the ubiquity of the concept of stewardship, there is no generally accepted definition. We define the information steward as the agent/institution who enhances the system's resilience and sustainability, by maintaining and extending the life of its nominal operational capacity. Unlike individual agents who are not able to value systemic losses, the steward, whose function is the viability of the system as a whole, values such damages that degrade the system at a higher rate by adopting a lower discount rate. In the presence of deliberate attacks that degrade the information used/kept in the system, individual agents' defensive expenditure is always lower that the expenditure undertaken under instructions from the information steward. The ability of the steward to mobilize the totality of agents reduces the number of attackers, increasing the system's sustainability under a variety of technological considerations. The resulting configuration of defensive expenditure, although higher than the level that individual agents would have chosen based on their own valuation of their expected losses, ensures that the overall probability of successful attacks falls, significantly extending the system's sustainability.
In: WEIS 2013, Georgetown University, Washington DC, 11-12 June, 2103: paper.
Trust Domains: An Algebraic, Logical, and Utility-theoretic Approach. Joint work with Gabrielle Anderson and Matthew Collinson.
Abstract. Complex systems of interacting agents are ubiquitous in the highly interconnected, information-rich ecosystems upon which the world is more-or-less wholly dependent. Within these systems, it is often necessary for an agent, or a group of agents, such as a business, to establish within a given ecosystem a trusted group, or a region of trust. Building on an established mathematical systems modelling framework --- based on process algebra, logic, and stochastic methods --- we give a characterization of such `trust domains' that employs logical assertions of the properties required for trust and utility-theoretic constraints on the cost of establishing compliance with those properties. We develop the essential meta-theory and give a range of examples.
Manuscript available here. Presented in the socio-economic track at TRUST 2013. In: Trust and Trustworthy Computing, Michael Huth, N. Asokan, Srdjan Capkun, Ivan Flechais, Lizzie Coles-Kemp (editors), LNCS 7904:232-249, 2013.
Extended versions of proofs available as University of Aberdeen Computing Science Technical Report TR-ABDN-CS-12-04.
A Proof-theoretic Analysis of the Classical Matrix Method. Joint work with Eike Ritter and Edmund Robinson.
Abstract. The matrix method, due to Bibel and Andrews, is a proof procedure designed for automated theorem-proving. We show that underlying this method is a fully structured combinatorial model of conventional classical proof theory.
Manuscript available here.
J. Logic Computation 24 (1): 283-301, 2014. doi: 10.1093/logcom/exs045. First published online: November 21, 2012 online advance access.
Systematic Decision Making in Security Management: Modelling Password Usage and Support. Joint work with Adam Beautement et al.
Abstract. We demonstrate the use of a systematic decision-making methodology to support an informed choice of a password policy. Our approach uses an executable system model, grounded in empirical data, to compare, using simulations, two different policy options. The problem is framed economically, with the basis of the comparison being a notion of organizational utility. We quantify utility in this case by considering breaches of system security, users' productivity, and investment in support operations. Using our results, we are able to explore trade-offs between these factors and thus determine the optimal policy configuration given the initial conditions.
In QASA 2012 (International Workshop on Quantitative Aspects in Security Assurance). Affiliated workshop with ESORICS. Presented version available here.
Utility-based Decision-making in Distributed Systems Modelling [Extended Abstract]. Joint work with Gabrielle Anderson and Matthew Collinson.
Abstract. We consider a calculus of resources and processes as a basis for modelling decision-making in multi-agent systems. The calculus represents the regulation of agents' choices using utility functions that take account of context. Associated with the calculus is a (Hennessy-Milner-style) context-sensitive modal logic of state. As an application, we show how a notion of `trust domain' can be defined for multi-agent systems.
Preprint available here. In Proc. TARK 2013, Burkhard C. Schipper (editor), Chennai, 2013. Computing Research Repository (CoRR): http://arxiv.org/corr/home. ISBN: 978-0-615-74716-3.
Extended versions of proofs available as University of Aberdeen Computing Science Technical Report TR-ABDN-CS-12-04.
A Substructural Logic for Layered Graphs. Joint work Matthew Collinson and Kevin McDonald.
Abstract. Complex systems, be they natural or synthetic, are ubiquitous. In particular, complex networks of devices and services underpin most of society's operations. By their very nature, such systems are difficult to conceptualize and reason about effectively. The concept of layering is widespread in complex systems, but has not been considered conceptually. Noting that graphs are a key formalism in the description of complex systems, we establish a notion of a layered graph. We provide a logical characterization of this notion of layering using a non-associative, non-commutative substructural, separating logic. We provide soundness and completeness results for a class of algebraic models that includes layered graphs, which give a mathematically substantial semantics to this very weak logic. We explain, via examples, applications in information processing and security.
Pre-publication manuscript here.
J. Logic Computation 24 (4):953-988, 2014. doi: 10.1093/logcom/exu002. First published online: February 18, 2014.
Erratum: Journal of Logic and Computation, 2015. doi: 10.1093/logcom/exv019. First published online: June 9, 2015
A Framework for Modelling Security Architectures in Services Ecosystems. Joint work with Matthew Collinson and Barry Taylor.
Abstract. We develop a compositional framework for modelling security and business architectures based on rigorous underlying mathematical systems modelling technology. We explain the basic architectural model, which strictly separates declarative specification from operational implementation, and show architectures can interact by composition, substitution, and stacking. We illustrate these constructions using a running example based on airport security and an example based on (cloud-based) outsourcing, indicating how our approach can illustrate how security controls can fail or be circumvented in these cases. We explain our motivations from mathematical modelling and security economics, and conclude by indicating how to aim to develop a decision-support technology.
Manuscript available at here. In Proc. ESOCC 2012. LNCS: 7592, 64-79, 2012.
Exploring Information Stewardship with the Cloud Ecosystem Model. Joint work with Adrian Baldwin et al.
Abstract. The emergence of cloud computing has transformed the way in which enterprise IT is delivered and creates new challenges around risk management, security strategy, and control over policies and information. For a particular example, the economies of scale that can be achieved by large cloud service providers are encouraging ecosystems of service providers in which the marketplace (rather than the consuming enterprises or individuals) determines security standards. The problem goes beyond core security concerns, since all cloud stakeholders will be relying on others to steward their information, and so will be concerned with the overall sustainability and resilience of the ecosystem, from both security and business perspectives. To help cloud consumers and other stakeholders explore the impact of the cloud ecosystem on their business decisions, we have developed a system that combines systems modelling, simulation, and 3D visualization techniques. At the heart of this system is a model of the cloud ecosystem, built by combining economic and system modelling approach. The model uses utility theory as the unifying vocabulary for stakeholders to express their decision-making. Simulations of the model representing several years of operations are then performed, with various shocks — such as economic downturns and security attacks — introduced at certain points in time. The visualization component has been built specifically for this model and consists of interactive 3D graphics that can be used in any compatible web browser, so allowing stakeholders to interact with and explore the model and simulation results easily.
To appear, Proc. 2012 International Conference on Modeling, Simulation and Visualization Methods (MSV 2012), 2012 World Congress in Computer Science, Computer Engineering, and Applied Computing. Las Vegas, July 2012. Preprint available here.
A Discipline of Mathematical Systems Modelling. College Publications, 2012. Joint work with Matthew Collinson and Brian Monahan.
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.
Contributor to the ENISA report Economics of Security: Facing the Challenges. Luxembourg: Publications Office of the European Union, 2012. ISBN: 978-92-9204-057-4, doi: 10.2824/23063.
Contagion in Cybersecurity Attacks. Joint work with Adrian Baldwin, Iffat Gheyas, Christos Ioannidis, and Julian Williams.
Abstract. We develop and estimate a vector equation system of threats to ten important IP services, using SANS-reported data over the period January 2003 to February 2011. Our results reveal strong evidence of contagion between such attacks, with attacks on ssh and Secure Web Server indicating increased attack activity on other ports. Security managers who ignore such contagious inter-relationships may underestimate the underlying risk to their systems' defence of security attributes, such as sensitivity and criticality, and thus delay appropriate information security investments.
Proceedings of WEIS 2012, Berlin: paper.
Information Stewardship in the Cloud. Joint work with Simon Shiu. IISP Pulse 7 Winter 2011: 6-8.
Available here.
Enterprise information risk management: Dealing with cloud computing. Joint work with Adrian Baldwin and Simon Shiu. To appear: Privacy and Security for Cloud Computing: Selected Topics, Siani Pearson and George Yee (editors), Springer, Computer Communications and Networks series, 2012.
Abstract. Managing information risk is a complex task that must continually adapt to business and technology changes. We argue that cloud computing presents a more significant step change, and so implies a bigger change for the enterprise risk and security management lifecycle. Specifically, the economies of scale that large providers can achieve are creating an ecosystem of service providers in which the marketplace (rather than consuming enterprises) determines security standards and properties. Moreover, the ability to consume high-level services from different environments is changing the nature of one-size-fits-all security policies.
Manuscript available here.
The TSB-funded Trust Economics project Final Report.
Information Stewardship in Cloud Ecosystems: Towards Models, Economics, and Delivery. Joint work with Adrian Baldwin, Martin Sadler, and Simon Shiu. Preprint.
Proc. 2011 Third IEEE International Conference on Cloud Computing Technology and Science (CloudCom 2011), IEEE Digital Library, 784--791, 2011. doi: 10.1109/CloudCom.2011.121 Copyright IEEE, 2011.
Abstract. We discuss the concept of information stewardship in cloud-based business ecosystems. The constituent concepts of stewardship --- which we believe will be crucial to the successful development of cloud-based business of all kinds --- extend those of security to encompass concepts such as values, ethics, resilience, and sustainability: all familiar from the stewardship of natural resources. Our view is based on rigorous approaches from mathematical systems modelling and economics, and is informed by concepts from natural resource management and information assurance.
Fixed Costs, Investment Rigidities, and Risk Aversion in Information Security: A Utility-theoretic Approach. Joint work with Christos Ioannidis and Julian Williams. Proc. WEIS 2011, George Mason University, Fairfax, Virginia, 14-15 June, 2011: WEIS 2011.
Proc. WEIS 2011, George Mason University, Fairfax, Virginia, 14-15 June, 2011. In Economics of Security and Privacy III, Bruce Schneier (editor), Springer 2012. pp. 171--192.
Abstract. This paper introduces and demonstrates a simple analytically tractable method of mapping utility theory to information security problems and in particular optimal timing for vulnerability management. Our primary focus is on the decision to defer costly deterministic investment, such as the removal of a service or implementation of a security patch, when the costs associated with future security vulnerabilities are uncertain. We outline an investment function with fixed and variable costs that imports a nominal rigidity into the investment decision-making profile. The rigidity introduces a delay in the implementation of security measures, resulting in cyclical investments in information security. We show how such cycles emerge endogenously from the policy-maker's chosen trade-offs between system and security attributes.
Available from the WEIS 2011 site at here.
Information Stewardship: Systems Perspective, Systems Solutions. Slides from my Keynote presentation at Information Security Leaders (2011), Edinburgh, February 2011.
Available here.
The Structure and Dynamics of Systems Security Economics. Joint work with Adam Beautement.
Abstract. Structured systems security economics provides a conceptual framework, inspired by macroeconomic models of trade-offs and mathematical systems models, for analysing the structure of security architectures, their policy constraints, and their interactions with users. In this paper, we explore the dynamics of structured systems security economics by considering the representation and functionality of Actors in the framework. We show how a simple representation of Actors' preferences is sufficient to understand the security dynamics of the system and support utility calculations that inform design and investment decisions. Overall, the framework is intended to facilitate the design and implementation of trustworthy security systems.
Manuscript available here.
Economics of Information Security and Privacy. Co-editor with Tyler Moore and Christos Ioannidis. Springer New York Dordrecht Heidelberg London, 2010. doi: 10.1007/978-1-4419-6967-5.
Papers from WEIS 2009, the Eighth Workshop on the Economics of Information Security, UCL, June 24-25, 2009.
Available from Amazon.
Security Analytics: Bringing Science to Security Management. Joint work with Simon Shiu. IISP Pulse 4 Summer 2010: 12-13.
Available here.
Information Stewardship in the Cloud: A Model-based Approach. Joint work with Martin Sadler, Simon Shiu, and Marco Casassa Mont. To appear, Proc. CloudComp 2010, Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering (LNICST) series, Springer, 2010. Preprint.
Abstract. Managing the information stewardship lifecycle is a challenge. In the context of cloud computing, the stakeholders in cloud ecosystems must also take account of the demands of the information stewardship lifecycles of other participants in the ecosystem. We describe a modelling framework --- incorporating tools from mathematical systems modelling, economics, and policy/user modelling --- suitable for supporting reasoning and decision making in cloud ecosystems, and so provides a basis for developing model-based service level agreements.
Structured Systems Economics for Security Management. Joint work with Adam Beautement. Proc. WEIS 2010, Harvard University. Paper. Presentation.
Abstract. We develop an ontological account of information security architectures that is inspired by economic models of trade-offs between confidentiality, integrity, and availability. Our approach clarifies the nature of the trade-offs by making a clear distinction between declarative and operational concepts in security. We integrate this approach with a semantically justified mathematical systems modelling technology, thus providing a basis for a systematic methodology to support operational decision-making in information security investments and trade-offs.
Information Stewardship in Cloud Computing. Joint work with Martin Sadler. International Journal of Service Science, Management, Engineering, and Technology 1(1), 50-67, 2010. Free sample copy, including this article.
Semantics for Structured Systems Modelling and Simulation. Joint work with Matthew Collinson and Brian Monahan. Proc. Simutools 2010, ACM Digital Library and EU Digital Library. ISBN: 978-963-9799-87-5. Preprint.
Abstract. Simulation modelling is an important tool for exploring and reasoning about the dynamics and properties of complex systems, and many supporting languages are available. Commonly occurring features of these languages are constructs that capture concepts such as process, resource, and location. We describe a mathematical framework that supports a modelling idiom based on these core concepts, and which also adopts stochastic methods for representing the environments within which systems exist. We explain how this framework can be used to give a formal semantics to a simulation modelling language, Core Gnosis, that includes basic constructs for process, resource, and location. We include a brief discussion of a system of logic for reasoning about our models that is compositional with respect to the structure of models. We believe that our mathematical analysis of systems in terms of process, resource, location, and stochastic environment, together with a language that captures these concepts quite directly, leads to an efficient and robust modelling framework within which natural mathematical reasoning about systems is captured in the associated tools.
Decision Support for Systems Security Investment. Joint work with Yolanta Beresnevichiene and Simon Shiu. Proc. Business-driven IT Management (BDIM) 2010. IEEE Xplore, 2010. Preprint
Abstract. Information security managers with fixed budgets must invest in security measures to mitigate increasingly severe threats whilst maintaining the alignment of their systems with their organization's business objectives. The state of the art lacks a systematic methodology to support security investment decision-making. We describe a methodology that integrates methods from multi-attribute utility evaluation and mathematical systems modelling. We illustrate our approach using a case study of a large organization divesting itself of its IT support services, delivering useful results to the organization's security managers. Specifically, by integrating a mathematical model of system behaviour with an account of the utility of available security investment strategies, the case study has enabled them to understand better the trade-offs between the security performance and the operational consequences of their choices.
Economics of Identity and Access Management: Providing Decision Support for Investments. Joint work with Marco Casassa Mont, Yolanta Beresnevichiene, and Simon Shiu. Proc. Business-driven IT Management (BDIM) 2010. IEEE Xplore, 2010. Preprint
Abstract. Identity and Access Management (IAM) is a key enabler of enterprise businesses: it supports automation, security enforcement and compliance. However, most enterprises struggle with their Identity and Access Management strategy. Discussions on IAM primarily focus at the IT operational level, rather than targeting strategic decision makers' issues, at the business level. Organisations are experiencing an increasing number of internal and external threats and risks: there is scarcity of resources and budget to address them all. Decision makers (e.g. CIOs, CISOs) need to prioritise their choices and motivate their requests for investments. This applies for investments in IAM vs. other possible security or business investments that could be made by the organisation. In this context, a range of possible IAM investment options has an effect on multiple strategic outcomes of interest, such as assurance, agility, security, compliance, productivity and empowerment. We have developed a repeatable approach and methodology to help organisations work through this complex problem space and determine an appropriate strategy, by providing them with decision support capabilities. The proposed approach, validated in collaboration with Security & IAM experts, couples economic modeling, enabling decision makers to explore their preferences between the different outcomes, with system modeling & simulations to predict the consequences (likely outcomes) associated with different investment choices and map them against decision makers' preferences to identify the most suitable options. We illustrate how this methodology has been applied in an IAM case study, in a business-driven context with core enterprise services. This work is in progress. We discuss current results and next steps.
Information Security Trade-offs and Optimal Patching Policies. Joint work with Christos Ioannidis and Julian Williams. European Journal of Operational Research, 216(2):434-444, 16 January 2012. doi:10.1016/j.ejor.2011.05.050. Preprint.
Abstract.We develop and simulate a model of the deployment of patches --- which incurs cost --- in the presence of trade-offs between confidentiality and availability. The patching of vulnerabilities is divided into regular and irregular events, for both networks and clients. The computation of the optimal patching policy requires knowledge of the joint processes of arrivals and intensities, system architecture, and the type of organization. We have found that different types of organizations, as characterized by the managers' preferences, exhibit distinct off-cycle patching profiles that are relatively cost-sensitive, and that the frequency of irregular patching depends crucially on the aspect of the system --- e.g., network or clients --- addressed.
Investments and Trade-offs in the Economics of Information Security. Joint work with Christos Ioannidis and Julian Williams. Proc. Financial Cryptography and Data Security 2009, LNCS 5628: 148-162, Springer, 2009. Preprint.
Abstract. We develop and simulate a dynamic model of investment in information security. The model is based on the recognition that both IT managers and users appreciate the trade-off between the fundamental characteristics of information security, namely confidentiality and availability. The model's parameters can be clustered in a manner that allows us to categorize and compare the responses to shocks of various types of organizations. We derive the system's stability conditions and find that they admit a wide choice of parameters. We examine the system's responses to the same shock in confidentiality under different parameter constellations that correspond to various types of organizations. Our analysis illustrates that the response to investments in information security will be uniform in neither size nor time evolution.
My Keynote Presentation at the recent ESRC Public Policy Seminar on the Economics of Information Security is summarized in the ESRC Report.
A Logical and Computational Theory of Located Resource. Joint work with Matthew Collinson and Brian Monahan. Journal of Logic and Computation19(b):1207-1244, 2009. Advance Access published on 22 July, 2009. doi:10.1093/logcom/exp021. Preprint. Also available as an HP Labs Technical Report: HPL-2008-74R1.
Abstract. Experience of practical systems modelling suggests that the key conceptual components of a model of a system are processes, resources, locations, and environment. In recent work, we have given a process-theoretic account of this view in which resources as well as processes are first-class citizens. This process calculus, SCRP, captures the structural aspects of the semantics of the Demos2k modelling tool. Demos2k represents environment stochastically using a wide range of probability distributions and queue-like data structures. Associated with SCRP is a (bunched) modal logic, MBI, which combines the usual additive connectives of Hennessy-Milner logic with their multiplicative counterparts. In this paper, we complete our conceptual framework by adding to SCRP and MBI an account of a notion of location that is simple yet sufficiently expressive to capture naturally a wide range of forms of location, both spatial and logical. We also provide a sketch of an extension of the Demos2k tool to incorporate this notion of location.
Modelling the Human and Technological Costs and Benefits of USB Memory Stick Security. Joint work with Adam Beautement et al. Available from Proc. WEIS 2008. In Managing Information Risk and the Economics of Security. M. Eric Johnson (editor), Springer, 2009: 141-163. Preprint.
Abstract. Organizations deploy systems technologies in order to support their operations and achieve their business objectives. In so doing, they encounter tensions between the confidentiality, integrity, and availability of information, and must make investments in information security measures to address these concerns. We discuss how a macroeconomics-inspired model, analogous to models of interest rate policy used by central banks, can be used to understand trade-offs between investments against threats to confidentiality and availability. We investigate how such a model might be formulated by constructing a process model, based on empirically obtained data, of the use of USB memory sticks by employees of a financial management company.
Some recent HP Labs Technical Reports on topics related to services sciences, systems modelling, mathematical logic, and other topics. Some of these papers have been published elsewhere (conferences, journals, etc.).
An Update to Located Demos2k. Joint work with Matthew Collinson and Brian Monahan. Available as an HP Labs Technical Report: HPL-2008-205.
Abstract. We give here a short update concerning Located Demos2k briefly describing the ability to forget and recall resource links, as reported in an earlier Technical Report. We also briefly mention our (purely applicative) implementation in OCaml of a simulator for Located Demos2k. Two appendices contain a substantial example of Located Demos2k, presented in OCaml terms, and the execution trace produced by the implementation.
Located Demos2k: A Tool for Executing Processes Relative to Distributed Resources. Joint work with Matthew Collinson and Brian Monahan. Available as an HP Labs Technical Report: HPL-2008-76.
Abstract. We describe the background to, and the current state of the development of, Located Demos2k, an executable modelling language which reconstructs the Demos2k language starting from an explicit model of location. The version of Located Demos2k described herein is the first useful stage in its development, and provides convenient a point of departure of discussing its further development.
Algebra and Logic for Access Control. Joint work with Matthew Collinson. Formal Aspects of Computing22(2), 83-104, 2010. Erratum: Formal Aspects of Computing22(3-4), 483-484, 2010. Available as an HP Labs Technical Report (with erratum incorporated): HPL-2008-75R1. The original publication is available at http://www.springerlink.com.
Abstract. The access control problem in computer security is fundamentally concerned with the ability of system entitites to see, make use of, or alter various system resources. As such, many access control situations are essentially problems of concurrency. We give an account of fundamental situations in access-control in distributed systems using a resource-based process calculus and a hybrid of Hennessy-Milner and resource logic. This yields a consistent account of operational behaviour and logical reasoning for access control, that includes an analysis of co-signing, roles and chains-of-trust.
Bunched Polymorphism. Joint work with Matthew Collinson and Edmund Robinson. Mathematical Structures in Computer Science 18(6), 1091-1132, 2008. doi: 10.1017/S0960129508007159. Preprint.
Abstract. We describe a polymorphic, typed lambda calculus with substructural features. This calculus extends the first-order substructural lambda calculus alphalambda associated with bunched logic. A particular novelty of our new calculus is the substructural treatment of second-order variables. This is accomplished through the use of bunches of type variables in typing contexts. Both additive and multiplicative forms of polymorphic abstraction are then supported. The calculus has sensible proof-theoretic properties and a straightforward categorical semantics using indexed categories. We produce a model for additive polymorphism with first-order bunching based on partial equivalence relations. We consider additive and multiplicative existential quantifiers separately from the universal quantifiers.
Algebra and Logic for Resource-based Systems Modelling. Joint work with Matthew Collinson. Mathematical Structures in Computer Science 19:959-1027, 2009. doi:10.1017/S0960129509990077. Preprint.
Abstract. Mathematical modelling is one of the fundamental tools of science and engineering. Very often, models are required to be executable, as a simulation, on a computer. In this paper, we present some contributions to the process-theoretic and logical foundations of discrete-event modelling with resources and processes. We present a process calculus with an explicit representation of resources in which processes and resources co-evolve. The calculus is closely connected to a logic that may be used as a specification language for properties of models. The logic is strong enough to allow requirements that a system have certain structure; for example, that it is a parallel composite of subsystems. This work consolidates, extends, and improves upon aspects of the earlier works. An extended example, consisting of a semantics for a simple parallel programming language, indicates a connection with separating logics for concurrency.
Errata
A Games Model of Bunched Implications. Proc. CSL '07, LNCS 4646: 573-588. Joint work with Guy McCusker.
Abstract. A game semantics of the implicational fragment of the (-*,->)-fragment of the logic of bunched implications, BI, is presented. To date, categorical models of BI have been restricted to two kinds: functor category models; and the category Cat itself. The game model is not of this kind. Rather, it is based on Hyland-Ong-Nickau-style games and embodies a careful analysis of the notions of resource sharing and separation inherent in BI. he key to distinguishing between the additive and multiplicative connectives of BI is a semantic notion of separation. The main result of the paper is that the model is fully complete: every finite, total strategy in the model is the denotation of a term of the alphalambda-calculus, the term language for the fragment of BI under consideration.
Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic. Joint work with Chris Tofts.
Here is a preprint of ENTCS 172, 545-587, 2007. ENTCS 172 is entitled 'Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin'.
Abstract. We describe a programme of research in resource semantics, concurrency theory, bunched logic, and stochastic processes, as applied to mathematical systems modelling. Motivated by a desire for structurally and semantically rigorous discrete event modelling tools, applicable to enterprise-scale as well as component-scale systems, we introduce a new approach to compositional reasoning based on a development of SCCS with an explicit model of resource. Our calculus models the co-evolution of resources and processes with synchronization constrained by the availability of resources. We provide a simple denotational semantics as a parametrization of Abramsky's synchronization trees semantics for SCCS. We also provide a logical characterization, analogous to Hennessy-Milner logic's characterization of bisimulation in CCS, of bisimulation between resource processes which is compositional in the concurrent and local structure of systems. We discuss applications to ideas such as location and access control.
Formal Aspects of Computing, 18(4): 495-517, 2006.
Preprint here. The original publication is available at http://www.springerlink.com.
Abstract. Recent advances in logics for reasoning about resources provide a new approach to compositional reasoning in interacting systems. We present a calculus of resources and processes, based on a development of Milner's synchronous calculus of communication systems, SCCS, that uses an explicit model of resource. Our calculus models the co-evolution of resources and processes with synchronization constrained by the availability of resources. We provide a logical characterization, analogous to Hennessy-Milner logic's characterization of bisimulation in CCS, of bisimulation between resource processes which is compositional in the concurrent and local structure of systems.
Abstract. There are a number of applied lambda-calculi in which terms and types are annotated with parameters denoting either locations or locations in machine memory. Such calculi have been designed with safe memory-management operations in mind.
It is difficult to construct directly denotational models for existing calculi of this kind. We approach the problem differently, by starting from a class of mathematical models that describe some of the essential semantic properties intended in these calculi. In particular, disjointness conditions between regions (or locations) are implicit in many of the memory-management operations.
Bunched polymorphism provides natural type-theoretic mechanisms for capturing the disjointness conditions in such models. We illustrate this by adding regions to the basic disjointness model of $\alphalambda$, the lambda-calculus associated to the logic of bunched implications. We show how both additive and multiplicative polymorphic quantifiers arise naturally in our models. A locations model is a special case. In order to relate this enterprise back to previous work on memory-management, we provide an example in which the model is refined and used to provide a denotational semantics for a language with explicit allocation and disposal of regions.
In: Proc. MFPS 2006, S. Brookes and M. Mislove (editors), Electronic Notes in Theoretical Computer Science, 2006.
Abstract. We describe a polymorphic extension of the substructural lambda calculus alphalambda associated with the logic of bunched implications. This extension is particularly novel in that both variables and type variables are treated substructurally, being maintained through a system of zoned, bunched contexts. Polymorphic universal quantifiers are introduced in both additive and multiplicative forms, and then metatheoretic properties, including subject-reduction and normalization, are established. A sound interpretation in a class of indexed category models is defined and the construction of a generic model is outlined, yielding completeness. A concrete realization of the categorical models is given using pairs of partial equivalence relations on the natural numbers. Polymorphic existential quantifiers are presented, together with some metatheory. Finally, potential applications to closures and memory-management are discussed.
Proc. CSL 05, Lecture Notes in Computer Science 3634, 36-50, 2005.
Abstract. Theorem proving, or algorithmic proof-search, is an essential enabling technology throughout the computational sciences. We explain the mathematical basis of proof-search as the combination of reductive logic together with a control régime. Then we present a games semantics for reductive logic and show how it may be used to model two important examples of control, namely backtracking and uniform proof.
Proc. ETAPS 05 Workshop on Games for Logic and Programming Languages, Edinburgh, April, 2005.
Oxford Logic Guides, 45, Oxford University Press, 2004.
Errata and Remarks.
Mathematical Structures in Computer Science (2007) 17, 957-1027.
Abstract. It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarized briefly herein, we have provided a class of models called classical categories which is sound and complete and avoids this collapse by interpreting cut-reduction by a poset-enrichment. Examples of classical categories include boolean lattices and the category of sets and relations, where both conjunction and disjunction are modelled by the set-theoretic product.
In this article, which is self-contained, we present an improved axiomatization of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models called Dummett categories. Examples include, besides the classical categories above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Dummett categories are MIX, and that the partial order can be derived from hom-semilattices which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic, by applying it to obtain a classical category from a Dummett category.
Along the way, we gain detailed insights into the changes that proofs undergo during cut-elimination in the presence of weakening and contraction.
Abstract. It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. We introduce sound and complete models that avoid this collapse by interpreting cut-reduction by a partial order between morphisms. We provide concrete examples of such models by applying the geometry-of-interaction construction to quantaloids with finite biproducts, and show hoe these models illuminate cut-reduction in the presence of weakening and contraction. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination.
Abstract. The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource rich enough, for example, to form the logical basis for `pointer logic' and `separation logic' semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI's tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, bottom, the challenge consists in dealing with BI's Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. Then, from these results, we can define a new resource semantics of BI, based on partially defined monoids, and prove that this semantics is complete. Such a semantics, based on partiality, is closely related to the semantics of BI's (intuitionistic) pointer and separation logics. Returning to the tableaux calculus, we propose a new version with liberalized rules for which the countermodels are closely related to the topological Kripke semantics of BI. As consequences of the relationships between semantics of BI and resource tableaux, we prove two strong new results for propositional BI: its decidability and the finite model property with respect to topological semantics.
Abstract. Since its earliest presentations, mathematical logic has been formulated as a formalization of deductive reasoning: given a collection of hypotheses, a conclusion is derived. However, the advent of computational logic has emphasized the significance of reductive reasoning: given a putative conclusion, what are sufficient premisses ? Whilst deductive systems typically have a well-developed semantics of proofs, reductive systems are typically well-understood only operationally. Typically, a deductive system can be read as a corresponding reductive system. The process of calculating a proof of a given putative conclusion, for which non-deterministic choices between premisses must be resolved, is called proof-search and is an essential enabling technology throughout the computational sciences. We suggest that the reductive view of logic is (at least) as fundamental as the deductive view and discuss some of the problems which must be addressed in order to provide a semantics of proof-searches of comparable value to the corresponding semantics of proofs. Just as the semantics of proofs is intimately related to the model theory of the underlying logic, so too should be the semantics of reductions and of proof-search. We discuss how to solve the problem of providing a semantics for proof-searches in intuitionistic logic which adequately models both not only the logical but also, via an embedding of intuitionistic reductive logic into classical reductive logic, the operational aspects, i.e., control of proof-search, of the reductive system.
Abstract. It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. Starting from a convenient formulation of the well-known categorical semantics of linear classical sequent proofs, we give models of weakening and contraction that do not collapse. Cut-reduction is interpreted by a partial order between morphisms. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination. We show soundness and completeness via initial models built from proof nets, and describe models built from sets and relations.
Errata and remarks applicable to this paper are available here.
Errata and remarks applicable to this paper are available here.
Theoretical Computer Science 232 (2000) 5-53. Erratum: p. 32, side-condition of Resolution rule, replace index i by k and insert `i ≤ k ≤ n,' after the comma. Erratum also applies to the corresponding occurrence of the Resolution rule in the preprint (above, p. 26).
Erratum: In Proposition 4, `DCC' should be `bicartesian DCC'.