WP5: ASSERT-M: Model based certificate

WP Leader: Fraunhofer SIT

This work package focuses on the structure and handling of ASSERT4SOA model based certificates. These ASSERT–M certificates will contain information concerning the formal model of the certified service or service based system (SBS), the security properties provided, and information related to the verification performed during the certification process in order to verify these security properties. ASSERT–M certificates will enable a service consumer to assess the assurance level provided by the certificate for a specific service with respect to their own security policy. They will further enable him/her to analyse the impact of security properties of services integrated into a system with respect to the security properties of the overall system, and to relate formal models of SBS being composed of different sets of services, thus supporting service orchestration (to be handled in work package WP2).

In order to achieve the above objectives, this work package will develop methods to model an SBS as a composition of the formal models of the integrated services. Further, we will develop methods to characterize in which cases models of an SBS containing different sets of services provide / do not provide the same security properties. From this, patterns of models will be derived that reflect different possibilities of service composition for an SBS that provide the same security property. In order to specify security properties in ASSERT–M certificates, a formal language for security properties will be developed that reflects the SBS's model being
a composition of the service models. Another part of the work in WP5 concerns to define the model based certification artefacts. More specifically, we will define how to specify models of services and service based systems, security properties provided, and relevant information with respect to the verification having been performed (attack models, assumptions on the environment, etc.). A third major part in this work package is concerned with the establishment of a two–dimensional partial order of ASSERT–M certificates, and with algorithms and techniques using this partial order for checking compliance of a model based certificate with respect to an assurance level or policy involving a set of desired security properties.

Task 5.1: Formal Models and their Composition for Certification Support (Leader: SIT, M1-M9):
The work in WP5 will start with investigating current certification processes being based on formal models with the aim to facilitate the integration of current certification processes into ASSERT4SOA methods. Taking this into account, we will develop appropriate formal model representations of service based systems as a composition of the models of the integrated services. These models can be based for example on a specification of the sequences of actions, specific actions serving as interfaces between services and system. An important aspect of this task is that its results can be integrated into state–of–the–art modelling techniques. Model composition will then be the basis for defining and relating model “patterns” of service based systems that integrate different sets of services. This includes to identify characteristics of changes in a system model that do / do not preserve its security properties. Relations between formal models can be established for example by mappings between the models satisfying specific conditions. These methods will support the analysis of how e.g. exchanging one service for another impacts the overall system's security properties and will be input for the work on service orchestration both at design time (Task 2.2) and at run time (Task 2.3).

Task 5.2: Security Property Language (Leader: UMA, M1-M24):
In order to express the security properties of services and SBS, a language for security properties will be developed. This language must meet the following requirements: It must (i) allow rich and detailed expression of the semantics of each property; (ii) enable the reasoning and the production of formal proofs of relations between security properties (see Task 5.4 below), hence it must be based on a formal semantics; (iii) it must provide sufficient flexibility to capture the properties relevant for ASSERT-M certificates; and (iv) it must enable security properties of an SBS to be derived from the security properties of its integrated services. The security property concepts defined in this task will be input for the design and development of the certificate ontology inTask 3.2.

Task 5.3: Model Based Certification Artifacts (Leader: SIT, M10-M24):
This task is concerned with the development of methods for capturing model patterns and security properties as defined in Tasks 5.1 and 5.2 in ASSERT–M certificates. Further work will concern the concepts for capturing the essential information with respect to the verification method having been applied during the certification process, and its results. This includes to specify the verification method itself (e.g. model checking using a specific approach), the attack model (based on the service/SBS model extended by attack behaviour), and the assumptions on the environment (i.e., security properties that the environment must satisfy). These concepts will be input for the definition of an ontology for ASSERT–M certificates to be carried out in WP3.A challenging question in this context is to which extend the generation of an ASSERT-M certificate for an SBS can be supported by ASSERT-M certificates for the integrated services Using ASSERT–M artefacts, algorithms and techniques will then be designed and developed for checking compliance of an ASSERT–M certificate with respect to an assurance level or policy involving a set of desired security properties. A proof–of–concept
implementation to be carried out independently of the framework activities in WP6 will validate the results of this task.

Task 5.4: Establishing a Partial Order on ASSERT-M Certificates (Leader: SIT, M16-M30):
The partial order to be established has two dimensions: For the first one we will use, gradually as they become available, the results obtained in Task 5.2 concerning security properties in order to prove relations between properties (e.g. with respect to their strength). The second dimension is related to the verification methods and results used during the certification process. These can be related to each other for example in terms of attack models used (the more powerful the attacker the stronger the result), and to assumptions used within mathematical proves and for model checking (the fewer assumptions the stronger the proof). One of the
research challenges will be to elaborate if and how different verification methods can be related.

Task 5.5: Validation of WP5 Methods and Techniques (Leader: SIT, M22-M36):
In this task we will apply the methods developed in the previous tasks gradually as they become available to the concrete case study to be defined in WP7, using state-of-the-art modeling techniques (such as UML, BPEL). Certificates for different versions of the case study scenario, composed of different sets of services, will be specified and, based on these, the impact of service exchange on the overall security of the scenario will be analysed.

template joomla