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 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.

It is pointed out that the incremental cost of a change to a program is often disproportionately high because of inadequate means of determining the semantic effects of the change. A practical logical technique for finding the semantic effects of changes through a direct analysis of the program is presented. The programming language features considered include parametrized modules, procedures, and global variables. The logic described is approximate in that weak (conservative) results sometimes are inferred. Isolating the exact effects of a change is undecidable in general. The basis for an approximation is a structural interpretation of the information-flow relationships among program objects. The approximate inference system is concise, abstract, extensible, and decidable, giving it significant advantages over the main alternative formalizations. The authors' implementation of the logic records the justification for each dependency to facilitate the interpretation of results.>

PegsSys is an experimental system in which a user formally describes how a program is put together by means of a hierarchically structured collection of pictures, called formal dependency diagrams (FDDs). Icons in an FDD denote a wide range of data and control dependencies among the relatively coarse-grained entities contained in large programs. Dependencies considered atomic with respect to one level in a hierarchy can be decomposed into a number of dependencies at a lower level. Each dependency can be a predefined primitive of the FDD language or it can be defined by a PegaSys user in terms of the primitives. A PegsSys user is given the illusion that logical formulas do not exist, even though PegaSys reasons about them internally. This involves (1) checking whether an FDD is meaningful syntactically, (2) determining whether hierarchical refinements of an FDD are methodologically sound, and (3) deciding whether an FDD hierarchy is logically consistent with the program that it is intended to describe. The techniques used to provide these capabilities are discussed along with the logical properties that enable PegaSys to maintain the user illusion.

Since developing and maintaining formally verified programs is an incremental activity, one is not only faced with the problem of constructing specifications, programs, and proofs, but also with the complex problem of determining what previous work remains valid following incremental changes. A system that reasons about changes must build a detailed model of each development and be able to apply its knowledge, the same kind of knowledge an expert would have, to integrate new or changed information into an existing model.