Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for verification. This paper describes a novel and practical approach to formally establishing the security of code. The approach begins with a well-defined set of security properties and, based on the properties, constructs a compact security model containing only information needed to rea-son about the properties. Our approach was formulated to provide evidence for a Common Criteria evaluation of an embedded soft-ware system which uses a separation kernel to enforce data separation. The paper describes 1) our approach to verifying the kernel code and 2) the artifacts used in the evaluation: a Top Level Specification (TLS) of the kernel behavior, a formal definition of dataseparation, a mechanized proof that the TLS enforces data separation, code annotated with pre- and postconditions and partitioned into three categories, and a formal demonstration that each category of code enforces data separation. Also presented is the formal argument that the code satisfies the TLS.

The biggest cost driver in building a High Assurance System can often be the choice of method used to attain sufficient trust in the system. This talk will take a look at trust methodology, some of the issues involved, and some of the history that surrounds these issues. We will then examine some newer applications for trusted systems where the traditional methods break down, and discuss a possible new paradigm for achieving trust.

We favor an approach to building secure systems that includes an application-based security model. An instance of such a model and its formalization have been presented. Important aspects of the model are: (1) because it is framed in terms of operations and data objects that the user sees, the model captures the system's security requirements in a way that is understandable to users; (2) the model defines a hierarchy of entities and references; access to an entity can be controlled based on the path used to refer to it; (3) because the model avoids specifying implementation strategies, software developers are free to choose the most effective implementation; (4) the model and its formalization provide a basis for certifiers to assess the security of the system as a whole. Simplicity and clarity in the model's statement have been primary goals. The model's statement does not, however, disguise the complexity that is inherent in the application. In this respect, we have striven for a model that is as simple as possible but stops short of distorting the user's view of the system. The work reported demonstrates the feasibility of defining an application-based security model informally and subsequently formalizing it.

The concept of non-interference seeks to characterize the absence of information flows through a computer system. The intuition is startlingly simple. Suppose that we want to assert that no information may flow from user A to user B via the system S. We characterize this by asserting that B’s view of S is unchanged by any alteration in A’s behaviour. It is thus asserting that A can have no causal influence on B’s interactions with and observations of the system. Non-interference is such a simple and obvious characterization of MLS confidentiality that the security community is understandably reluctant to give it up. However, it has well known problems. First, in real systems high-level input interferes with low-level output all the time. High-level files can be encrypted, sanitized, or simply downgraded and sent on their way over low-level networks. Second, after fifteen years of trying, we still don’t have any consensus as to what is the “correct” nondeterministic formulation of it. Nondeterministic versions tend to be too weak (e.g., Nondeducibility), too strong (e.g., Noninference), too cumbersome (e.g., PNI and AFM), too limiting (e.g., the Roscoe, Woodcock, Wulf determinism approach) too Baroque (e.g., Restrictiveness), or some combination of the five. In [2] it is argued that, in a process algebraic setting, the characterization of non-interference reduces to characterizing the equivalence of certain processes. This in turn is a fundamental and difficult question of theoretical computer science and one to which there is no universally agreed answer. Thus it is not even clear whether a “correct”, Platonic notion of secrecy actually exists. Non-interference would seem to be a fundamental notion in information security. It could be argued that, if we cannot get the specification and verification of the absence of information flows right, we really don’t understand the foundations of our subject. On the other hand, it is such an abstract formulation that it seems remote from real concerns of security managers, policy makers and the developers of secure systems. Most “real” security policies are concerned with specifying who has access to what resources under what circumstances. Non-interference is never mentioned. Furthermore, non-interference is in practice impossible to realise in any real system: contention for resources etc render it infeasible. Even the so-called One-WayRegulators (e.g. the NRL Pump) allow some downward flow, albeit of low channel capacity. The study of non-interference arose from the need to understand why covert channels were possible, at a time when the only theoretical security models were access-control models, which were unable to explain them. The first wave of responses consisted of information flow models, which used the syntactic structure of statements to recognize possible flows, such as “indirect flow” from the condition of an if-then statement to variables that might be modified in its body. These models were found to overestimate flows. The second wave of models were the deterministic non-interference models, which were based on the notion of functional dependency. These models explained some covert channels, and found flows only where they really existed. Subsequent varieties of models found more channels by allowing for nondeterminacy in the computer system model, either “possibilistic” or probabilistic, and still other models addressed desirable features like composability. What’s wrong with these models? This question could be addressed at several levels. At the policy level, it has been suggested that no one cares about covert channels anymore, therefore models that purport to explain them are uninteresting. This does not really seem to be a valid response. There may be a shift in application areas, however. There is less emphasis in the design of multilevel operating systems, but more interest in something like the Bleichenbacher attack on the PKCS #1 cryptographic protocol standard [1], where a channel that is due partly to the algorithm and partly to the protocol design leads to compromise of encrypted data. Attacks that might expose a stored key are of great concern. The basic principles of information compromise still apply. There is also the practical question of how noninterference theory can be translated into efficient algorithms for detecting covert channels. Non-interference anal-

This debate was conceived by Carl Landwehr, who asked me to serve as moderator. The proposition under discussion was first put forward by Bill Wulf in the JavaSoft Forum 1.1 (http://java.sun.com/forum/securityForum.html). Wulf objects to the JavaSoft security model, which aims to protect user files, network connections! and other resources from malicious applets by restricting applets to executing in a “sandbox”. Wulf states:

To provide a firm foundation for proofs about the security properties of a system specification or implementation, a formal statement of its security model is needed. This paper presents a formal model that corresponds to an informal, application-based security model for military message systems (MMS) that has been documented elsewhere. Following the formal statement, some considerations that led to its present form are discussed. The paper concludes with the statement of a "Basic Security Theorem" for the model.

Military systems that process classified information must operate in a secure manner; that is, they must adequately protect information against unauthorized disclosure, modification, and withholding.A goal of current research in computer security is to facilitate the construction of multilevel secure systems, systems that protect information of different classifications from users with different clearances.Security models are used to define the concept of security embodied by a computer system.A single model, called the Bell and LaPadula model, has dominated recent efforts to build secure systems but has deficiencies.We are developing a new approach to defining security models based on the idea that a security model should be derived from a specific application.To evaluate our approach, we have formulated a security model for a family of military message systems.This paper introduces the message system application, describes the problems of using the Bell-LaPadula model in real applications, and presents our security model both informally and formally.Significant aspects of the security model are its definition of multilevel objects and its inclusion of application-dependent security assertions.Prototypes based on this model are being developed.

An abstract requirements specification states system requirements precisely without describing a real or a paradigm implementation. Although such specifications have important advantages, they are difficult to produce for complex systems and hence are seldom seen in the "real" programming world. This paper introduces an approach to producing abstract requirements specifications that applies to a significant class of real-world systems, including any system that must reconstruct data that have undergone a sequence of transformations. tions. It also describes how the approach was used to produce a requirements document for SCP, a small, but nontrivial Navy communications system. The specification techniques used in the SCP requirements document are introduced and illustrated with examples.