Applying the Abadi-Lamport composition theorem in real-world secure system integration environments

This paper describes research that addresses application of the Abadi Lamport Composition theorem to the integration of real-world systems. The Formal Development Methodology (FDM) was used to describe system and component security properties, including access control, label consistency, and communications constraints. These descriptions were then used as input to the FDM theorem prover to prove the hypotheses of the Abadi Lamport Composition Rule. Although the FDM tools were not designed for this application, they were found to be usable as long as the properties being addressed are limited to safety properties. The Abadi Lamport framework provides a powerful, well-grounded mathematical proof rule for composing the properties of components to form systems. The combination of this framework and a usable supporting tool set is especially valuable for system integration efforts, in that it enhances the integrator´s ability to describe, analyze, understand, and control the integration process