Section: New Results

Practical applications

Security policies specification and analysis

Participants : Tony Bourdier, Horatiu Cirstea, Hélène Kirchner, Pierre-Etienne Moreau.

Access control policies, a particular case of security policies should guarantee that information can be accessed only by authorized users and thus prevent all information leakage. We proposed [18] a framework where the security policies and the systems they are applied on are specified separately but using a common formalism. This separation allows not only some analysis of the policy independently of the target system but also the application of a given policy on different systems. In this framework, we propose a method to check properties like confidentiality, integrity or confinement over secure systems based on different policy specifications.

We also propose an approach [12] where the specification of a security policy is split into two distinct elements: a security model and a configuration. The security model (expressed as an equational problem) describes how authorization requests must be evaluated depending on security information. The configuration (expressed as a rewriting system) assigns values to security information. We show that this separation eases the formal analysis of security policies and makes it possible to automatically convert a given policy with respect to an alternative security model.

Symbolic analysis of network security policies

Participants : Tony Bourdier, Horatiu Cirstea.

In computer networks, security policies are generally implemented by firewalls. We propose in [16] an original framework based on tree automata which can be used to specify firewalls and which takes into account the network address translation functionality. We show that this framework allows us to perform structural analysis as well as query analysis and comparisons over firewall policies.

We have extended the above formalism to take into account the composition of firewalls. In our approach [17] all the components of a firewall, i.e. filtering and translation rules, are specified as rewrite systems. The same formalism can be used to formally describe the composition of firewalls (including routing) in order to build a whole network security policy. The properties of the obtained rewrite systems are strongly related to the properties of the specified networks and thus, classical theoretical and practical tools can be used to obtain relevant properties of the security policies. We showed that the proposed specifications allow us to handle usual problems such as comparison, structural analysis, and query analysis over complete networks.

Model transformation using rewriting

Participants : Jean-Christophe Bach, Pierre-Etienne Moreau.

New development chains of critical systems rely on Domain Specific Modeling Languages (DSML) and on qualifiable transformations (insurance that a transformation preserves interesting properties). To specify and to make such transformations we have started to extend Tom.

A first part of this extension is an EMF (Eclipse Modeling Framework, http://www.eclipse.org/modeling/emf/ ) mapping generator which allows to use Tom with EMF. The idea of this tool is to generate Tom mappings (i.e. an algebraic view) by introspecting EMF generated Java code. These mappings can then be used to describe transformations of models that have been created in Eclipse. Tom-EMF is documented and available in the Tom source distribution.

The second part of this extension consists in the addition of new Tom language constructs to express transformations of models. Studying several use cases(available on the Quarteft subversion repository: https://gforge.enseeiht.fr/projects/quarteft/ ), we have already handwritten the code that should be generated. We are currently considering abstraction of the code in order to make the generation of this one automatic in a near future.

A constraint language for algebraic terms

Participants : Horatiu Cirstea, Pierre-Etienne Moreau, François Prugniel.

With the development of model transformation formalisms and tools, a need for checking the result of transformations appears. For UML, the Object Management Group developed OCL(Object Constraint Language, http://www.omg.org/spec/OCL/2.2/ ) but there are no equivalent formalisms for the algebraic views of models used in Tom-EMF. Starting from the OCL experiences, we have proposed an extension of Tom with a constraint language for algebraic signatures [23] .

We show that the constructs of this new constraint language inspired from OCL and XPath can be naturally described using strategic rewriting and consequently, constraint checking can be performed by executing Tom programs. This kind of language is a major asset for debugging tools and a great step to obtain trustworthy compilers. Indeed, the first important application for this language will be the Tom compiler itself.