Modern software systems are increasingly complex and the environment where they operate is increasingly dynamic. The number and needs of stakeholders is also changing constantly as they need to adjust to the changing environment. A consequence of this trend is that the requirements for a software system increases and changes continually. To deal with evolution, we need analysis techniques that assess the impact of system evolution on the satisfaction of requirements such as security of the system which is very sensitive to evolution: security properties satised before evolution might no longer hold or new security properties need to be satised as result of the evolution.
Another important aspect is the change management process itself which is a major problem in practice. Changes make the traceability of requirements Work parly supported by the project EU-FP7-ICT-FET-IP-SecureChange.
hard and the monitoring of requirements unreliable: requirements management is dicult, time-consuming and error-prone when done manually. Thus, a semiautomated requirements evolution management environment, supported by a tool, will improve requirement management with respect to keeping requirements traceability consistent, realizing reliable requirements monitoring, improving the quality of the documentation, and reducing the manual eort.
In this paper we present SeCMER 4 , a tool developed in the context of the Se- cureChange European project 5 . The tool supports the dierent steps of SeCMER methodology for evolutionary requirements [4]. The methodology allows to model requirement evolution in dierent state of the art requirement languages such as SI* [6], Problem Frames (PF) [9] and SeCMER that is a requirement language that includes concepts belonging to SI*, PF and security such as asset. The methodology also supports the automatic detection of requirement changes and violation of security properties and argumentation analysis [9] to check security properties are preserved by evolution and to identify new security properties that should be taken into account. Change driven transformations based on evolution rules [3] are leveraged to check argument validity, to automatically detect violations or fullment of security properties, and to issue alerts prompting human intervention, a manual analysis or argumentation process, or trigger automated reactions in certain cases.
In the next section (2) we describe the tool architecture, then we illustrate the tool features based on an industrial example of evolution taken from the air trac management domain (3) and nally conclude the paper (4).
SeCMER is an Eclipse-based heterogeneous modeling environment for managing evolving requirements models. It has the following features (See also Fig. 1):
Modeling of Evolving Requirements. Requirement models can be drawn in SI*, Problem Frames or SeCMER. Traceability and bidirectional synchronization is supported between SeCMER and SI* requirements models.
Change detection based on evolution rules. Violations of formally dened static security properties expressed as patterns can be automatically identied. Detection of formal or informal arguments that has been invalidated by changes aecting model elements that contributed to the argument as evidence is also supported.
Argumentation-based security analysis. Reasoning about security properties satisfaction and identication of new security properties is supported. These capabilities of the tool are provided by means of the integration of a set of EMF-based [7] Eclipse plug-ins written in Java, relying on standard EMF technologies such as GMF, Xtext and EMF Transaction. 4 A detailed description of the tool implementation is reported in [5] 5 www.securechange.eu The core trigger engine plug-in oers an Eclipse extension point for dening change-driven rules. Multiple constituent plug-ins contribute extensions to register their respective set of rules. The graph pattern-based declarative event/condition feature of the rules is evaluated eciently (see measurements in [2]) by the incremental graph pattern matcher plug-ins automatically generated from the declarative description by EMF-IncQuery. At the commit phase of each EMF transaction, the rules that are found to be triggered will be executed to provide their reactions to the preceding changes. These reactions are implemented by arbitrary Java code, and they are allowed to modify the model as well (wrapped in nested transactions) and could therefore be reacted upon.
So far, there are three groups of change-driven rules as extension points: transformation rules that realize the on-the-y synchronization between multiple modeling formalisms, security-specic evolution rules that detect the appearance of undesired security patterns, raise alerts and optionally oer candidate solutions. rules for invalidating arguments when their ground facts change.
A major feature is the a bi-directional synchronizing transformation between Si* and the SeCMER model with changes propagated on the y, interactively. Since the languages have dierent expressive power, the following challenges arise:
1. some concepts are not mapped from one formalism to the other or vice versa, some model elements may be mapped into multiple (even an unbounded amount of ) corresponding model elements in the other formalism, and nally 3. it is possible that a single model element has multiple possible translations (due to the source formalism being more abstract); one of them is created as a default choice, but it can later be changed to the other options, which are also tolerated by the transformation system.
We are going to illustrate the features supported by our prototype using the ongoing evolution of ATM systems as planned by the ATM 2000+ Strategic Agenda [1] and the SESAR Initiative. Part of ATM system's evolution process is the introduction of the Arrival Manager (AMAN), which is an aircraft arrival sequencing tool to help manage and better organize the air trac ow in the approach phase. The introduction of the AMAN requires new operational procedures and functions that are supported by a new information management system for the whole ATM, an IP based data transport network called System Wide Information Management (SWIM) that will replace the current point to point communication systems with a ground/ground data sharing network which connects all the principal actors involved in the Airports Management and the Area Control Centers.
The entities involved in the simple scenario used for this demo are the AMAN, the Meteo Data Center (MDC), the SWIM-Box and the SWIM-Network. The SWIM-Box is the core of the SWIM information management system which provides access via dened services to data that belong to dierent domain such as ight, surveillance, meteo, etc. The introduction of the SWIM requires suitable security properties to be satised: we will show how to protect information access on meteo data and how to ensure integrity of meteo data.
1. Requirements evolution. We show how SeCMER supports the representation of the evolution of the requirement model as eect of the introduction of the SWIM. 3. Argumentation-based security analysis. We show how argumentation analysis [9] can be carried to provide evidence that the information access property applied to the meteo data is satised after evolution. Detecting violations of security properties based on security patterns. SeCMER includes facilities that allow for the declarative denition of security patterns that express situations that leads to the violation of a security property. For example, if a concerned actor wants a security goal that expresses that a resource must be protected, then each actor that the resource is delegated to must be trusted (possibly transitively) by the concerned actor. An exception is made if a trusted actor performs an action to explicitly fulll the security goal, e.g. digital signature makes the trusted path unneccessary in case of an integrity goal. See Lst. 1 for the denition of the pattern using the declarative model query language of EMF-IncQuery [2].
According to this pattern the integrity property for MD is violated because AMAN entrusts MDC with the integrity security goal, but the communitation intermediary actors SWIMBox_MDC, and SWIMBox_AMAN are not.
Lst. 1 can be used to dene evolution rules that dene automated corrective actions to be applied to the model in order to re-establish the integrity security property. Possibile examples of corrective actions are: Add a trust relationship between MDC and SWIM Network having the integrity security goal as dependum.
Alternatively, an Action such as MD is digitally signed can be created to protect the integrity of MD even when handled by untrusted actors. The diagram says that the AMAN system is claimed to be secure before the change (Round #1), and the claim is warranted by be the facts the system is known to be a close system (F1), and the physical location of the system is protected (F2). This argument is rebutted in Round #2, in which another argument claims that the system is no longer secure because SWIM will not keep AMAN closed. The rebuttal argument is mitigated in Round #3 by three arguments, which suggest that the AMAN may still be secure given that the physical infrastructure is secure, personnel are trustworthy and access to data is controlled.
The paper presented SeCMER, a tool for managing evolving requirements. As shown by the ATM-based demo scenario, the tool supports visual modeling of security requirements. Additionally, argument models can be constructed manually to investigate the satisfaction of security properties; the tool detects invalidated arguments if the requirements model evolves. Finally, the tool performs continuous and automatic pattern-based security properties violation detection, with quick x corrective actions specied by evolution rules.
We are planning to extend the tool in order to support other set of security patterns and evolution rules to automate the detection and handling of security violations in a wider range of application scenarios. We will also realize a tighter integration with additional modeling formalisms (Problem Frames ) and industrial tools e.g DOORS-TREK. The usability and the features of the tool are going to be evaluated through a study involving ATM-domain experts.