Security@Runtime: A flexible MDE approach to enforce fine-grained security policies

in Lecture Notes in Computer Science (2014), 8364 LNCS

In this paper, we present a policy-based approach for automating the integration of security mechanisms into Java-based business applications. In particular, we introduce an expressive Domain Specific ... [more ▼]

In this paper, we present a policy-based approach for automating the integration of security mechanisms into Java-based business applications. In particular, we introduce an expressive Domain Specific modeling Language (Dsl), called Security@Runtime, for the specification of security configurations of targeted systems. The Security@Runtime Dsl supports the expression of authorization, obligation and reaction policies, covering many of the security requirements of modern applications. Security requirements specified in security configurations are enforced using an application-independent Policy Enforcement Point Pep)-Policy Decision Point (Pdp) architecture, which enables the runtime update of security requirements. Our work is evaluated using two systems and its advantages and limitations are discussed. © 2014 Springer International Publishing Switzerland. [less ▲]

A Survey of Formal Verification Techniques for Model Transformations: A Tridimensional Classification

in Journal of Technology (2014)

Towards the Formal Verification of Model Transformations: An Application to Kermeta

Doctoral thesis (2013)

Model-Driven Engineering (MDE) is becoming a popular engineering methodology for developing large-scale software applications, using models and transformations as primary principles. MDE is now being ... [more ▼]

Model-Driven Engineering (MDE) is becoming a popular engineering methodology for developing large-scale software applications, using models and transformations as primary principles. MDE is now being successfully applied to domain-specific languages (DSLs), which target a narrow subject domain like process management, telecommunication, product lines, smartphone applications among others, providing experts high-level and intuitive notations very close to their problem domain. More recently, MDE has been applied to safety-critical applications, where failure may have dramatic consequences, either in terms of economic, ecologic or human losses. These recent application domains call for more robust and more practical approaches for ensuring the correctness of models and model transformations. Testing is the most common technique used in MDE for ensuring the correctness of model transformations, a recurrent, yet unsolved problem in MDE. But testing suffers from the so-called coverage problem, which is unacceptable when safety is at stake. Rather, exhaustive coverage is required in this application domain, which means that transformation designers need to use formal analysis methods and tools to meet this requirement. Unfortunately, two factors seem to limit the use of such methods in an engineer’s daily life. First, a methodological factor, because MDE engineers rarely possess the effective knowledge for deploying formal analysis techniques in their daily life developments. Second, a practical factor, because DSLs do not necessarily have a formal explicit semantics, which is a necessary enabler for exhaustive analysis. In this thesis, we contribute to the problem of formal analysis of model transformations regarding each perspective. On the conceptual side, we propose a methodological framework for engineering verified model transformations based on current best practices. For that purpose, we identify three important dimensions: (i) the transformation being built; (ii) the properties of interest ensuring the transformation’s correctness; and finally, (iii) the verification technique that allows proving these properties with minimal effort. Finding which techniques are better suited for which kind of properties is the concern of the Computer-Aided Verification community. Consequently in this thesis, we focus on studying the relationship between transformations and properties. Our methodological framework introduces two novel notions. A transformation intent gathers all transformations sharing the same purpose, abstracting from the way the transformation is expressed. A property class captures under the same denomination all properties sharing the same form, abstracting away from their underlying property languages. The framework consists of mapping each intent with its characteristic set of property classes, meaning that for proving the correctness of a particular transformation obeying this intent, one has to prove properties of these specific classes. We illustrate the use and utility of our framework through the detailed description of five common intents in MDE, and their application to a case study drawn from the automative software domain, consisting of a chain of more than thirty transformations. On a more practical side, we study the problem of verifying DSLs whose behaviour is expressed with Kermeta. Kermeta is an object-oriented transformation framework aligned with Object Management Group standard specification MOF (Meta-Object Facility). It can be used for defining metamodels and models, as well as their behaviour. Kermeta lacks a formal semantics: we first specify such a semantics, and then choose an appropriate verification domain for handling the analysis one is interested in. Since the semantics is defined at the level of Kermeta’s transformation language itself, our work presents two interesting features: first, any DSL whose behaviour is defined using Kermeta (more precisely, any transformation defined with Kermeta) enjoys a de facto formal underground for free; second, it is easier to define appropriate abstractions for targeting specific analysis for this full-fledged semantics than defining specific semantics for each possible kind of analysis. To illustrate this point, we have selected Maude, a powerful rewriting system based on algebraic specifications equipped with model-checking and theorem-proving capabilities. Maude was chosen because its underlying formalism is close to the mathematical tools we use for specifying the formal semantics, reducing the implementation gap and consequently limiting the possible implementation mistakes. We validate our approach by illustrating behavioural properties of small, yet representative DSLs from the literature. [less ▲]

Invariant Preservation in Interative Modelling (Extended Version)

Report (2012)

A Formal Semantics of Kermeta

in Mernik, Marjan (Ed.) Formal and Practical Aspects of Domain-Specific Languages: Recent Developments (2012)

This chapter contributes to the formal specification of Kermeta, a popular metamodelling framework useful for the design of DSL structure and semantics. The formal specification is tool-/tool syntax ... [more ▼]

This chapter contributes to the formal specification of Kermeta, a popular metamodelling framework useful for the design of DSL structure and semantics. The formal specification is tool-/tool syntax independent; it only uses classical mathematical instruments taught in usual computer science courses. This specification serves as a reference specification from which specialised implementation can be derived for execution, simulation, or formal analysis of DSLs. By providing such a specification, the chapter ensures that each and every DSL written in Kermeta, receives de facto a formal counterpart, making its definition fully formal. This radically contrasts with other approaches that require a new ad hoc semantics defined for every new DSL. The chapter briefly reports on two implementations conducted to demonstrate the feasibility of the approach. [less ▲]

A Tridimensional Approach for Studying the Formal Verification of Model Transformations

in Proceedings of the First Workshop on Verification and Validation of Model Transformations (2012)