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.

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 communication 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 than formalize this model by using the CSP Trace Model of computation.

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 these components in relation to the environment in which they operate and in relation to the system’s mission and the threats to it. This paper proposes an informal but comprehensive certification 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.

We briefly describe the current implementation of the Time Map Manager (TMM), followed by a description of the system’s suitability for and application to planning and scheduling tasks.

Classical nonlinear planning has been studied in the abstract since the early 1970’s. More recently, interest has grown in applying these techniques to real problems, or at the least to simplified versions of real problems. In this paper, we explore some of the implications and results of those applications, with an eye to addressing the question of where the main problems lie. What successes have been achieved? What remains to be done? In particular, what fundamental representational or algorithmic issues, if any, need to be addressed before classical planning becomes a useful tool for large, complex, real-world problems?

In this paper, we explore the expressive and computational properties of the logic of model-preference defaults (MPD). We extend the set of sublanguages of MPD known to be tractable. We compare MPD with the approaches to nonmonotonic reasoning represented by default logic and circumscription. Finally, we discuss MPD’’s suitability for various applications of nonmonotonic reasoning, including inheritance, temporal reasoning, and knowledge representation. In doing so, we show that MPD provides tractable solutions to the problems of temporal projection and mixing strict and defeasible inheritance.

Past experience in system security certification indicates the need for developers of high assurance systems to coherently integrate the evidence that their system satisfies its critical requirements. This document describes a method based on literate programming techniques to help developers present the evidence they gather in a manner that facilitates the certification effort. We demonstrate this method through the implementation and verification of a small but nontrivial, security-relevant example, an RS-232 character repeater. By addressing many of the important issues in system design, we expect that this example will provide a model for developing assurance arguments for full-scale composite systems with corresponding gains in the expediency of the system certification process.

In this paper, we present an analysis of planning with uncertain information regarding both the state of the world and the effects of actions using a Strips- or (propositional) Adl-style representation. We provide formal definitions of plans under incomplete information and conditional plans, and describe Plinth, a conditional linear planner based on these definitions. We also clarify the definition of the term “conditional action, ” which has been variously used to denote actions with context-dependent effects and actions with uncertain outcomes. We show that the latter can, in theory, be viewed as a special case of the former but that to do so requires one to sacrifice the simple, single-model representation for one which can distinguish between a proposition and beliefs about that proposition.

Honeywell has developed an approach, State-Based Feature Recognition (SBFR), automatically recognize trends and predict failures using parametric data. We have applied this technique to the health monitoring of space vehicle systems including the Orbital Maneuvering System/Reaction Control System for the Space Shuttle, the Attitude Determination and Control System for Space Station Freedom, and Electro-Mechanical Actuators to be used on future space vehicles. Our success in this domain has led us to explore applications in other domains, such as power plant monitoring and building control. Applying SBFR to the medical domain is a recent exploration and this paper represents the first foray into that domain. It will introduce SBFR, review some similar work, describe its current status, and discuss applications of the technology to the medical domain.

Previous work at NRL demonstrated the benefits of a security modeling approach for building high assurance systems for particular application domains. This paper introduces an application domain called selective bypass that is prominent in certain network security solutions. We present a parameterized modeling framework for the domain and then instantiate a confidentiality model for a particular application, called the External COMSEC Adaptor (ECA), within the framework. We conclude with lessons we learned from modeling, implementing and verifying the ECA. Our experience supports the use of the application-based security modeling approach for high assurance systems.