Report on The Computer Security Foundations Workshop VI James W. Gray, III Department of Computer Science Hong Kong University of Science and Technology Clear Water Bay, Kowloon, HONG KONG The Computer Security Foundations Workshop VI was held during June 15--17, 1993 in Franconia, New Hampshire. This is an annual workshop with the purpose of ``bring[ing] together researchers to explore fundamental issues in computer security'' [13]. Every year since its inception, the workshop has been limited to forty participants, the majority of whom present papers or speak on panels. The setting is informal with plenty of time for technical discussion. This year, the program chair was Catherine Meadows. The program included sessions on covert channel analysis, information flow, integrity and aggregation, access control, and crypto protocol analysis. Also included were an invited talk by Gus Simmons, two panel discussions, and a report on the Cambridge crypto protocols workshop held earlier this year. The proceedings of the workshop are available from: IEEE Computer Society Press 10662 Los Vaqueros Circle PO Box 3014 Los Alamitos, CA 90720-1264 The first morning of the workshop---Tuesday morning---started off with the session on covert channel analysis. (For a description of covert channels, see [8] or [9].) This session consisted of two papers. The first paper, ``On Analyzing the Bus-Contention Channel Under Fuzzy Time'' by the present author, analyzes the bus-contention channel---a covert channel that can be exploited at a rate exceeding 1000 bits per second---under the fuzzy time countermeasure, which was developed at DEC. The analysis provides the best known upper bound on the capacity of the bus-contention channel under fuzzy time (viz, 22 bits per second) and also provides a tradeoff between clock accuracy and covert channel capacity. The second paper, ``The Concurrency Control and Recovery Problem for Multilevel Update Transactions in MLS Systems'' by Amit G. Mathur and Thomas F. Keefe, addresses the problem of providing both security and correctness in a multilevel secure database management system. In particular, the authors show that no scheduler can ensure atomicity of multilevel update transactions in the presence of transaction aborts and at the same time be secure. The authors go on to describe and compare two possible approaches to this dilemma, both of which contain covert channels. The authors then analyze the two covert channels and offer their analysis as a basis for comparison of the two approaches. The second session of Tuesday morning was on information flow. The first paper was ``Modeling Restrictive Processes that Involve Blocking Requests'' by David Rosenthal. In this paper, the author considers the problem of proving restrictiveness (see [10] for the definition of restrictiveness) of the composition of a set of client processes and server processes, where the clients block on their requests to the servers. He defines two properties, client restrictiveness and server restrictiveness and proves that if all of the clients satisfy client restrictiveness and all of the servers satisfy server restrictiveness, then the composition (when the processes are hooked up in an appropriate way) satisfies restrictiveness. The next paper was ``Information Flow Control in a Parallel Language Framework'' by Jean-Pierre Banatre and Ciaran Bryce. In this paper, the authors develop a logic for reasoning about information flow between program variables in programs written in Hoare's Communicating Sequential Processes (CSP) (viz, Hoare's original version of CSP [7]). The authors also give an operational ``flow semantics'' for the language, which they intend, in later work, to use to prove the soundness and completeness of their logic. A parallel language with message passing, and in particular CSP, allows information to flow in various indirect and subtle ways. This paper brings these subtle flows to light and provides an interesting approach to reasoning about them. The final paper in the information flow session was ``A Logical Formalization of Secrecy'' by Frederic Cuppens. In this paper, Cuppens extends the work begun in [1]. He argues that a previous definition, causality, is a pessimistic definition of security in that it may rule out some systems that are secure, but every system that satisfies it is covert channel free. He also gives a new definition, non-disclosure, and argues that it is an optimistic definition of security in that it does not rule out any covert-channel-free systems, but some systems that satisfy it may have insecure refinements or noisy covert channels. The paper also describes how the two definitions could be used together. Tuesday afternoon started off with the session on Integrity and Aggregation, the first paper of which was ``A Lattice of Information'' by Jaisook Landauer and Timothy Redmond. This paper pursues the idea of defining information (about the state of a given system) as an equivalance relation on the state of the system. Knowing the information represented by a given equivalence relation can be intuitively regarded as knowing which equivalance class the system is in. This idea has been explored since as early as 1986 [14]. The present paper takes the idea further by giving an ordering on the set of all equivalence relations that yields a complete lattice. The paper then shows the relationship between this lattice and some issues in multilevel security, including the Unwinding Theorem [6] and certain aggregation problems (see e.g., [5] for a discussion of aggregation problems). The second paper of the Integrity and Aggregation session was ``Automated Support for External Consistency'' by James G. Williams and Leonard J. LaPadula. In this paper, the authors address the difficult problem of ensuring that a given system's outputs are consistent with the external environment. For example, if an automated teller machine outputs the statement that a certain account contains $10, then that account should actually contain $10. They call such requirements external-consistency requirements. Clearly, there must be some informality in any proof that a system satisfies an external-consistency requirement. However, the authors make some progress by focusing on the decomposition of external-consistency requirements into system requirements and user responsibilities. For example, a system might satisfy the above external-consistency requirement, given that all account transactions made via human tellers are properly input to the system (i.e., given that the user responsibilities are satisfied). The first day of the workshop concluded with a panel organized by Mary Ellen Zurko called ``What are the Foundations of Computer Security?''. Panel participants were invited to give their views on the progress that has been made since the first Computer Security Foundations Workshop in 1988 and on what remains to be done. The panel consisted of John McLean, Jonathan K. Millen, Robert Morris, and Marv Shaefer. Their position statements appear in the workshop proceedings [12]. The first session on Wednesday was on access control, the first paper of which was ``A Petri Net Representation of the Take-Grant Model'' by Marc Dacier. This paper gives a Petri net representation of the Take-Grant model [2]. Then the paper gives a linear time algorithm (using the Petri net representation) for finding all rights that a given subject can obtain with a given set of conspirators. The next paper in this session was ``On Testing for Absence of Rights in Access Control Models'' by Ravi S. Sandhu and Srinivas Ganta. In this paper, the authors show that augmenting the Typed Access Matrix (TAM) model with the ability of subjects to test for the absence (as well as the presence) of rights does not add any expressive power to the model. They do however argue that augmenting the model in this way is useful in practice. The next session on Wednesday morning started off with a report on the Cambridge Cypto Protocols Workshop, by Mark Lomas, in which he summarized the presentations and discussions of that workshop. The report does not appear in the proceedings of the present workshop. Following Mark Lomas' report, Gus Simmons gave an invited talk on ``The Mathematics of Trust in Security Protocols''. A paper accompanying the talk ``An Introduction to the Mathematics of Trust in Security Protocols'' appears in the proceedings [12]. In the paper, Simmons describes a lattice of ``concurrence schemes'', where a ``concurrence'' is a set of users that are required to act jointly to exercise some function (as in, e.g., the separation of duty requirements of [4]). This lattice has been explored previously by McLean in [11], but Simmons describes some new applications of the lattice including the analysis of the effects of trusts held by cryptographic protocol participants. The first session on Wednesday afternoon was on crypto protocol analysis and consisted of three papers. The first paper was Li Gong's ``Variations on the Themes of Message Freshness and Replay''. This paper informally surveys the various mechanisms that are used to validate message freshness (i.e., to determine whether or not a given message was recently generated) and the various forms of replay attacks (i.e., attempts to subvert the protocol by replaying old messages). Gong also argues that due to the wide variety of such mechanisms and attacks, it would be difficult to develop a single formalism that could be used to reason about all of them. The next paper was ``Abstract Machines for Communication Security'' by Pierre Bieber, Nora Boulahia-Cuppens, Thomas Lehmann, and Erich van Wickeren. In this paper, the authors make use of a existing formal language, B, and associated automated tools to specify and reason about cryptographic protocols. The main novelty of the paper is the modular style in which they develop their specifications and proofs. For example, there is one module that describes the way messages are passed between subjects in the system; this includes actions for the legitimate participants as well as actions that penetrators can perform in an attempt to subvert the system. Another module describes the properties of the cryptosystem being used. Still another module describes the cryptographic algorithm under consideration. The authors claim that structuring the specification in this way allows them to reuse specifications and proofs in the verification of additional protocols. The last paper in this session was ``Towards Formal Analysis of Security Protocols'' by Wenbo Mao and Colin Boyd. This paper addresses two shortcomings of the BAN approach (see [3]) to authentication protocol analysis: (1) the authors propose a method for formalizing much of the ``idealization'' process (wherein an informal statement of the protocol is transformed into a formal one); and (2) the authors provide inference rules for reasoning about the ``confidentiality'' of cryptographic keys. This latter concern is crucial since a compromised key (i.e., one that is known to a penetrator) is no longer usable for authentication purposes. The final technical event of the workshop was a panel organized by Paul Syverson on ``Cryptographic Protocol Models and Requirements''. Panel participants were invited to give their views on questions such as the following. How are cryptographic protocol requirements dependent on the model of computation? Should we attempt to develop formal languages to reason about requirements? And what kinds of models and requirements should we focus on? The panel consisted of Whitfield Diffie, Catherine Meadows, Michael Merritt, Gus Simmons, and Einar Snekkenes. Their position statements do not appear in the workshop proceedings. The workshop closed with a business meeting on Thursday morning at which plans for next year's workshop were discussed. For next year, the general chair will be Ravi Sandhu and the program chair will be Li Gong. For further information about next year's workshop, contact Ravi Sandhu (email preferred): ISSE Dept., George Mason U, Fairfax, VA 22033 voice: 703-993-1659, fax: 703-993-1638 email: sandhu@isse.gmu.edu or sandhu@sitevax.gmu.edu References [1] P. Bieber and F. Cuppens. A logical view of secure dependencies. Journal of Computer Security, 1(1):99--129, 1992. [2] M. Bishop and L. Snyder. The transfer of information and authority in a protection system. In Proceedings of the 7th ACM Symposium on Operating System Principles, pages 45--54, Pacific Grove, CA, 1979. [3] Michael Burrows, Martin Abadi, and Roger Needham. A logic of authentication. ACM Transactions on Computer Systems, 8(1):18--36, February 1990. [4] David D. Clark and David R. Wilson. A comparison of commercial and military computer security policies. In Proceedings of the 1987 IEEE Symposium on Security and Privacy, pages 184--194, Oakland, CA, April 1987. IEEE Computer Society Press. [5] Dorothy E. Denning, Selim G. Akl, Matthew Morgenstern, Peter G. Neumann, Roger R. Schell, and Mark Heckman. Views for multilevel database security. Proc. 1986 IEEE Symposium on Security and Privacy, pages 156--172, April 1986. [6] Joseph A. Goguen and Jose Meseguer. Unwinding and inference control. In Proceedings of the 1984 IEEE Computer Society Symposium on Security and Privacy}, Oakland, CA, 1984. [7] C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666--676, August 1978. [8] Richard A. Kemmerer. Shared resource matrix methodology: An approach to identifying storage and timing channels. ACM Transactions on Computer Systems, 1(3):256--277, August 1983. [9] Butler W. Lampson. A note on the confinement problem. Communications of the ACM, 16(10), October 1973. [10] Daryl McCullough. A hookup theorem for multilevel security. IEEE Transactions on Software Engineering}, 16(6):563--568, June 1990. [11] John McLean. The algebra of security. In Proceedings of the 1988 IEEE Symposium on Security and Privacy, Oakland, CA, May 1988. IEEE Computer Society Press. [12] Proceedings of the Computer Security Foundations Workshop VI, Franconia, NH, June 1993. IEEE Computer Society Press. [13] Ravi Sandhu. Preface. In Proceedings of the Computer Security Foundations Workshop VI, page v, June 1993. Available from the IEEE Computer Society Press. [14] David Sutherland. A model of information. In Proceeding of the 9th National Computer Security Conference, Baltimore, MD, September 1986. Note: conversion to text was done by Li Gong from LaTeX source supplied by Jim Gray.