Verifiable composition of access control and application features

Abstract

Access control features are often spread across and tangled with other functionality in a design. This makes modifying and replacing these features in a design difficult. Aspect-oriented modeling (AOM) techniques can be used to support separation of access control concerns from other application design concerns. Using an AOM approach, access control features are described by aspect models and other application features are described by a primary model. Composition of aspect and primary models yields a design model in which access control features are integrated with other application features. In this paper, we present, through an example, an AOM approach that supports verifiable composition of behaviors described in access control aspect models and primary models. Given an aspect model, a primary model, and a specified property, the composition technique produces proof obligations as the behavioral descriptions in the aspect and primary models are composed. One has to discharge the proof obligations to establish that the composed model has the specified property.