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.

In this paper we discuss two abstraction techniques we use in CIRCA planning (Musliner, Durfee, & Shin 1993; 1995). CIRCA agents construct and execute plans for controlling real-time systems that interact with a dynamic environment including uncontrolled, exogenous events. In these environments, catastrophic failure is possible if a timely control action is not taken in certain situations. Control plans for these environments must provide guarantees that failures will not occur. Therefore, the CIRCA planning problem is one of generating a timed, discrete event controller (Ostroff & Wonham 1990) that attempts to achieve goals while delivering performance guarantees. In this generation process we abstract temporal information, using a special-purpose temporal prover to summarize information about the latency of various events. We also use a technique we call Dynamic Abstraction Planning (Goldman et al. 1997) to minimize the (non-temporal) feature space of the controllers.

In this position paper we present the two abstraction methods used in CIRCA state-space planning. We start by reviewing the CIRCA architecture, which couples a deliberative planning component with a scheduler and a real-time executive. We then present the state-space planning problem, which is the responsibility of CIRCA’s AI Subsystem. We then discuss temporal abstraction in state-space planning, and then present Dynamic Abstraction Planning (DAP), a planning technique that dynamically and locally abstracts the feature space of the controller NFA. We relate these techniques to methods used in AI planning, Model (automation) Minimization and Markov Decision Processes.

This paper demonstrates that composition and refinement techniques are a promising solution for performing rigorous, security architecture trade-off analysis. Such analysis typically occurs in one of two forms: comparing two architectures for implementation and determining the impact of change to an implemented architecture. Composition and refinement techniques reduce the overhead of such analysis significantly over traditional formal methods by facilitating specification and proof reuse and by providing powerful reasoning tools. In this paper, we propose an approach for applying composition and refinement techniques to trade-off analysis. Our approach relies on a formal composition and refinement framework, which is not described here. We describe the approach and apply it to a simple example. We conclude with lessons learned and future work.

This paper argues that Napoleon, a flexible, role-based access control (RBAC) modeling environment, is also a practical solution for enforcing business process control,or workflow, policies. Napoleon provides two important benefits for workflow: simplified policy management and support for heterogeneous, distributed systems. We discuss our strategy for modeling workflow in Napoleon, and we present an architecture that incorporates Napoleon into a workflow management system.