The computer industry is increasingly dependent on open architectural standards for their competitive success. This paper describes a new approach to secure system design in which the various representations of the architecture of a software system are described formally and the desired security properties of the system are proven to hold at the architectural level. The main ideas are illustrated by means of the X/Open distributed transaction processing reference architecture, which is formalized and extended for secure access control as defined by the Bell-LaPadula model. The extension allows vendors to develop individual components independently and with minimal concern about security. Two important observations were gleaned on the implications of incorporating security into software architectures.

A multilevel relational database represents information in a multilevel state of the world, which is the knowledge of the truth value of a statement with respect to a level in a security lattice. The authors develop a semantic framework of the multilevel secure relational model with tuple-level labelling, which formalizes the notion of validity in multilevel relational databases. They also identify the multilevel security properties that precisely characterize the validity of multilevel relational databases, which can be maintained efficiently. Finally, they give an update semantics of the multilevel secure relational model that preserves both integrity and secrecy.

Query folding refers to the activity of determining if and how a query can be answered using a given set of resources, which might be materialized views, cached results of previous queries, or queries answerable by other databases. We investigate query folding in the context where queries and resources are conjunctive queries. We develop an exponential time algorithm that finds all complete or partial foldings, and a polynomial time algorithm for the subclass of acyclic conjunctive queries. Our results can be applied to query optimization in centralized databases, to query processing in distributed databases, and to query answering in federated databases.

In the proposed mandatory access control model, arbitrary, label changing policies can be expressed. The relatively simple model can capture a wide variety of security policies, including high-water marks, downgrading, separation of duties, and Chinese Walls. The model forms the basis for a tiered approach to the formal development of secure systems, whereby security verification can be spread across what makes up the reference monitor and the security requirement specification. The advantage of this approach is that once a trusted computing base (TCB) is in place, reconfiguring it for different security requirements requires verification of just the new requirements. We illustrate the approach with a number of examples, including one policy that permits high-level subjects to make relabelling requests on low-level objects; the policy is multilevel secure.

View-based access control enables content-based and context-based security, as opposed to the container-based security provided in operating systems. However, view-based access control in multilevel secure (MLS) databases suffers from two problems: safety and assurance. We investigate view-based access control in MLS relational databases for a large class of views expressible as project-select-join queries. We develop a polynomial-time label compilation algorithm that transforms view-level labelling to tuple-level labelling in such a way that guarantees safety and high assurance. We identify two problems related to optimal label compilation, and show that they are both NP-complete even for totally ordered security lattices of size two.

We develop a formal framework of MAC policies in multilevel relational databases. We identify the important components of MAC policies and their desirable properties. The framework provides a basis for systematically specifying MAC policies and characterizing their potential mismatches. Based on the framework, we compare and unify the MAC policies and policy components that are proposed in the literature or imposed in existing systems. Our framework could be used to capture and resolve MAC policy mismatches in the trusted interoperation of heterogeneous multilevel relational databases.

Advances in distributed systems and networking technology have made interoperation not only feasible but also increasingly popular. We define the interoperation of secure systems and its security, and prove complexity and composability results on obtaining optimal and secure interoperation. Most problems are NP-complete even for systems with very simple access control structures, while for a general setting the problem is undecidable. Nevertheless, composability reduces complexity in that secure global interoperation can be obtained incrementally by composing secure local interoperation. We illustrate, through an application in secure database interoperation, how these theoretical results can help system designers in practice.

We develop an efficient algorithm for the query interoperation among existing heterogeneous object-oriented and relational databases. Our algorithm utilizes a canonical deductive database as a uniform representation of object-oriented schema and data. High-order object queries are transformed to the canonical deductive database in which they are partially evaluated and optimized, before being translated to relational queries. Our algorithm can be incorporated into object-oriented interfaces to relational databases or object-oriented federated databases to support object queries to heterogeneous relational databases.>

Common security models such as Bell-LaPadula focus on the control of access to sensitive data but leave some important systems issues unspecified, such as the implementation of read-only objects, garbage collection, and object upgrade and downgrade paths. Consequently, different implementations of the same security model may have conflicting operational and security semantics. We propose the use of more expressive security labels for specifying these system issues within the security model, so that the semantics of a system design are precisely understood and are independent of implementation details.>

A method is presented for the stepwise refinement of an abstract architecture into a relatively correct lower-level architecture that is intended to implement it. A refinement step involves the application of a predefined refinement pattern that provides a routine solution to a standard architectural design problem. A pattern contains an abstract architecture schema and a more detailed schema intended to implement it. The two schemas usually contain very different architectural concepts (from different architectural styles). Once a refinement pattern is proven correct, instances of it can be used without proof in developing specific architectures. Individual refinements are compositional, permitting incremental development and local reasoning. A special correctness criterion is defined for the domain of software architecture, as well as an accompanying proof technique. A useful syntactic form of correct composition is defined. The main points are illustrated by means of familiar architectures for a compiler. A prototype implementation of the method has been used successfully in a real application.>

The design of a large system typically involves the development of a hierarchy of different but related architectures. A criterion for the relative correctness of an architecture is presented, and conditions for architecture composition are defined which ensure that the correctness of a composite architecture follows from the correctness of its parts. Both the criterion and the composition requirements reflect special considerations from the domain of software architecture.The main points are illustrated by means of familiar architecture for a compiler. A proof of the relative correctness of two different compiler architectures shows how to decompose a proof into generic properties, which are proved once for every pair of architectural styles, and instance-level properties, which must be proved for every architecture.

Advances in distributed systems and networking technology have made interoperation not only feasible but also increasingly popular. The authors define the interoperation of secure systems and its security, and prove complexity and composability results on obtaining optimal and secure interoperation. Most problems are NP-complete even for systems with very simple access control structures. Nevertheless, composability reduces complexity in that secure global interoperation can be obtained incrementally by composing secure local interoperation. The authors illustrate, through an application, how these theoretical results can help system designers in practice.>

A multilevel relational database with tuple-level labeling is a relational database together with a mapping, which associates a set of levels in a security lattice with every tuple in every relation in the database. Integrity constraints represent the invariant properties of data in a multilevel relational database. We study the relationship between integrity and secrecy, and show that they are not necessarily in fundamental conflict. We identify common classes of constraints whose enforcement is free of both static and dynamic inference channels. We also extend the integrity checking mechanism by proper update semantics to remove dynamic inference channels in the enforcement of more general classes of constraints.>

The addition of stringent security specifications to the list of requirements for an application poses many new problems in DBMS design and implementation, as well as database design, use, and maintenance. Tight security requirements, such as those that result in silent masking of witholding of true information from a user or the introduction of false information into query answers, also raise fundamental questions about the meaning of the database and the semantics of accompanying query languages. In this paper, we propose a belief-based semantics for secure databases, which provides a semantics for databases that can “lie” about the state of the world, or about their knowledge about the state of the world, in order to preserve security. This kind of semantics can be used as a helpful retrofit for the proposals for a “multilevel secure” database model (a particularly stringent form of security), and may be useful for less restrictive security policies as well. We also propose a family of query languages for multilevel secure relational database applications, and base the semantics of those languages on our semantics for secure databases. Our query languages are free of the semantic problems associated with use of ordinary SQL in a multilevel secure context, and should be easy for users to understand and employ.

Although the mathematical foundations of relational databases are very well established, the state of affairs for object-oriented databases is much less satisfactory. We propose a semantic foundation for object-oriented databases based on a simple logic of change called rewriting logic, and a language called MaudeLog that is based on that logic. Some key advantages of our approach include its logical nature, its simplicity without any need for higher-order features, the fact that dynamic aspects are directly addressed, the rigorous integration of user-definable algebraic data types within the framework, the existence of initial models, and the integration of query, update, and programming aspects within a single declarative language.

Multilevel relational database systems store information at different security classifications. An inference problem exists if it is possible for a user with a low-level clearance to draw conclusions about information at higher classifications. The authors are developing DISSECT, a tool for analyzing multilevel relational database schemas to assist in the detection and elimination of inference problems. A translation is defined from schemas to an equivalent graph representation, which can be presented graphically in DISSECT. The initial focus is on detection of inference problems that depend only on information all of which is stored in the database. In particular, potential inference problems are identified as different sequences of foreign key relationships that connect the same entities. Inferences can be blocked by upgrading the security classification of some of foreign key relationships. A global optimization approach to upgrading is suggested to block a set of inference problems that allows upgrade costs to be considered, and supports security categories as well as levels.>

Database programming requires knowledge of database semantics both to maintain database integrity and to explore more optimization opportunities. Automated programming of database transactions is desirable and feasible. In general, transactions use simple constructs and algorithms; specifications of database semantics are available; and transactions perform small incremental updates to database contents. Automated programming in such a restricted but well-understood and important domain is promising. We approach the synthesis of database transactions that preserve the validity of integrity constraints using deductive techniques. A transaction logic for a fairly expressive class of transactions is developed as the formalism within which the synthesis is conducted. Transactions are generated as the by-product of proving specifications in the logic. The Manna-Waldinger deductive-tableau system is extended with inference rules for the extraction of transactions from proofs, which require t...

Database updates are small and incremental compared to database contents. It is therefore desirable that recomputations of active relational expressions-such as views, derived data, integrity constraints, active queries, and monitors-can also be performed incrementally. An efficient algorithm for the incremental recomputation of active relational expressions based on finite differencing techniques is presented. Database updates are modeled as incremental changes to database relations, and the algorithm derives, by update propagation, the minimal incremental relational expressions that need recomputation. The algorithm has applications in the maintenance of materialized views and derived data, the checking of integrity constraints, and the evaluation of active queries and monitors.>

A description is given of a very effective method for the syntax-directed simplification of multirelation, multivariable, aggregate-free integrity constraints against a fairly general class of multirelation update transactions with partial specifications. Compared with other work, the approach covers a wider range of update transactions and integrity constraints, and explores more optimization opportunities with no more effort. The method is both a uniform generalization of previous research and a basis for examining arbitrary update transactions.>

We introduce a logical formalism for the specification of the dynamic behavior of databases. The evolution of databases is characterized by both the dynamic integrity constraints which describe the properties of state transitions and the transactions whose executions lead to state transitions. Our formalism is based on a variant of first-order situational logic in which the states of computations are explicit objects. Integrity constraints and transactions are uniformly specifiable as expressions in our language. We also point out the application of the formalism to the verification and synthesis of transactions.

A new relationship type is proposed which permits describing the issues raised when information is distributed over autonomous workstations. Such federated environments are becoming the dominant form of distributed systems. Fully synchronous update of replicated data is not feasible in such systems. The proposed identity connection identifies data which should eventually match, but which can be in differing states for some time intervals. The concept permits modeling of the systems which are now becoming common in data processing.