Compositional Verification of Application-Level Security Properties

Automatic model checking can be employed to verify that security properties are fulfilled by a system model. However, since security requirements constrain most, if not all, functional modules of a system, such a proof needs to consider nearly all of the system’s control and data flows. For complex real-life applications, that leads to a large state space to be explored effectively restricting the applicability of a model checker. To deal with this problem, we advocate a compositional approach utilizing the features of our model-based engineering technique SPACE. Both functional behavior and security-related aspects are specified using UML 2 activities. Further, we supplement each activity with an interface behavior description which will be extended by a security contract modeling certain security properties to be fulfilled by the activity. This enables us to verify application-level security properties by using contracts instead of their respective activities in model checker runs so that the number of states to be checked is significantly reduced. The approach is exemplified by an Android application example in which one’s location must only be shared with certain recipients.