GerardAllwein
NavalResearchLaboratory,
USA
DISTRIBUTED LOGICS
The term "distributed logic" derives from the subtitle of a book by Jon Barwise and Jerry Seligman, Information Flow, the Logic of Distributed Systems. Modularity is the central organizing principle underlying distributed logics, manifested structurally as the composition of a number of component or "local" logics.
Engineering design practices rely on modularity to control complexity when creating both hardware and software artifacts. Furthermore, such practices require additional effort beyond building functionally correct artifacts for providing security. However, it is not enough to merely claim one has provided security; one must prove such claims. Most logics today are monolithic and assume they work on the entire problem at hand. Thus, there is a conceptual disconnecting between most logics and a rather large part of engineering systems which ought to be natural field for the application of modern logic.
It might sound strange to bring this point of view to a Logic and Philosophy conference, but because we care about logic and its growth and development, we as logicians must take care to ensure that it will be recognized as valuable within relevant domains of discourse. We cannot rely on engineers to find the bits and bytes of our formal systems and discover how to apply them in their work. They are not logicians, and, hence, they are unlikely to negotiate a technical field as broad and diverse as modern logic without assistance.
The major open questions in security today are the same as they have been for years. First and foremost they are philosophical in nature: what is security, and what are its terms, principles, and methods? A more technical open question is how a formal security argument can be constructed that follows the same modular philosophy used by engineers to handle functional complexity. Can we stitch together a formal security argument over several components and very non-trivial interconnection schemes?
We will briefly review some of the features of channel theory - Barwise and Seligman's colloquial term for their model theoretic based logic. Many arguments in security are arguments about information flow and, hence, channel theory should be a natural fit. We show that channel theory can be used to argue for correct operation of a particular computer circuit, a bus master.
One can go further along the route of distribution in the form of component based logics with no centralizing notion as a channel. In a recent paper, we introduced simulation logic. This logic is the result of wanting to generalize an earlier logic, partially ordered modalities. The core of the latter was that we should be able to use a partial order of Kripke relations to partially order modalities they help to interpret. The generalization comes from taking the partial order and promoting it into a category. The modalities then map formulas in one logic to formulas in logic.
Dropping the simulation condition and abstracting a bit, logic is specified by something similar to categorical sketch. At each node, choose logic. For each arrow, choose a kind of relation, or what the same is effectively, choose the properties of modalities that go between the logics. Any interpretation turns this into a distributed logic, one that is apropos for many classes of engineered systems (we now have the modularization we sought) and we have the logical apparatus to argue for security of a particular engineered system because we choose the sketch structure to mirror the structure of the engineered system.