A distinctive concern in the U.S. military for computer security dates from the emergence of time-sharing systems in the 1960s.  This paper traces the subsequent dvelopment of the idea of a \“security kernel\” and of the mathmtical modeling of security, focusing in particular on the paradigmatic Bell LaPadula model.  The paper examines the connections between security and formal , deductiv verification of the properties of computer systems.  It goes on to discuss differencs between the cultures of communications security and computer security, the bureaucratic turf war over security, and the emergence and impact of the Department of Defense\‘s Trusted Computer System Evaluation Criteria (the so-called Orange Book), which effectively took its final form in 1983.  The paper ends by outlining the fragmentation of computer security since the Orange Book was written.

Will developing intrusion detection capabilities meet the operational, performance, and implementation goals of the US Air Force?  To help ensure that they will, the MITRE C2 Protect Mission-Oriented Investigation and Experimentation (MOIE) project is making Air Force goals for intrusion detection available to commercial interests that may develop capabilities. This paper, a first cut at defining goals, capitalizes on customer and corporate experience with intrusion detection tools as well as knowledge of the problem domain.  It creates an information base abot intrusion detection, providing a framework for discussing, refining, and enhancing intrusion detection goals.

Will future intrusion detection tools meet the goals of theh US Air Force?  To help ensure that they will, the MITRE C2 Protect Mission-Oriented Investigation and Experimentation (MOIE) project is forecasting the environment for Air Force intrusion detection.  The forecast should be helpful to commercial interests that may develop capabilities, can be a means of coordinating and shaping future finding decisions, and may provide a common framework for discussing issues. The first phase of the MOIE project capturred customer and corporate experience with intrusion detection tools as well as joint knowledge of the intrusion detection tools within the Air Force.  This paper, a product of the seond phase of effort, records trend information developed primarily from in-house technical expertise.

This paper details our experiences with successfully validating a trusted device at FIPS 140-1 Level 4 - earning the world\‘s first certificate at this highest level.  Over the last several years, our group designed and built a physically secure PCI card containing general-purose processor with crypto support.  However, for this device to function as a trusted platform for secure coprocessor applications, we needed to establish that assurance through independent validation.  We chose FIPS 140-1, since discussions of secure hardware usually cite that standard, and Level 4, since the weaker levels did not provide sufficient assurance for many proposed applications. Successful validation at Level 4 required withstanding a fairly open-ended suite of physical attacks, and preparing formal modeling and verification of the internal software - as well as meeting a number of other sizable chalenges that were not initially apparent.  In some sense, our validation effort was an experiement to quantify the design and work effort necassary to achieve the previously unachieved security assurance level.  Since our device is a programmable platform, we hope this work substantially lowers the barrier for others to develop, deploy, and validate secure coprocessor applications.

We give a formal specification of the dynamic loading of classes in the Java Virtual Machine (JVM) and of the visibility of mmbers of the loaded classes.  This specification is obtained by abstracting out the part of the run-time state of the JVM that is relevant for dynamic loading and visibility, and consists of a set of inference rules defining abstract operations for loading, linking and verifying classes.  The formalisation of visibility includes an axiomatisation of the rules for membership of a class under inheritance, and of accessibility of a member in th presence of accessibility modifiers such as private and protected.  We believe this specification to be at the right level of abstraction to help reasoning about security properties in Java because it is precise enough to include the security critical features of the language (e.g. visibility rules, dynamic loading and class loaders) and abstract enough to avoid all the irrelevant details (w.r.t. security) of the computer sematics.  The contribution of the formalisation is twofold.  First, it provides a clear and concise description of the loading process and the rules for member visibility compared to the definitions of the Java language and the JVM.  Second, it is sufficiently simple to allow calculations of the effects of load operations in JVM.  We demonstrate the usability of this formalisation by applying it to an example, due to Saraswat, of how dynamic loading can affect th visibility in a way that leads to a security breach in the JVM.

In a multilevel security database there are multiple beliefs about a given real world object.  The ability of a database model to accommodate multiple beliefs is termed polyinstantiation in the multilevel security literature.  In thi paper we remark that in an abstract sense polyinstantiation is a priori present in all models for temporal and spatial datbass.  In particular we investigate the applicability of the paramtric models for temporal data to query multilevel security data nd, as a case study, compare it to model for multilevel scurity given by Winslett, Smith, and Qian.

Recent work has shown that conventional operating system audit trails are insufficient to detect low-level network attacks.  Because audit are typically based upon system calls or application sources, operations in the network protocol stack go unaudited.  In our earlier work, we determined the audit data needed to detect low-level network attacks.  in this paper we describe an implementation of an audit system which collects this data and analyze th issues that guided th implementation.  Finally, we report the performance impact on th systm and the rat of audit data accumulation in a test network.