A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This article describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, the security property of interest is represented formally and a compact security model, containing only information needed to reason about the policy, is constructed. To reduce the cost of verification, the code to be verified is partitioned into three categories: Only the first category, less than 10% of the code, requires requires substantial effort to verify; the proof of the other two categories is relatively trivial. Our approach was developed to support a Common Criteria evaluation of the separation kernel of an embedded software system. This article describes 1) our techniques and theory for verifying the kernel code and 2) the artifacts produced: a Top Level Specification (TLS), a formal statement of the security property, a mechanized proof that the TLS satisfies the property, the partitioning of the code, and a demonstration that the code conforms to the TLS. The article also presents the formal argument that the kernel code conforms to the TLS and consequently satisfies the security property.

We have become increasingly dependent on a national technological fabric that contains software, computers, and communication networks as essential components. Unfortunately, our ability to build affordable software systems for which there exists compelling evidence that the systems delivers their services in a manner that satisfies certain critical properties has not kept pace with the importance that these systems play in our lives. There are five basic research issues that we must address if we are to advance our ability to build trustworthy software

We, as individuals, as well as governments, corporations, and institutions, form a networked society and we are increasingly dependent on that network. The very fabric of our everyday life and business utilizes this networked connectivity, particularly critical infrastructures such as the electric power grid, oil and gas pipeline and distribution systems, telecommunications, transportation, and water treatment systems. All of these applications, and many more, are relied upon daily and need to be "trustworthy." By trustworthiness, we mean many qualities which include, but are not limited to, availability, assurance of information delivered, reliability, security, survivability, recoverability, confidentiality, integrity and other "ilities." Basically, when you pick up the phone, you expect to hear a dial tone; when you turn on a light switch, you expect the light to turn on; and when you send an e-mail, you expect it to reach its intended recipient with message intact and without others reading it en route. Since all of our critical infrastructures are themselves network-centric systems, this trustworthiness is both difficult to achieve and critical to maintain. One panel session cannot begin to capture all of the aspects of trustworthy computing; however, this panel is composed of experts who will explore many of the fundamental aspects of this increasingly important topic, particularly focused on critical research needs.

Following Godel, consider a formal mathematical system to be a system of symbols together with rules for employing them (K. Godel, 1965). The rules may be formation rules (stipulating the strings of symbols that constitute well formed formulae), proof rules (stipulating the strings of formulae that constitute proofs), or semantic rules (mapping formulae into an algebraic domain). The rules must be recursive. The requirement that the rules be recursive is an important one since it makes it possible to construct a computer program that can determine whether a rule set has been correctly applied. This, in theory, should give us the ability to use computers to determine whether properties we attribute to specifications or computer programs hold for certain. However, the assurance that can be obtained from formal methods comes at a price. For many applications, formal methods are prohibitively expensive. The formal methods community has traditionally looked to computer security as an application area where the expense of faulty software would make the application of formal methods cost-effective. For its part, the computer security community has traditionally looked to formal methods as a source of assurance that goes beyond what is attainable by testing. Although the marriage of formal methods and computer security has not been completely smooth sailing, it has led to a substantial growth in each partner. The article documents that growth.

Since the initial work of Daryl McCullough (1987) on the subject, the security community has struggled with the problem of composing "possibilistic" information-flow properties. Such properties fall outside of the Alpern-Schneider safety/liveness domain, and hence, they are not subject to the Abadi-Lamport Composition Principle. The paper introduces a set of trace constructors called selective interleaving functions and shows that possibilistic information-flow properties are closure properties with respect to different classes of selective interleaving functions. This provides a uniform framework for analyzing these properties, allowing us to construct both a partial ordering for them and a theory of composition for them. We present a number of composition constructs, show the extent to which each preserves closure with respect to different classes of selective interleaving functions, and show that they are sufficient for forming the general hook-up construction. We see that although closure under a class of selective interleaving functions is generally preserved by product and cascading, it is not generally preserved by feedback, internal system composition constructs, or refinement. We examine the reason for this.

We use standard linear-time temporal logic to specify cryptographic protocols, model the system penetrator, and specify correctness requirements. The requirements are specified as standard safety properties, for which standard proof techniques apply. In particular, we are able to prove that the system penetrator cannot obtain a session key by any logical or algebraic techniques. We compare our work to Meadows' method. We argue that using standard temporal logic provides greater flexibility and generality, firmer foundations, easier integration with other formal methods, and greater confidence in the verification results.

Unlike previous approaches to developing a trusted database system, the replicated architecture approach provides access control at a high level of assurance through replication of data and operations. We present a model of the SINTRA replicated architecture trusted database system which shows how the logical (users') view of the system and its security policy is translated into the physical structure and operations of the SINTRA system. We formalize the intended security policy for replicated architecture and demonstrate that a high level of assurance can be obtained solely from replication with virtually no change to the structure of the underlying database systems or the security kernel.>

This paper presents a general theory of system composition for "possibilistic" security properties. We see that these properties fall outside of the Alpern-Schneider safety/liveness domain and hence, are not subject to the Abadi-Lamport composition principle. We then introduce a set of trace constructors called selective interleaving functions and show that possibilistic security properties are closure properties with respect to different classes of selective interleaving functions. This provides a uniform framework for analyzing these properties and allows us to construct a partial ordering for them. We present a number of composition constructs, show the extent to which each preserves closure with respect to different classes of selective interleaving functions, and show that they are sufficient for forming the general hook-up construction. We see that although closure under a class of selective interleaving functions is generally preserved by product and cascading, it is not generally preserved by feedback, internal system, composition constructs, or refinement. We examine the reason for this.>

We present a new para.digmfor the development of trustworthy systems.It differs from our current paradigm by separating distinct desiderata.that, are bundled in the Trusted Comp&er System Evaluation Criteria, requiring tha.t our formalisms be t.ied t.o real world concerns, requiring a uniform method for a.ssuring that formalisms a.re met, replacing a. code-t,henvalidate methodology by a. refiilement-l,a.sedmet.llodology, and using con~posa1~ilit.ylogic to develop systems from COTS software.

The trace method of software specification is extended to provide a natural semantics for a procedural programming language. This extension provides a method for proving program correctness that permits a direct proof of program Noninterference witho

A theory of information flow is developed that differs from that of nondeducibility, which is seen to be a theory of information sharing. The theory is used to develop a flow-based security model (FM) and to show that the proper treatment of security-relevant causal factors in such a framework is very tricky. Using FM as a standard for comparison, an examination is made of interference, generalized noninterference, and extensions to noninterference designed to protect high-level output, and it is seen that the proper treatment of causal factors in such models requires programs to be considered as explicit input to systems. This gives a new perspective on security levels. The model of D.E. Bell and L.J. LaPadula (1973), on the other hand, more successfully models security-relevant causal information, although this success is bought at the expense of the model being vague about its primitives. This vagueness is examined with respect to the claim that the Bell-LaPadula model and noninterference are equivalent.>

A general framework is developed in which various mandatory access control security models that allow changes in security levels can be formalized. These models form a Boolean algebra. The framework is expanded to include models that allow n-person rules necessary for discretionary access controls in an industrial security setting. The resulting framework is a distributive lattice.>

A method for evaluating security models is developed and applied to the model of Bell and LaPadula. The method shows the inadequacy of the Bell and LaPadula model, in particular, and the impossibility of any adequate definition of a secure system based solely on the notion of a secure state. The implications for the fruitfulness of seeking a global definition of a secure system and for the state of foundational research in computer security, in general, is discussed.

An intuitive presentation of the trace method for the abstract specification of software contains sample specifications, syntactic and semantic definitions of consistency and totalness, methods for proving specifications consistent and total, and a comparison of the method with the algebraic approach to specification. This intuitive presentation is underpinned by a formal syntax, semantics, and derivation system for the method. Completeness and soundness theorems establish the correctness of the derivation system with respect to the semantics, the coextensiveness of the syntactic definitions of consistency and totalness with their semantic counterparts, and the correctness of the proof methods presented. Areas for future research are discussed.