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.

DoD operates many system high enclaves with limited information flow between enclaves at different security levels. Too often, the result is duplication of operations and inconsistent and untimely data at different sites, which reduces the effectiveness of DoD decision support systems. This paper describes our solution to this problem as it arises in installations of the Joint Maritime Command Information System JMCIS, an integrated C4I system. Our approach views databases in more classified enclaves as potential replica sites for data from less classified enclaves. Replicated data flows from lower enclaves to higher ones via one-way connections, yielding a high assurance MLS multi-level secure distributed system. The one-way connections are the only trusted components.
This approach is based on our work on SINTRA Secure Information Through Replicated Architecture, and applies generally to any collection of systems each running a database at system high. It complements and exploits modern system design methods, which separate data management from data processing, and enables effective, low-cost MLS operation within that paradigm. In addition to describing current JMCIS installations and our architectural approach, the paper presents our approach for justifying a systems security and our use of formal methods to increase assurance that security requirements are met.

The External COMSEC Adaptor (ECA) is a device responsible for providing cryptographic protection of information based on rules that (possibly coarsely) define the sensitivity of that information. The ECA is trusted to satisfy a set of critical requirements that support data confidentiality in the network in which it is embedded. Ensuring that the ECA is worthy of this trust requires defining its critical requirements precisely and constructing a strong argument that its implementation satisfies these requirements. This paper describes a software engineering methodology that uses formal methods for specifying and verifying the most critical requirements of the ECA and uses testing and simulation for verifying the overall functional requirements of the ECA. The methodology integrates the formal specifications and proofs with structured software documentation to clarify the relationship between the refinement of ECA functionality and the argument that the ECA meets its critical requirements. This methodology was used successfully to build the ECA using the KG84A to satisfy its cryptographic requirements.

The assurance argument that a trusted system satisfies its information security requirements must be convincing, because the argument supports the accreditation decision to allow the computer to process classified information in an operational environment. Assurance is achieved through understanding, but some evidence that supports the assurance argument can be difficult to understand. This paper describes a novel application of a technique, called literate programming 11, that significantly improves the readability of the assurance argument while maintaining its consistency with formal specifications that are input to specification and verification systems. We describe an application of this technique to a simple example and discuss the lessons learned from this report.

We describe two integrated languages and associated tools for capturing and analyzing two different views of the architecture of an embedded system. One language is tailored to address guidance, navigation and control issues, while the other is tailored to address real-time, fault-tolerance, secure partitioning and multi-processor system issues. Both languages have tools that perform analyses appropriate for the issues each addresses, and tools to automatically configure the application software from a sufficiently detailed specification. The integrated languages and tools are intended to support an architecture reuse development process, in which the development of a new product in a family of similar products starts from a generic or reusable architecture specification for that product family.

The Distributed CIRCA (D-CIRCA) project is focused on developing planning technology to concurrently build and execute real-time control plans for multiple cooperating autonomous agents. In this paper, we demonstrate how the goals of the D-CIRCA program relating to distributed, cooperating agents motivate our recent work on Dynamic Abstraction Planning (DAP). We contend that problems of incomplete knowledge, limited communication bandwidth, and state-space explosion can all be addressed by abstraction. We present a high-level description of the DAP technique and conclude by outlining several issues for future work.

We have recently begun work on extending our least-commitment constraint-based scheduling technology to handle more complex dynamical models. The current scheduling process involves a complex interaction between discrete choices (resource assignments, sequencing decisions), and a continuous temporal model. Discrete choices enforce new constraints on the temporal model. Those constraints may be inconsistent with the current model, thus forcing backtracking in the discrete domain, or if consistent, may serve to constrain choices for discrete variables not yet assigned. The extensions currently underway involve adapting and modifying more complex continuous models. This will permit us to apply the system to such complex problems as crude blending or tank management at a refinery, aircraft mission planning, or spacecraft mission planning and control.

To an increasing extent, large-scale information processing is a distributed phenomenon. As the trend in computing moves further towards distributed networks of powerful workstations and information servers, we see the growing importance of solutions to dynamic distributed scheduling problems. In these domains, resource providers are distributed both geographically and bureaucratically, so that no central authority can dictate a global schedule. Resource consumers are also distributed: tasks arrive at different locations according to arrival functions that are at best stochastically predictable. In this paper, we describe a distributed constraint-based scheduling system that adjusts task distribution and execution times through the negotiation of contracts, using a refinement of the Contract Net protocol. By combining the minimal-commitment capabilities of constraint-based scheduling with the distributed coordination features of contracting, this system responds flexibly to dynamic variations in load balance and unpredictable task arrivals. Large-scale simulations show significant performance benefits to using powerful scheduling methods in the determination of contract negotiation bids. These results can be used to improve the performance of distributed computing systems cooperating to process large-scale shareable tasks.