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.

In this paper we present a sound and complete linear planning algorithm which accommodates conditional actions: actions whose effects cannot be predicted with certainty. Conditional linear planning is significantly simpler than conditional non-linear planning in conception and implementation. Furthermore, the efficiency trade-offs which favor non-linear planning do not necessarily carry over with the same force to planning with conditional actions. We have applied our conditional linear planner, Plinth, to the problem of planning image processing actions for NASA’s Earth Observing System. We discuss the extension of Plinth to probabilistic planning.

Several current NASA programs such as the EOSDIS Core System (ECS) have data processing and data management requirements that call for an integrated planning andscheduling capability. As we have shown in previous work, the scale and complexity of data ingest and product generation for ECS will overwhelm the capabilities of manual planning and scheduling procedures. Meeting this challenge requires the innovative application of advanced technology. Some of our work on developing this technology was described in a paper presented at the 1994 Goddard AI Conference, in which we talked about advanced planning and scheduling capabilities for product generation. We are now moving to deploy some of the technology we have developed for operational use.