1993

Costich, Oliver and S. Jajodia. "Maintaining Multilevel Transaction Atomicity in MLS Database Systems with Kernelized Architecture," in Database Security VI: Status and Prospects, eds. B. Thuraisingham and C. Landwehr, North-Holland, 1993, pp. 249-266. PostScript, PDF

In most models of trusted database systems, transactions are considered to be single-level subjects. As a consequence, users are denied the ability to execute some transactions that can be run on conventional (untrusted) database systems, namely those that perform functions that become inherently multilevel in the MLS environment. This paper introduces a notion of multilevel transaction and proceeds to an algorithm for their concurrent execution. The algorithm is proven to be correct in the sense that resulting schedule for executing the multilevel transactions is one-copy serializable.

Gray, James W. "On Introducing Noise into the Bus Contention Channel," Proc. 1993 IEEE Symposium on Security and Privacy, IEEE Press, 1993.

Kang, Myong H. and Peyton, Rodney. "Design Documentation for the SINTRA Global Scheduler," NRL Memorandum Report #5542-93-7362, June 30, 1993. PostScript, PDF

In this report, we present the detailed description of the Secure Information Through Replicated Architecture (SINTRA) global scheduler. The detailed description includes: (1) the replica control algorithm, (2) design descriptions, and (3) rational behind our decision to choose specific methodology, an implementation language, and software engineering principles.

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.

Communication from a low-level to a high-level system without acknowledgements will be unreliable; with acknowledgements, it can be insecure. We propose to provide quantifiable security, acceptable reliability, and minimal performance penalties by interposing a device (called the Pump) to push messages to the high system and provide a controlled stream of acknowledgements to the low system.

This paper describes how the Pump supports the transmission of messages upward and limits the capacity of the covert timing channel in the acknowledgement stream without affecting the average acknowledgement delay seen by the low system or the message delivery delay seen by the high system in the absence of actual Trojan horses. By adding random delays to the acknowledgment stream when the Pump's message buffer is full, we show how to further reduce the covert channel capacity even in the presence of cooperating Trojan horses in both the high and low systems. We also discuss engineering tradeoffs relevant to practical use of the Pump.

An organized record of actual flaws can be useful to designers, implementors, and evaluators of computer systems. This paper provides a taxonomy for computer program security flaws together with an appendix that carefully documents 50 actual security flaws. These flaws have all been described previously in the open literature, but in widely separated places. For those new to the field of computer security, they provide a good introduction to the characteristics of security flaws and how they can arise. Because these flaws were not randomly selected from a valid statistical sample of such flaws, we make no strong claims concerning the likely distribution of actual security flaws within the taxonomy. However, this method of organizing security flaw data can help those who have custody of more representative samples to organize them and to focus their efforts to remove and, eventually, to prevent the introduction of security flaws.

This volume contains the papers presented at the Third IFIP International Working Conference on Dependable Computing for Critical Applications, sponsored by IFIP WG 10.4, as revised by the authors following presentation. System developers increasingly apply computers where they can affect the safety and security of people and equipment. This conference, like its predecessors, addressed various aspects of computer system dependability, a broad term defined as the degree of trust that may justifiably be placed in a system's reliability, availability, safety, security, and performance. The program committee selected 18 papers for presentation from a total of 74 submissions. The resulting program represented a broad spectrum of interests, with papers from universities, corporations, and government agencies in eight countries.

The history of attempts to secure computer systems against threats to confidentiality, integrity, and availability of data is breifly surveyed, and the danger of repeating a portion of that history is noted. Areas needing research attention are highlighted, and a new approach to developing certified systems is described.

This volume contains the papers presented at the Sixth IFIP WG11.3 Working Conference on Database Security, as revised by the authors following presentation, together with an account of the discussions held during the meeting and the IFIP WG11.3 Research Questions List. Papers presented covered a wide range of topics in database security including the semantics of multilevel database applications, security policies and models, the inference problem, and multilevel database concurrency control.

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.

The most critical problem with associated with implementing replicated architecture multilevel-secure database systems is transaction management: concurrency control, mutual consistency of replicas, and atomic recovery from failures, under the constraints of multilevel security. This paper investigates and compares the performance of five of the most promising transaction management approaches, via analytic performance modeling. We find that all five have acceptable performance and, over a wide range of circumstances, can be chosen based on structural considerations rather than performance.

Payne, C., J.N. Froscher, and C. E. Landwehr. "Toward a comprehensive INFOSEC certification methodology," Proc. Sixteenth National Computer Security Conference, Baltimore, MD, Sept., 1993. pp. 165-172. PostScript, PDF

Accreditors want to know what vulnerabilities will exist if they decide to turn on a system. TCSEC evaluations address products, not systems. Not only the hardware and software of a system are of concern; the accreditor needs to view the system components in relation to the environment in which they operate and in relation to the system's mission. This paper proposes an informal but comprehensive approach that can provide the accreditor with the necessary information. First, we discuss the identification of assumptions and assertions that reflect system INFOSEC requirements. Second, we propose the definition of an assurance strategy to integrate security engineering and system engineering. The assurance strategy initially documents the set of assumptions and assertions derived from the requirements It is elaborated and refined throughout the development, yielding the assurance argument, delivered with the system, which provides the primary technical basis for the certification decision. With the assurance strategy in place, certification of the trusted system can become an audit of the development process.

In [BAN89] Burrows, Abadi, and Needham presented a logic (BAN) for analyzing cryptographic protocols in terms of belief. This logic is quite useful in uncovering flaws in protocols; however, it also has produced confusion and controversy. Much of the confusion was cleared up when Abadi and Tuttle provided a semantics for a version of that logic (AT) in [AT91].

In this paper we present a protocol to show that both BAN and AT are not expressive enough to capture all of the kinds of flaws that appear to be within their scope. We then present a logic that adds temporal formalisms to AT and that is rich enough to reveal the flaws in the presented protocol; nonetheless, this logic is sound with respect to the same semantics that was given in [AT91]. Finally, we argue that any approach of this type is inadequate by itself to demonstrate the absence of such flaws. We must supplement the formal logic with semantic analysis techniques.

In [KSL92], Kehne et al. present a protocol (KSL) for key distribution. Their protocol allows for repeated authentication by means of a ticket. They also give a proof in BAN logic [BAN89] that the protocol provides the principals with a reasonable degree of trust in the authentication and key distribution. They present an optimality result that their protocol contains a minimal number of messages. Nonetheless, in [NS93] Neuman and Stubblebine present a protocol (NS) as an explicit alternative to KSL that requires one less message in the initial authentication and key distribution. One goal of this paper is to examine some of the reasons for this discrepancy. Another goal is to demonstrate possible attacks on NS. Like any attacks on cryptographic protocols, these depend on assumptions about implementation details. But, when possible they are serious: a penetrator can initiate the protocol, masquerade as another principal, obtain the session key, and even generate the session key herself. We will set out implementation assumptions required for the attacks to take place and implementation assumptions that preclude such an attack. We will also look at other protocols, including one that is not subject to this form of attack and has the same number of messages as NS. Finally, we will briefly discuss the logical analysis of these repeat authentication protocols.

In this paper we present a formal language for specifying and reasoning about cryptographic protocol requirements. We give examples of simple sets of requirements in that language. We look at two versions of a protocol that might meet those requirements and show how to specify them in the language of the NRL Protocol Analyzer. We also show how to map one of our sets of formal requirements to the language of the NRL Protocol Analyzer and use the Analyzer to show that one version of the protocol meets those requirements. In other words, we use the Analyzer as a model checker to assess the validity of the formulae that make up the requirements.

Back to the CHACS Publications Page.

Back to the Publications Page.