Center for High Assurance Computing Systems (CHACS) Publications

1992

Replicated architecture has been proposed as a way to obtain acceptable performance in a multilevel secure database system. This architecture contains a separate database for each security level such that each contains replicated data from lower security classes. The consistency of the values of replicated data items must be maintained without unnecessarily interfering with concurrency of database operations. This paper provides a protocol to do this that is secure, since it is free of covert channels, and also ensures one-copy serializability of executing transactions. The protocol can be implemented with untrusted processes for both concurrency and recovery.

A user of a database management system has an intuitive idea of a transaction as a sequence of database commands that he or she submits. The user expects this sequence of commands to be executed in the order of submission, without interference from other database commands submitted by other users. Techniques for doing this while concurrently supporting multiple database users are well known for conventional (i.e., not multilevel) database systems. Most of the transaction management theory for multilevel secure database systems has been developed for transactions that act within a single security class. In this paper, we look at transactions that act across security classes, that is, the transaction is a multilevel sequence of database commands, which more closely resemble user expectations. We then give an algorithm for controlling concurrent execution of these transactions on a particular multilevel secure database architecture.

The Navy has designated the Naval Research Laboratory (NRL) as its Center for Computer Security Research and Evaluation. NRL is actively developing a Navy capability to certify trusted systems. This paper describes the NRL effort to understand assurance, certification, and trusted system certification criteria through the production of the Handbook for the Computer Security Certification of Trusted Systems. Through this effort, NRL hopes to discover new and more efficient ways of satisfying the assurance requirement for a high assurance system.

Gray, James ``A Logical Approach to Multilevel Security in Probabilistic Systems,'' (with P. Syverson) Proc. 1992 IEEE Symposium on Security and Privacy, IEEE Press, 1992.

Kang, M., O. Costich, and J.N. Froscher, "A Practical Transaction Model and Untrusted Transaction Manager for a Multilevel-Secure Database system" Proc. 6th IFIP Working Conference on Database Security, August 1992, Vancouver, British Columbia, pp. 289-310. PostScript

A new transaction model for multilevel-secure databases which use the replicated architecture is presented. A basic concurrency control algorithm and two variations are given based on this transaction model. We also present new correctness criteria for multilevel-secure databases which use the replicated architecture. Based on this criteria, we prove that our algorithms are correct.

There are two components in the scheduler for multilevel-secure databases which use the replicated architecture; global and local schedulers. Since the global scheduler, which enforces data consistency among replicas, has to make scheduling decisions based on transactions (i.e., without any knowledge of actual data or physical layout of data), an accurate analysis technique which can detect conflicts among queries is needed. The data dependence analysis introduced here provides a method for precisely determining whether the portions of relations affected by various database operations overlap without the knowledge of actual data.

The concurrency control lock (e.g. file lock, table lock) has long been used as a canonical example of a covert channel in a database system. Locking is a fundamental concurrency control technique used in many kinds of computer systems beside database systems. Locking is generally considered to be interfering and hence unsuitable for multilevel systems. In this paper we show how such locks can be used for concurrency control, without introducing covert channels.

Catherine Meadows, "Applying Formal Methods to the Analysis of a Key Managment Protocol,'' The Journal of Computer Security," vol 1, no 1, Jan. 1992. PostScript

In this paper we develop methods for analyzing key management and authentication protocols using techniques developed for the solutions of equations in a term rewriting system. In particular, we describe a model of a class of protocols and possible attacks on those protocols as term rewriting systems, and we also describe a software tool based on a narrowing algorithm that can be used in the analysis of such protocols. We formally model a protocol and describe the results of using these techniques to analyze security properties. We show how a security flaw was found, and we also describe the verification of a corrected scheme using these techniques.

Moskowitz, I. and O. Costich, "A Classical Automata Approach to Noninterference Type Problems", Proc. IEEE Computer Security Foundations Workshop 5, IEEE Press, 1992. PostScript

Moskowitz, Ira ``The Influence of Delay Upon an Idealized Channel's Bandwidth,'' (with A. Miller) Proc. 1992 IEEE Symposium on Research in Security and Privacy, IEEE Press, 1992.

Moskowitz, Ira and A. Miller, ``The Channel Capacity of a Certain Noisy Timing Channel,'' IEEE Transactions on Information Theory, v. 38, no. 4, 1992.

Payne, C., D. Mihelcic, A. Moore, and K. Hayman, "The ECA critical requirements model", NRL Report 9528, Naval Research Laboratory, Washington DC, Dec., 1992. (to get a copy, contact C. Payne)

The ECA is an embedded computing device that processes message traffic for a network that must enforce end-to-end user message confidentiality. The ECA uses a commercial, off-the-shelf cryptographic device to transform sensitive data from the Red Domain of the network so that it can be transmitted over the untrusted communications links of the Black Domain. For transmission purposes, certain parts of a message, namely the message header, must be bypassed around the cryptographic device. The primary critical requirement for the ECA, "Restricted Red-to-Black Flow" (RRTBF), requires that the bypassed portion of each message must satisfy certain format restrictions, and that the rate of bypass must be constrained. In this report, we present an informal model of the ECA's critical requirements together with the assumptions under which the model was constructed. We then formalize this model by using the CSP Trace Model of computation.

We resolve a debate over the appropriateness for cryptographic protocol analysis of formalisms representing knowledge vs. those representing belief by showing that they are equally adequate for protocol analysis on the logical level. We discuss the significance of semantics for logics of cryptographic protocols. In particular, we look at semantics as a measure of a logic and as a reasoning tool in its own right. To illustrate the value of a semantics we use the semantics given in [Abadi and Tuttle 91] to resolve a debate over an alleged flaw in BAN, the logic of [Burrows, Abadi, and Needham 89].