Information Stewardship in Cloud Computing. Joint work with Martin Sadler. To appear: International Journal of Service Science, Management, Engineering, and Technology 1(1), 2009.
Semantics for Structured Systems Modelling and Simulation. Joint work with Matthew Collinson and Brian Monahan. To appear, Proc. Simutools 2010, ACM Digital Library; EU Digital Library. 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. Manuscript.
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.
Information Security Trade-offs and Optimal Patching Policies. Joint work with Christos Ioannidis and Julian Williams. Manuscript.
Abstract. We develop and simulate a model of the trade-off between confidentiality and availability in information security in which deploying software patches is costly. We decompose the patching cycle into regular and irregular events, for both networks and clients. Patches are assumed to be defined by a Poisson arrivals process with log-normal intensities. The computation of the optimal patching policy requires knowledge of the joint processes of arrivals and intensities. System architecture and the preferences of IT managers are important inputs to the implementation of the policy. Within a framework that permits a specification of organizational preferences and threat environments, we show that patching cycles will differ between networks and clients. From our simulations, we conclude that with costly patching, large networks are relatively more reluctant to undertake irregular patching.
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. To appear, Journal of Logic and Computation, 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. To appear, Formal Aspects of Computing, 2009. Available as an HP Labs Technical Report: HPL-2008-75R1.
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.
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.
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.
Last updated 31 March, 2005.
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.
Last updated 7 March, 2005.
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''.