<figure><img src="image_1.png" /></figure>

HAL
open science

Formal Model Driven Engineering

Akram Idani

► To cite this version:

Akram Idani. Formal Model Driven Engineering. Computer Science [cs]. Université Grenoble - Alpes, 2023. tel-04313622

HAL Id: tel-04313622

https://theses.hal.science/tel-04313622

Submitted on 29 Nov 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

Public Domain
<figure><img src="image_2.png" /></figure>

Communauté

UNIVERSITÉ Grenoble Alpes

# Thèse d'Habilitation à Diriger des Recherches

Spécialité : Informatique

Présentée par

Akram IDANI

Laboratoire d'Informatique de Grenoble

École Doctorale Mathématiques, Sciences et technologies de l'information, Informatique

# Formal Model Driven Engineering

# Ingénierie Formelle Dirigée par les Modèles

Soutenue publiquement le **26 Mai 2023**,
devant le jury composé de :

Rapporteur.e.s

**Mme, Catherine Dubois**

Professeure, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), France

**M., Pierre-Yves Schobbens**

Professeur, Université de Namur, Belgique

**Mme, Virginie Wiels**

Directrice de Recherche, Office national d'études et de recherches aérospatiales (ONERA), France

Examinateur.rice.s

**Mme, Sophie Dupuy-Chessa**

Professeure, Université Grenoble Alpes, France

**Mme, Régine Laleau**

Professeure, Université Paris-Est Créteil, France

**M., Michael Leuschel**

Professeur, Heinrich-Heine-Universität Düsseldorf, Allemagne

<figure><img src="image_3.png" /></figure>
@PhdThesis{hdr-idani,
  author = {Akram Idani},
  title = {Formal Model Driven Engineering},
  school = {Université Grenoble Alpes},
  year = {2023},
  type = {Habilitation à Diriger des Recherches (HDR)},
  address = {LIG},
}
باسم الله الرحمان الرحيم

« Le secret... de l'expression et du message, consiste à communiquer des idées.
Sans transmission de la pensée, le langage n'est qu'une terre morte. »

Ibn Khaldoun (Prolégomènes, 1377)

à mes ancêtres et leur descendance ...

à mes parents et mes enfants ...

à mon frère et à ma soeur ...

...

à mon étoile, à la belle sirène et aux airs de guitare !
<figure><img src="image_4.png" /></figure>
Remerciements

Toutes les personnes m'ayant permis de mener à bien ce travail sont assurées de ma gratitude :
« Grâce à vous ce qui n'était qu'une question de recherche est devenu une passion ».

***

À mon collègue, chef d'équipe et directeur de thèse, Yves Ledru : « Je t'adresse, en signe de reconnaissance, mes plus vifs remerciements pour ta gentillesse et ton soutien. Tu as manifesté à mon égard de bienveillants conseils tout au long de mon parcours ».

À mon collègue, German Vega, Ingénieur de Recherche au CNRS : « J'exprime mes sincères remerciements pour tous les échanges qu'on a pu avoir et qui ont permis d'élaborer le cadre applicatif de mes travaux. Sans toi les outils B4MSecure et Meeduse seraient restés à un état embryonnaire. J'espère que tu trouveras ici l'expression de ma gratitude et de ma grande estime pour ta personne, ainsi que ma profonde considération pour ta compétence professionnelle ».

***

Il n'est pas aisé, en quelques lignes, de remercier toutes les personnes ayant permis à ce
modeste travail de prendre forme. C'est grâce aux collègues, étudiants, amis et proches que
ce travail est ce qu'il est aujourd'hui. Ce mémoire est une synthèse d'une dizaine d'années de
recherches durant lesquelles j'ai fait des rencontres riches qui ont forgé ma pensée scientifique
et qui ont contribué à la maturité de mes réflexions.

C'est avec reconnaissance et sincérité que je remercie les membres du jury pour leur travail d'évaluation. Je remercie vivement Catherine Dubois, Virginie Wiels et Pierre-Yves Schobbens, pour leurs judicieux commentaires et leurs remarques et critiques très constructives. Je remercie aussi Sophie Dupuy-Chessa, Régine Laleau et Michael Leuschel qui m'ont fait l'honneur d'examiner ce travail : « Votre regard avisé sur les nombreux sujets traités dans ce mémoire est fort utile pour moi car il constitue un guide pour mes recherches futures ».

Merci particulièrement à mes collègues du LIG, de l'UGA et de Grenoble INP. Je ne saurais
les citer tous en cette page. Grâce à leur bonne humeur et à l'ambiance chaleureuse j'ai agréable-
ment effectué mon travail et mené une carrière d'enseignant-chercheur épanouissante.

Il ne fait aucun doute que mes travaux se sont enrichis au fil des années des nombreux
échanges que j'ai eus avec mes collègues, mais aussi avec les jeunes étudiants-chercheurs
en master et en thèse. Je tiens à les remercier très sincèrement pour avoir contribué à mes
recherches. Je témoigne ici de leur mérite et je leur souhaite un avenir plein de succès.

Finalement, je tiens à souligner que ce travail est aussi le fruit d'encouragements et de
bienveillance de la part de mes ami(e)s : « Votre bonté sincère et générosité inconditionnelle
font de vous des personnes exceptionnelles. ».

***
<figure><img src="image_5.png" /></figure>
# Outline

## Introduction 1

# I Formal Modeling of Secure Information Systems 15

## Chapter 1 A Model-Driven Architecture for UML-to-B 17

1.1 Brief overview of the B method 19

1.1.1 Abstract machines 19

1.1.2 Structured developments 20

1.1.3 Generalized substitutions 21

1.1.4 Illustration 23

1.2 A quick survey of UML-to-B techniques 25

1.2.1 Existing approaches 25

1.2.2 Application 26

1.2.3 Discussion 26

1.3 Towards a unifying method integration approach 28

1.3.1 Model driven engineering and method integration 28

1.3.2 The proposed model driven architecture 29

1.3.3 A meta-model for the B method 30

1.4 Multiple transformations 33

1.4.1 A meta-model for configurable transformations 33

1.4.2 Transformation process and phasing 35

1.4.3 Abstraction levels 36

1.4.4 Transformation rules 37

1.4.5 Application 39

1.5 Conclusion 40
Chapter 2 Formal Model-Driven Security 43

<table><tr><td>2.1</td><td>Role-Based Access Control (RBAC)</td><td>46</td></tr><tr><td>2.1.1</td><td>Main concepts</td><td>46</td></tr><tr><td>2.1.2</td><td>Modeling RBAC with SecureUML</td><td>47</td></tr><tr><td>2.1.3</td><td>V&amp;V of RBAC policies</td><td>48</td></tr><tr><td>2.1.4</td><td>Discussion</td><td>51</td></tr><tr><td>2.2</td><td>B4MSecure</td><td>52</td></tr><tr><td>2.2.1</td><td>Overview</td><td>52</td></tr><tr><td>2.2.2</td><td>Functional model</td><td>54</td></tr><tr><td>2.2.3</td><td>Security model</td><td>58</td></tr><tr><td>2.3</td><td>Animation and dynamic analyses</td><td>66</td></tr><tr><td>2.3.1</td><td>Animation in B4MSecure</td><td>66</td></tr><tr><td>2.3.2</td><td>Testing the security policy</td><td>67</td></tr><tr><td>2.3.3</td><td>Attack scenarios</td><td>69</td></tr><tr><td>2.4</td><td>Discussion and conclusion</td><td>71</td></tr></table>

Chapter 3 Looking for malicious behaviours 75

<table><tr><td>3.1</td><td>Running Example</td><td>76</td></tr><tr><td>3.1.1</td><td>Functional model</td><td>76</td></tr><tr><td>3.1.2</td><td>Access control rules</td><td>76</td></tr><tr><td>3.1.3</td><td>Validation</td><td>77</td></tr><tr><td>3.2</td><td>Dynamic analysis</td><td>78</td></tr><tr><td>3.2.1</td><td>Trace Semantics for B Specifications</td><td>78</td></tr><tr><td>3.2.2</td><td>Tools to exhibit behaviours from B specifications</td><td>79</td></tr><tr><td>3.2.3</td><td>Malicious Behaviour</td><td>81</td></tr><tr><td>3.3</td><td>Symbolic Search</td><td>83</td></tr><tr><td>3.3.1</td><td>Termination</td><td>83</td></tr><tr><td>3.3.2</td><td>Completeness</td><td>84</td></tr><tr><td>3.3.3</td><td>Step by Step Illustration</td><td>85</td></tr><tr><td>3.3.4</td><td>Application</td><td>86</td></tr><tr><td>3.3.5</td><td>Discussion</td><td>89</td></tr><tr><td>3.4</td><td>Related Work</td><td>90</td></tr><tr><td>3.5</td><td>Conclusion</td><td>92</td></tr></table>
## II Building correct DSLs

93

## Chapter 4 Formal Model-Driven Executable DSLs

95

<table><tr><td>4.1</td><td>DS(M)L's semantics</td><td>97</td></tr><tr><td>4.1.1</td><td>Abstract syntax and semantic domains</td><td>97</td></tr><tr><td>4.1.2</td><td>Dynamic semantics vs Behavioural semantics</td><td>98</td></tr><tr><td>4.1.3</td><td>Executable DS(M)Ls in Meeduse</td><td>99</td></tr><tr><td>4.2</td><td>Preliminary study and critical review</td><td>101</td></tr><tr><td>4.2.1</td><td>A simplified Petri-net DSL</td><td>101</td></tr><tr><td>4.2.2</td><td>Ascertainment and discussion</td><td>104</td></tr><tr><td>4.3</td><td>A Formal Model-Driven Petri-net DSL</td><td>107</td></tr><tr><td>4.3.1</td><td>Static semantics</td><td>107</td></tr><tr><td>4.3.2</td><td>Modeling operations</td><td>108</td></tr><tr><td>4.3.3</td><td>Operational semantics</td><td>109</td></tr><tr><td>4.3.4</td><td>Semantics coordination</td><td>112</td></tr><tr><td>4.4</td><td>Debugging with PNet<sub>Reference</sub></td><td>114</td></tr><tr><td>4.4.1</td><td>Mutual exclusion</td><td>115</td></tr><tr><td>4.4.2</td><td>Fairness</td><td>115</td></tr><tr><td>4.5</td><td>Conclusion</td><td>117</td></tr></table>

## Chapter 5 Applications and case studies

119

<table><tr><td>5.1</td><td>Application 1: Petri-net Markup Language</td><td>121</td></tr><tr><td>5.1.1</td><td>PNML</td><td>121</td></tr><tr><td>5.1.2</td><td>The PNML Meta-model</td><td>122</td></tr><tr><td>5.1.3</td><td>Formal static semantics</td><td>123</td></tr><tr><td>5.1.4</td><td>Operational semantics</td><td>125</td></tr><tr><td>5.1.5</td><td>MeeNET</td><td>127</td></tr><tr><td>5.2</td><td>Application 2: Railway systems</td><td>129</td></tr><tr><td>5.2.1</td><td>ERTMS/ETCS Case Study</td><td>130</td></tr><tr><td>5.2.2</td><td>Coloured Petri-nets</td><td>131</td></tr><tr><td>5.2.3</td><td>A Railway DSL for ERTMS/ETCS</td><td>134</td></tr><tr><td>5.2.4</td><td>Putting it all together</td><td>137</td></tr><tr><td>5.2.5</td><td>Refinements</td><td>139</td></tr><tr><td>5.3</td><td>Application 3: Model transformation</td><td>140</td></tr><tr><td>5.3.1</td><td>Step 1: merging meta-models</td><td>141</td></tr></table>
<table><tr><td>5.3.2 Step 2: generation of the “model construction” specification</td><td>142</td></tr><tr><td>5.3.3 Step 3: writing the transformation rules</td><td>143</td></tr><tr><td>5.3.4 Step 4: animation and debugging</td><td>145</td></tr><tr><td>5.3.5 Step 5: Proving the transformation</td><td>146</td></tr><tr><td>5.3.6 Discussion</td><td>147</td></tr><tr><td>5.3.7 The TTC’2019 Case Study</td><td>148</td></tr><tr><td>Conclusion and perspectives</td><td>151</td></tr><tr><td>Bibliography</td><td>159</td></tr></table>
# Introduction

La notion d'abstrait est comprise comme ce qui est flou, pas clair,
pas ou peu compréhensible, peu ou pas accessible.
En fait, l'abstrait est ce qui est virtuel, conceptualisé.
C'est l'univers mental, les pensées, les idées, les productions
de cette aptitude à faire des concepts à partir
de mes sensations, de mes émotions, ou de mes intuitions.

L. Martinez

## Preamble

My research works are dedicated to the integration of two well known paradigms: Formal Methods (FM) and Model-Driven Engineering (MDE). This integration is called Formal MDE (FMDE) all along the current document. In fact, several works have been already done in order to strengthen the MDE paradigm with formal reasoning, and therefore make it more viable as far as safety and security concerns have to be addressed. When taken separately, these works provide a partial coverage of MDE, but when combined they can address a wide range of models and languages. During the last decade, I investigated two directions in which the FMDE paradigm proved its value: (i) Model-Driven Security (MDS), and (ii) Domain-Specific Languages (DSLs). Under the MDE umbrella, both the MDS and DSL communities advocate for the use of models throughout the development process, providing solutions to the validation problem ('do the right system'). Nonetheless, the verification problem ('do the system right') is still a major challenge, perhaps because formal reasoning (i.e. model-checking and/or theorem proving) was not apart of the MDE initiative. To be pragmatic my contributions build on well-established notations: mainly UML and B, and — at a smaller scale — BPMN, CSP, Z and Petri-Nets. Besides, the obtained results can be inspiring and, in my opinion, should be extended with other approved (semi-)formal languages, which would confer to FMDE a broader spectrum. The next two sections (A. and B.) summarize for every research direction (respectively MDS and DSLs) the challenges that guided my works, and give an overview of my contributions and publications in the field.
# A. Model-Driven Security

## A.1. Challenges

Computer security often refers to hackers or intruders, who are persons with high technical skills and whose intention is to exploit security breaches in order to get an illegal access to a system. However, in reality the greatest threats come from inside the system, i.e. from trusted users who are already granted a legal access. This kind of threat is called “insider attack” in cyber-security and it is known to be difficult to tackle (Probst et al., 2010). Studies done by IBM X-Force Research in the cyber-security landscape state that: “In 2015, 60 percent of all attacks were carried out by insiders [...] and they resulted in substantial financial and reputational losses”. The problem is beyond the access control frontier since it includes unpredictable human behaviours. To deal with these threats, existing industrial, academic and government studies (Kont et al., 2018, Greitzer, 2019, Homoliak et al., 2019) elaborate human profiles and advocate for the use of surveillance systems. Without being exhaustive, some of these profiles are:

* Curious persons who, without a malicious intention but without self-control too, get access to sensitive data or do some actions that are in contradiction with the company rules.

* Super-heroes who, in order to fix a problem or help someone, bypass the company policies believing that it may be useful or simply be approved.

* Audacious persons who, in order to prove their strength (most of the time to them-selves), secretly get access to private information available in the company network.

Other profiles are established in the literature, like machiavellian, greedy, disgruntled, opportunistic, etc. Unfortunately, the eventuality of a breach of trust is difficult to predict in advance based on human-centric factors. On the one hand there is no certainty about a possible acting out, and on the other hand people surveillance must comply with privacy legislation, which makes it almost ineffective. Nonetheless, Information Systems (IS) together with their business logic and processes, provide useful knowledge allowing one to deal with the insider threat problem. In fact, based on the aforementioned studies it can be observed that insiders often do not have high computer skills (contrary to intruders), but they have a fine-grained knowledge about the IS procedures. The latter are mostly well-established and already protected via access control mechanisms. Hence, by being able to answer the question “who has access to sensitive data and what kind of access is given?”, one cannot claim that the system is secure enough. The good question should be: “is the user able to run a sequence of actions that may bring him from a prohibition to an authorization?”. The first question refers to static concerns, and it is widely addressed in Model-Driven Security (MDS) thanks to several access control models (SecureUML, UMLSec, etc). However, the second question remains open in MDS because it refers to behavioural features and the reachability of unwanted situations granting to the user misappropriated privileges.
## A.2. Contributions

I contributed toward MDS through a FMDE approach covering structural and behavioural features of secure IS, and addressing their validation against insider threats. The proposed security-by-design technique builds on the strengths of UML, SecureUML (a UML profile for access control) and formal languages (B (Abrial, 1996) and Z). The aim is to combine graphical views and automated reasoning during the IS development. This research began in 2008 in the context of the ANR-Selkis project<fnref n="1" /> and has been the subject of several PhD and master projects that I (co-)supervised. To summarize, my contributions can be separated in two major axes: Modeling, and Analysis.

### A.2.1 Axis 1: Modeling

Separation of concerns is a core technique in MDS (Basin et al., 2011), since MDS means “ap-
plying the concepts behind model-driven software development to security”. It has been pro-
posed to master the complexity of the IS by distinguishing its functional concerns (data model
and the associated business logic) from high-level ACIT properties (Availability, Confidential-
ity, Integrity, Traceability). In order to guarantee a security-by-design approach in which the
MDS benefits from an automated formal support, my works first apply UML and SecureUML
to represent both functional and security concerns, and then suggest their translation into B and
Z. I co-supervised two PhD students on this topic: M.-A. Labiadh and N. Qamar. The research
work of M.-A. Labiadh was built on the B method, and proposed configurable transformations
allowing one to mix several transformation approaches. Regarding the work of N. Qamar, it
applied a direct translation using RoZ, a tool by Ledru (2006) whose aim is to extract Z speci-
fications from UML class diagrams. Both techniques are complementary and provide together
a good coverage of MDS. In the remainder I will focus on the usage of the B method, mainly
because it is a backbone of my current and further works in FMDE.

**Functional models.** The extraction of B specifications from UML models is not a new topic; it was widely investigated between 2002 and 2006 resulting in a rich state of the art. However, an exhaustive analysis of the existing approaches shows that each kind of UML-to-B mapping has its specific objectives and characteristics and, except iUML-B by Snook and Butler (2006a), a major issue is that tools are either obsolete or not publicly available. Thus, to be applied in MDS efforts have been done to polish, adapt, extend and combine those works in a usable framework. The proposal done in the work of M.-A. Labiadh is to make the UML-to-B mappings as parametric as possible, such that the user can easily manage the transformation rules and experiment various solutions.

**Security models.** Regarding the translation of SecureUML, it has been built on formal defi-
nitions of the Role-Based Access Control model (RBAC). RBAC is supported by several soft-
ware products like popular commercial database management systems (e.g. Oracle, Sybase) or

<footnote n="1">¹ ANR-08-SEGI-018, 20012–2018.</footnote>
webservers (e.g. JBoss). The available implementations of this model act like a filter which intercepts a user request to a resource in order to permit or deny the access to associated functional actions (e.g. transactions on databases, file operations, etc). The thesis of M.-A. Labiadh followed a similar principle, but at a modeling stage, leading to the extraction of RBAC filters written in B, and in which permissions/prohibitions are defined as security guards.

**Business process models.** Another important pillar of an IS, in addition to its functional and security concerns, is to perform established processes that are followed by the stakeholders during their working activities. A business process model represents a set of steps undertaken for a specific purpose in which intrinsically operations concerning the IS data (like reading, modification, etc.) and responsibilities for performing tasks are defined. The three concerns (functional models, security policies and business processes) are important; their alignment is useful to address several inconsistencies, such as when the access control policy gives more permissions than the actions required by the business process. In this case following the process may hide several authorizations giving the impression that some bad actions are not possible while they can still be done from outside the process, which is a typical example of insider attacks. This topic was addressed in the PhD of S. Chehida, and by two master 2 students during their trainees. It also led to an established collaboration with the SIGMA team from the LIG lab, with local fundings. The objective is to align the three models and provide a technique to verify the correctness of this alignment using B.

### A.2.2 Axis 2: Analysis

A direct consequence of the separation of concerns principle is that functional and security models are often validated separately. Existing works in MDS are therefore stateless and they mostly validate security policies statically without taking into account the dynamic evolution of the IS. Nonetheless, authorized actions often lead to evolutions of the functional state, which may influence the security behaviour and favour insider threats. A well known insider attack which was possible due to evolutions of the functional state is that of 'Société Générale', perpetrated by Jérôme Kerviel. This attack resulted in a net loss of $7.2 billion to the bank<fnref n="2" />. The insider circumvented internal security mechanisms to place more than $70 billion in secret, unauthorized derivatives trades. Through authorized actions, he was able to cover up operations he has made on the market by introducing into the functional system fictive offsetting inverse operations, so that the unauthorized trades were not detected. Dynamic analysis based on reachability properties is therefore crucial because it would establish that a system evolves as expected and that unwanted situations are not possible.

By using B and its composition mechanism, my works provide a way to take into account the intertwining of security policies and functional concerns of the IS. The underlying analysis techniques are intended to verify whether a given targeted functional state is reachable, and eliminate threats by proving that a given unwanted state is unreachable. Since an (un)wanted

<footnote n="2">² The New York Times. French Bank Says Rogue Trader Lost $7 Billion. January 2008.</footnote>
state can be formally characterized with a predicate *P*, then one can assume that insider threats start from an initial normal situation where *P* is false, and may occur if it is possible to exhibit a sequence of *B* operations, whose security guards are true, and leading to a state where *P* holds. The solutions I investigated build on two strategies: forward search and backward search.

**Forward search.** Forward search is a classical approach that is often done thanks to model-checking techniques, but it is more efficient for relatively small applications. As this is not always possible in the case of IS, a model-checker may require some guidance. To this purpose I investigated, on the one hand, process-based search applying CSP||B (Butler and Leuschel, 2005); and on the other hand, an original optimisation technique built on a variant of the ant colony algorithm (Merkle and Middendorf, 2006). This part of the work was developed in collaboration with students from the master 2 MoSIG, and two ENSIMAG students during the teaching unit "Initiation à la recherche en laboratoire".

**Backward search.** Backward search starts from the unwanted state and tries to go back to a normal situation. In other words it starts by qualifying the attack (*P*) and then looks at the authorized operations, called critical, that reach *P* from $\neg P$. Hence, rather than looking for one unwanted state (like in forward search), the technique considers that every precondition of every critical operation is itself an unwanted state. This topic was addressed during the thesis of A. Radhouani, leading to the development of the GenISIS tool (Generator of Insider Scenarios in Information Systems). The tool provides a symbolic backward search applying both theorem proving and constraint solving approaches.

## A.3. Main publications

Akram Idani and Mario Cortes Cornax. Towards a model driven formal approach for merging data, access control and business processes. In *2nd International Workshop on Security for and by Model-Driven Engineering (SecureMDE). MODELS'20 Companion Proceedings*, pages 57:1–57:5. ACM, 2020. doi: 10.1145/3417990.3420046.

Yves Ledru, Akram Idani, Rahma Ben Ayed, Abderrahim Ait Wakrime, and Philippe Bon. A separation of concerns approach for the verified modelling of railway signalling rules. In *Third International Conference on Reliability, Safety, and Security of Railway Systems - Modelling, Analysis, Verification, and Certification (RSSRail)*, volume 11495 of LNCS, pages 173–190. Springer, 2019. doi: 10.1007/978-3-030-18744-6\_11.

Akram Idani. Model driven secure web applications: the SeWAT platform. In *5th European Conference on the Engineering of Computer-Based Systems, ECBS 2017*, pages 3:1–3:9. ACM, 2017. doi: 10.1145/3123779.3123800.

Salim Chehida, Akram Idani, Yves Ledru, and Mustapha Kamel Rahmouni. Combining UML and B for the specification and validation of RBAC policies in business process activities. In
10th IEEE International Conference on Research Challenges in Information Science, RCIS, pages 1–12. IEEE, 2016. doi: 10.1109/RCIS.2016.7549284.

Amira Radhouani, Akram Idani, Yves Ledru, and Narjes Ben Rajeb. Symbolic Search of Insider Attack Scenarios from a Formal Information System Modeling. LNCS Transactions on Petri Nets and Other Models of Concurrency, 10:131–152, 2015. doi: 10.1007/978-3-662-48650-4\_7.

Yves Ledru, Akram Idani, Jérémy Milhau, Nafees Qamar, Régine Laleau, Jean-Luc Richier, and Mohamed-Amine Labiadh. Validation of IS security policies featuring authorisation constraints. International Journal of Information System Modeling and Design (IJISMD), 6 (1), 2015a.

Akram Idani and Yves Ledru. B for Modeling Secure Information Systems - The B4MSecure Platform. In 17th International Conference on Formal Engineering Methods, ICFEM, volume 9407 of LNCS, pages 312–318. Springer, 2015. doi: 10.1007/978-3-319-25423-4\_20.

Yves Ledru, Akram Idani, and Jean-Luc Richier. Validation of a security policy by the test of its formal B specification - A case study. In 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, FormaliSE’15, pages 6–12. IEEE Computer Society, 2015b. doi: 10.1109/FormaliSE.2015.9.

Amira Radhouani, Akram Idani, Yves Ledru, and Narjes Ben Rajeb. Extraction of insider attack scenarios from a formal Information System Modeling. In 5th International Workshop on Formal Methods for Security (FMS), 2014.

Jérémy Milhau, Akram Idani, Régine Laleau, Mohamed-Amine Labiadh, Yves Ledru, and Marc Frappier. Combining UML, ASTD and B for the formal specification of an access control filter. International Journal on Innovations in Systems and Software Engineering (ISSE), 7 (4):303–313, 2011. doi: 10.1007/s11334-011-0166-z.

Yves Ledru, Nafees Qamar, Akram Idani, Jean-Luc Richier, and Mohamed-Amine Labiadh. Validation of Security Policies by the Animation of Z Specifications. In Proceedings of the 16th ACM Symposium on Access Control Models and Technologies, SACMAT’11, New York, NY, USA, 2011a. ACM.

Nafees Qamar, Yves Ledru, and Akram Idani. Evaluating RBAC supported techniques and their validation and verification. In 6th International Conference on Availability, Reliability and Security, ARES’11, pages 734–739. IEEE Computer Society, 2011a. doi: 10.1109/ARES.2011.112.

Nafees Qamar, Yves Ledru, and Akram Idani. Validation of security-design models using Z. In 13th International Conference on Formal Engineering Methods, ICFEM’11, volume 6991 of LNCS, pages 259–274. Springer, 2011b. doi: 10.1007/978-3-642-24559-6\_19.
Yves Ledru, Akram Idani, Jérémy Milhau, Nafees Qamar, Régine Laleau, Jean-Luc Richier, and Mohamed-Amine Labiadh. Taking into account functional models in the validation of IS security policies. In *CAiSE Workshops*, volume 83 of *LNBIP*. Springer, 2011b.

# B. Domain Specific Languages

## B.1. Challenges

Domain-Specific Languages (DSLs) have gained significant attention in industry and academy with an increasing number of tools. Their advantage is their ability to offer substantial gains in expressiveness and ease of use compared with general purpose languages. Tools for handling DSLs can be classified in two major currents: (i) meta-compilers (Mandell and Estrin, 1966) (named also compiler-compiler) dedicated to the construction of compilers, translators, and interpreters, and (ii) language workbenches (Fowler, 2005), designed to build software through a rich environment of multiple, but integrated, domain-centric notations. The latter have received a lot of interest by the MDE community leading to a plethora of approaches with several perspectives: design, execution, debugging, code generation, etc. One can refer to Kosar et al. (2016) for a survey about tools that are referenced from 2006 to 2012, and to Iung et al. (2020) for the period between 2012 and 2019. These studies can help engineers to choose the best DSL option for a specific context and select the ones that fulfill their requirements.

The aforementioned surveys show that DSL tools have reached a good level of maturity, but they also show a major limitation of these tools, the lack of formal reasoning. Kosar et al. (2016) observed that only 5.7% of primary studies applied a formal analysis approach, and mentions that “there is an urgent need in DSL research for identifying the reasons for lack of using formal methods within domain analysis and possible solutions for improvement”. One possible reason, as discussed in (Bryant et al., 2011), could be that the syntactical description of DSLs is often straightforward, but specifying the semantics is much more harder. This would explain why the semantics are often left toward “other less than desirable means”. Obviously, for large scale projects formal methods are not as widespread, because of the overhead they may create during the development activities; nonetheless, several specialized conferences have presented a lot of approaches over the years where formal methods found their way in MDE techniques, and vice-versa. One can refer to the MoDeVVa Workshop (Model Driven Engineering, Verification and Validation) collocated with the Models conference, and also to the international conference on integrated formal methods (IFM), etc.

Unfortunately, in spite of the existence of the required material in order to provide a valuable formal approach for DSLs, not only the integration attempts remain poor, but also the applications of existing approaches remain limited to illustrative examples without going further towards realistic safety-critical requirements. This statement is based on the recent study of Iung et al. (2020) because it does not report on a better situation even several years after (Bryant et al., 2011) and (Kosar et al., 2016). In fact, Iung et al. (2020) refer to testing as ‘the’
verification feature of language workbenches. Not only the formal dimension is completely absent, but also the mapping shows that among the fifty-nine discussed tools only nine (15%) provide supports for testing. This important shortcoming of existing language workbenches weakens their applicability, especially for safety-critical systems. In these systems correctness is a strong requirement and it is often addressed by the application of formal methods.

## B.2. Contributions

The aim of my research works in the context of DSLs is to circumvent the lack of formal reasoning in language workbenches. During the last three years I devoted a great deal of effort-through this topic, leading to several publications and novel research directions. The achieved work is materialized by the Meeduse tool (Idani, A., 2020b, Idani, A. et al., 2020), which is today the only available language workbench that allows one to build and execute proved DSLs. The tool won three awards: "best verification" and "audience award" at the Transformation Tool Contest (Idani, A. et al., 2019c) and "best presentation" at the 2nd ACM Symposium on Software Engineering (Idani, A., 2021). The tool was also demonstrated during an invited keynote at the MoDeVVa'21 workshop (collocated with the Models'21 conference). Furthermore, several realistic applications have been done with Meeduse, showing how useful is a FMDE approach in the field of DSLs, and meaning also that the approach should be investigated further in the future.

### B.2.1. Applications

**Railway systems.** Most modeling tools (e.g. SafeCap, RailAid, etc) are not built on a formally defined DSL; and most formal solutions are not often supported by domain-specific modeling tools. The application of Meeduse to the railway field showed its strength to mix both aspects in the same tool. This work was funded by the NExTRegio project of IRT Railenium and supported by SNCF Réseau. The intention was to deal with the analysis of railway signalling systems based on emergent train automation solutions, especially the European Rail Traffic Management System (ERTMS) and the underlying Train Control System (called ETCS). There are three levels of ERTMS/ETCS which differ by the used equipments and the operating mode. The first two levels are already operational, and the third one is still in design and experimentation phases: it aims at replacing signalling systems with a global European GPS-based solution for the acquisition of train positions. This collaboration led to a graphical DSL (Idani, A. et al., 2019b,a) equipped with formal semantics, which safely assists domain experts while defining the domain models and simulating the underlying operating rules. This work provided several perspectives that are currently under study in the PhD thesis of A. Yar.

**Model transformations.** Model transformation is a core concept in MDE. It is aiming at automating the extraction of platform specific representations and/or executable artifacts from high level models. Despite the advances in this field, the Verification & Validation (V&V) of model transformations still remains scattered, and perspectives on the subject are still open. An
FMDE approach for model transformations makes sense as soon as critical concerns have to be taken into account. Meeduse was used to participate to the 2019 edition of the transformation tool contest (TTC'19). The call for solutions was about a case study that is well-known in safety-critical systems (even if it is an academic one): the transformation of Truth Tables (TT) into Binary Decision Diagrams (BDD). The proposed solution (Idani, A. et al., 2019c) was carried out in a collaboration with M. Leuschel from the University of Düsseldorf and G. Vega from the LIG lab. My major observation during the contest is that among the seven participants, Meeduse was the only attempt that addressed V&V; the other solutions addressed flexibility, performance and optimality. Meeduse was not only used to verify the model transformation, but also to execute it, which is its novelty in comparison with the discussed approaches. However, the downside is its low performance when executing the transformation of huge models (millions of entries). Nonetheless, as the transformation is written in B, proved and attested for middle size models, it can therefore be used as a reference specification from which one can build a low-code model transformation solution.

**XML standards.** XML is used across a lot of domains because it favours readability (thanks to its structuring features) and interoperability between platforms (thanks to the availability of parsers). Several communities have developed XML-based exchange standards to structure domain concepts and improve the interoperability of the growing number of computer applications that use these domain concepts. In the railway field for example, one can refer to RailML (Railway Markup Language, an open XML based data exchange format for data interoperability of railway applications). An XML file is a DSL, whose static semantics (well-formedness rules) are established via an XML schema, which is itself a meta-model in the MDE jargon. Dealing with XML documents opens a broad spectrum of possibilities to FMDE, since a formal approach can be applied to any domain standard approved by experts. Having this argument, I applied Meeduse to PNML (Petri-Net Markup Language), the international standard ISO/IEC 15909 for Petri-nets. PNML provides an agreed-on interchange format that is compliant with a formal definition of Petri-nets and is managed by EMF-based platforms such as PNML Framework and The ePNK. This application led to a new tool called MeeNET (Idani, A., 2022, 2020a) in which a PNML file can be executed, debugged, verified and translated into an implementation.

**B.3. Research directions**

The current applications of Meeduse and its underlying FMDE approach show the practical side of my contributions to the field of DSLs. Notwithstanding, several research directions are still under investigation.

**Reusing specifications.** Several companies, such as Siemens Transport (Essamé, 2004) and Clearsy (Pouzancre, 2003), have an established software development process that follows the B method: B specifications are written from a requirements document, and then refined until
the production of executable programs. However, one of the major difficulties with formal specifications is their poor readability, which prevents user involvement during the validation activities. In (The Standish Group, 2008) it is clearly mentioned that “lack of user involvement traditionally has been the number one reason for project failure”. Furthermore, as stated by Bjørner (2010) “before we can formulate requirements, we must understand the [application] domain”, meaning that domain specific representations are required before starting to think about formal models. In a pragmatic approach, these representations should be provided by the domain expert who has a greater knowledge of the application domain than the formal methods engineer. For these reasons I advocate for the use of DSLs as a way to validate B specifications. Since Meeduse defines the semantics of a given DSL using B, the proposal is to establish a proved linkage, also defined in B, between the provided B specifications and the DSL semantics. This question motivates the ongoing thesis of A. Yar, that is dedicated to the verification and validation of ERTMS/ETCS. On the one hand, one can find many existing formal models of ERTMS/ETCS. For example, the ABZ’2018 conference published several papers and artifacts that provide proved B specifications of ERTMS/ETCS. On the other hand, standard notations such as RailML (RailML, 2018) and Rail Topo Model (International Union of Railways (UIC), 2016), for the design of railway infrastructures are not formally defined. RailML is an XML-based language, and Rail Topo Model is defined via a UML meta-model; and hence, both standards can be seen as DSLs. The question is therefore: “how to make the bridge between the existing B artifacts, that are already proved correct, and a formal definition of standardized railway notations?”.

**DSL Refinements and Models@Runtime.** Meeduse links two technological spaces: that of the B method and that of MDE. Technically it connects ProB (Leuschel and Butler, 2008), a powerful animator and model-checker, to EMF<fnref n="3" /> (Steinberg et al., 2009), one of the most popular frameworks for building DSLs. This connection allows one to take benefit of the cross contributions of these technological spaces in order to address several interesting challenges for both DSLs and the B method. In this context I investigated two directions: incremental development of DSLs through refinements and the usage of the corresponding formal models at run-time. The first direction builds on the refinement principle of the B method, so that one can incrementally create a DSL, or provide several versions of the same DSL without breaking the global safety properties of the application domain. Regarding the usage of models at run-time, it exploits the pre-established notification mechanism of EMF. This mechanism is responsible for a great deal of the power offered to applications running EMF run-time (Steinberg et al., 2008). This second direction is inspired by (Körner et al., 2019) where the authors proposed to embed a model checker and animator into applications in order to use the formal models themselves at run-time. The approach assumes that a tool like an animator or model checker is able to compute all state transitions and proposes to implement the software system on top of programs that execute in background the formal model by choosing traversing transitions. The Meeduse approach goes a step further by reducing the effort required for writing the aforemen-

<footnote n="3">³ EMF: Eclipse Modeling Framework</footnote>
tioned programs that interact with the animator. This topic has been the subject of a master's project (M2 Génie Industriel) and was supported by DomoSûr, a local project funded by the LIG lab. The project applies Meeduse to instrument an executable smart-home solution that is proved correct. Furthermore, this approach has been applied as a proof of concept in the smart-buildings field to provide a lightweight development of outbreak prevention strategies (Idani, A., 2021).

**A pragmatic embedding of B within modelling languages.** There exists a plethora of approaches (including our works in MDS) that extract B specifications from modeling languages (UML, BPMN, Petri-Nets, etc). Overall, they share common motivations: (i) give a precise definition to the input formalism, and (ii) apply the B tools to address the verification tasks. Nevertheless, they also share a common limitation: the extraction process and the underlying transformation rules are not claimed correct in the literature. A lot of these approaches apply MDE tools (e.g. EMF (Steinberg et al., 2008), Acceleo (Eclipse, 2012), ATL (Jouault et al., 2006), etc) to ensure the transformation into B, which do not favour formal verification especially as the latter are not supported by provers and/or model-checkers. Obviously Meeduse can be applied to rethink transformational approaches using the B language so that the correctness of the transformation can be ensured. In my opinion this observation is reasonable considering that mostly these approaches are done by persons who have good skills in B. Furthermore, not only Meeduse has showed its strength in the field of model transformation, but it is itself built on an MDE architecture that can interoperate with the aforementioned tools; and given that it embeds ProB, it therefore includes the required verification features. The challenge of (correctly) embedding B within modelling languages is addressed in the xOWL project (executable OWL<sup>4</sup>), that I have undertaken recently with the LIMICS<sup>5</sup> unit of INSERM<sup>6</sup>. The project is about domain ontologies and health-care applications. Among its objectives, the xOWL project proposes to revisit, via Meeduse, the two kinds of embeddings (Aït-Ameur et al., 2017): shallow embedding and deep embedding. In a shallow embedding, the ontology is directly translated into B without keeping trace of its semantics, and in a deep embedding, the ontology together with its underlying semantic domain are mapped to a formal B model. The contribution of Meeduse is the usage of B in order to rigorously define the transformation rules, prove their correctness and execute them as well to produce the expected formal models.

**Assisted animation of xDSLs via machine learning and ProB.** Under the MDE umbrella, executable DSLs (xDSLs) are seen as an efficient way for building a model of the system, because of their ability to simulate the system's behaviour, before jumping to its implementation. Most of the tools dedicated to xDSLs provide interactive animation features (also called debugging) allowing domain experts to understand a behaviour, find the origin of errors or simply play with normal execution scenarios. This feature in Meeduse benefits from the various capabilities of ProB, especially animation, model-checking and constraint solving. However, even

<footnote n="4">⁴ OWL: Web Ontology Language.</footnote>

<footnote n="5">⁵ LIMICS: Laboratoire d'Informatique Médicale et d'Ingénierie des Connaissances en e-Santé.</footnote>

<footnote n="6">⁶ INSERM: Institut national de la santé et de la recherche médicale</footnote>
if Meeduse is built on a well-established formal approach, debugging a model remains a cyclic
process, during which, after the model is created or refined, the modeler executes it and navi-
gates through its state space to check if the requirements are satisfied, and if not, the steps are
repeated. Practically, “satisfying the requirements” means that, starting possibly from any state,
for reaching some target states, the sequence of needed actions to be performed on the model
is the desired one. Significant drawbacks of such an approach is that in the debugging loop, it
is very likely that the state space will change, thus, the same sequence of actions is no longer
valid, or the state space could be considerably large, therefore, a manual exploration could be
impractical. A brute force inspection of all the possible paths is out of discussion, thus there
is a need for an “intelligent” recommendation of which actions to perform for specific states.
With this in mind, machine learning techniques appear as a promising approach to assist inter-
active animation, by identifying the good actions to execute, towards a specific goal defined by
the domain expert. This topic has been investigated in a master’s project (M2 MoSIG) that I
co-supervised with D. Vaufreydaz from the M-PSI<fnref n="7" /> team of the LIG lab. After investigating the
state of the art, we realized that assisting the interactive animation of xDSLs via AI techniques
were not explored at all; and thus this project is a first attempt in this field. Our work resulted
in the development of a reinforcement learning approach that is integrated within Meeduse and
whose objective is to provide guidance during the animation (and the debugging) of an xDSL.

**B.3. Main publications**

**Akram Idani.** The B Method meets MDE: Survey, progress and future. In *16th International Conference on Research Challenges in Information Science (RCIS)*, volume 446 of *LNBIP*. Springer, 2022a. URL https://doi.org/10.1007/978-3-031-05760-1_29.

Akram Idani. A Lightweight Development of Outbreak Prevention Strategies Built on Formal Methods and xDSLs. In *ACM European Symposium on Software Engineering (ESSE)*. ACM, 2021. URL https://doi.org/10.1145/3501774.3501787.

Akram Idani. Formal model-driven executable DSLs: Application to Petri-nets. *International Journal on Innovations in Systems and Software Engineering (ISSE)*, 18(4), 2022b. doi: 10.1007/s11334-021-00408-4.

Akram Idani, Yves Ledru, and German Vega. Alliance of Model Driven Engineering with a Proof-based Formal Approach. *International Journal on Innovations in Systems and Software Engineering (ISSE)*, 16(3):289–307, 2020. doi: 10.1007/s11334-020-00366-3.

Akram Idani. Meeduse: A tool to build and run proved DSLs. In Brijesh Dongol and Elena Troubitsyna, editors, *16th International Conference on Integrated Formal Methods (IFM)*, volume 12546 of LNCS, pages 349–367. Springer, 2020a. URL https://doi.org/10.1007/978-3-030-63461-2_19.

<footnote n="7"><sup>7</sup> M-PSI: Multimodal Perception and sociable Interaction</footnote>
Akram Idani. Dependability of Model-Driven Executable DSLs, Critical Review and Solutions. In *14th European Conference on Software Architecture, Companion Proceedings*, volume 1269 of *CCIS*, pages 358–373. Springer, 2020b. URL https://doi.org/10.1007/s11334-021-00408-4.

Akram Idani, Germán Vega, and Michael Leuschel. Applying Formal Reasoning to Model Transformation: The Meeduse solution. In *Proceedings of the 12th Transformation Tool Contest, co-located with STAF'2019, Software Technologies: Applications and Foundations*, volume 2550 of *CEUR Workshop Proceedings*, pages 33–44, 2019a.

Akram Idani, Yves Ledru, Abderrahim Ait-Wakrime, Rahma Ben-Ayed, and Simon Collart-Dutilleul. Incremental Development of a Safety Critical System Combining formal Methods and DSMLs – Application to a Railway System. In *24th International Conference on Formal Methods for Industrial Critical Systems (FMICS'2019)*, volume 11687 of *LNCS*, pages 93–109. Springer, 2019b.

Akram Idani, Yves Ledru, Abderrahim Ait-Wakrime, Rahma Ben-Ayed, and Philippe Bon. Towards a Tool-Based Domain Specific Approach for Railway Systems Modeling and Validation. In *Third International Conference on Reliability, Safety, and Security of Railway Systems (RSSRail'2019)*, volume 11495 of *LNCS*, pages 23–40. Springer, 2019c.

## C. How to read this document?

The objective of a HDR is:

> “L’Habilitation à Diriger des Recherches sanctionne la reconnaissance du haut niveau scientifique du candidat, du caractère original de sa démarche dans un domaine de la science, de son aptitude à maîtriser une stratégie de recherche dans un domaine scientifique ou technologique suffisamment large et de sa capacité à encadrer de jeunes chercheurs.”
> (Arrêté du 23 nov. 1988 - art. 1).

Considering this objective, there are several ways to write a HDR; ranging from detailed presentation to a general overview of the major research contributions. The doctoral school ED-MSTII, advocates for two possibilities<fnref n="8" />:

> “Le mémoire d’habilitation peut correspondre à un document de type « thèse » (monographie) ou être une compilation d’articles de recherche significatifs accompagné d’une synthèse de quelques dizaines de pages.”

<footnote n="8">⁸ https://edmstii.univ-grenoble-alpes.fr/MSTII-formulaires/Procedures-HDR-MathsAppli-Info.pdf, Section 3, Page 3.</footnote>
This document is a mixture of the two possibilities. Some chapters refer to already published papers, and some other chapters present a self-contained technical contribution. In all cases, most of the work presented in this document has been published. The preamble of every chapter provides a list of papers to which the reader may refer in order to get more details about the discussed results. As stated in this introduction, I worked in two fields: MDS and MDE; hence, the remainder is structured in two parts:

* Part I (Formal Modeling of Secure IS) presents my contributions in MDS

* Part II (Building correct DSLs) presents my contributions in MDE and DSLs.
1st part

# Formal Modeling of Secure Information Systems
<figure><img src="image_6.png" /></figure>
# Chapter 1

## A Model-Driven Architecture for UML-to-B

### Contents

<table><tr><td>1.1</td><td>Brief overview of the B method</td><td>19</td></tr><tr><td>1.2</td><td>A quick survey of UML-to-B techniques</td><td>25</td></tr><tr><td>1.3</td><td>Towards a unifying method integration approach</td><td>28</td></tr><tr><td>1.4</td><td>Multiple transformations</td><td>33</td></tr><tr><td>1.5</td><td>Conclusion</td><td>40</td></tr></table>

Method integration has been a challenge since several years. The objective is to link formal and graphical paradigms in order to guarantee the quality of specifications. Indeed, on the one hand, graphical languages (such as UML) have been widely used for specifying, visualizing, understanding and documenting software systems, but they suffer from the lack of precise semantical basis. Hence, these languages are more convenient for large-scale software than for industrial applications which address safety challenges. On the other hand, formal methods (such as B (Abrial, 1996)) are specifically used for safety critical systems in order to rigorously check their correctness but they lead to complex models which may be difficult to read and understand. These complementarities between formal and graphical languages motivate a lot of research teams to develop tools which combine both languages. Indeed, disadvantages of semi-formal languages can be avoided thanks to contributions of formal languages and vice versa. In my works I focused my interest on tools dedicated to produce B models from UML diagrams.

The disparity between these two paradigms provides several transformation strategies from UML models to the B language and explains the existence of various UML to B translation
approaches (Laleau and Polack, 2002, Lano et al., 2004, Ledang, 2001, Meyer, 2001, Snook and Butler, 2006b). Each approach proposed its own transformation rules and encoded them in a dedicated tool. Despite the difference between the resulting B specifications, their transformation rules are overlapping and can be mixed and customized for a better coverage of UML concepts. For a more flexible application of model transformation tools, the works of M.-A. Labiadh (supervised by Y. Ledru and myself, and supported by the ANR-SELKIS project) proposed a unifying MDE platform in which one can enhance and customize the existing UML-to-B approaches. This chapter provides the general ideas behind the platform.

## Related publications

Akram Idani, Mohamed-Amine Labiadh, and Yves Ledru. Infrastructure dirigée par les modèles pour une intégration adaptable et évolutive de UML et B. *Ingénierie des Systèmes d'Information*, 15(3):87-112, 2010. URL https://doi.org/10.3166/isi.15.3.87-112. Extended version.

Akram Idani, Yves Ledru, and Mohamed-Amine Labiadh. Ingénierie dirigée par les modèles pour une intégration efficace de UML et B. In *Actes du XXVIIème Congrès INFORSID*, pages 261-276, 2009.

Mohamed-Amine Labiadh, Akram Idani, and Yves Ledru. Approche transformationnelle à base de méta-modèles pour l’intégration de UML et de notations formelles. In *Actes de la Conférence AFADL’10: Approches Formelles dans l’Assistance au Développement de Logiciels*, pages 197-212, Poitiers, June 2010.

## Structure

This chapter is structured as follows:

* Section 1.1 gives a quick overview about the B method and its underlying tools.

* Section 1.2 is a survey about existing UML-to-B techniques for class diagrams.

* Section 1.3 discusses a model-driven architecture that we developed to gather in a unifying framework, the various approaches.

* Section 1.4 shows how multi-transformations are defined and executed within our platform.

* Section 1.5 draws the conclusions of this chapter.
# 1.1 Brief overview of the B method

This section gives a brief overview of the B method focusing on the notions that are useful for the readability of this document. The reader can refer to the B-Book (Abrial, 1996) for more details about the B theory. Roughly speaking, B is a formal method based on mathematical foundations (set theory and first order logic) and where the system state is modeled via predefined abstract data types. It covers both static and dynamic aspects of a system. The static aspects are characterized by a set of variables and constants (called *data*) and the dynamic aspects are performed by a set of operations built on the generalized substitution theory.

## 1.1.1 Abstract machines

The notion of abstract machine is fundamental in B. It provides a structured development composed of three parts: header, declarations and operations. Abrial (1996) compares abstract machines to a pocket calculator with an invisible memory and a number of keys:

> "The memory (or better the values stored in it) forms the state of this machine, whereas the various keys are the operations that a user is able to activate in order to modify the state." Abrial (1996).

### *Structural features of abstract B machines*

**MACHINE**

**HEADER PART**

Name of the machine

Parameters

Constraints

**STATIC PART (DECLARATIVE)**

Sets

Constants

Properties of the constants

Variables (*state*)

Invariant (*properties of the state*)

**DYNAMIC PART (OPERATIONAL)**

Initialization of the variables

Operations

**END**

1. The header part: introduces the name of the machine, its parameters and the constraints of these parameters;

2. The static (declarative) part: includes sets, constants and variables. It also lists the properties of the constants and a characterization of the machine state using invariants. The latter are expressed in the first order predicate logic;
3. The dynamic (behavioural) part: includes the initialization of the variables and the various operations. The task of an operation is to modify the state of the machine without violating its invariant properties.

## 1.1.2 Structured developments

The B method masters the complexity of the formal development process using structured specifications. There are two kinds of structures: refinement and composition. Refinement is used to transform an abstract model into a more concrete one, and composition makes possible to construct an abstract machine from smaller, already defined and proved, ones.

### 1.1.2.1 Refinements

Starting from a high-level abstract specification, and following a refinement process until the production of an executable program, the B method, is a well-established development process. It has the ability to cover all the stages of a software life cycle. Indeed, B formal documents (Figure 1.1) may define several abstraction levels ranging from preliminary design to coding. The transition from one level to another is called refinement, and is guided by proof obligations whose purpose is to establish a correct relationship between the abstraction levels. This decomposition into successive proved refinements allows modular and safe developments.

<figure><img src="image_7.png" /><figcaption>Figure 1.1: Formal development process</figcaption></figure>

In B, there are two kinds of refinements: behaviour refinement and data refinement. The behaviour refinement means that the operation body is changed by an other one but without violating neither the conditions under which the initial operation is defined nor its possible executions. Data refinement applies a new set of data in the refined model, that is some data
can be replaced and some data can be added. When data are being replaced, a linkage invariant
must be defined to specify a conformity relationship between the old data and the new ones.

1.1.2.2 Composition

The B method provides an assembly mechanism aiming at the creation of structured and interdependent components. The objective, as stated in (Abrial, 1996), is to compose the specifications of two (or more) abstract machines and thus, eventually, construct abstract machines in an incremental way. The composition mechanism in B, establishes the rules under which an abstract machine can access (read, write) data and operations issued from other machines. There are five clauses that ensure this composition: INCLUDES, SEES, USES, EXTENDS, PROMOTES and IMPORTS.

The mostly used composition construct in the current document is the inclusion (clause INCLUDES). The latter is illustrated in Figure 1.2 where two abstract machines *M* and *N* are presented, and such that *N* includes *M*. The visibility rules are then as follows: (i) the parameters of *M* are not accessible outside *M*, (ii) the variables of *M* can be read by *N* but their modification is only possible via operation call, (iii) the properties of *N* can refer to sets and constants from *M*, and (iv) the invariants of *N* can refer to sets, constants and also variables from *M*.

<figure><img src="image_8.png" /><figcaption>Figure 1.2: Clause INCLUDES.</figcaption></figure>

1.1.3 Generalized substitutions

1.1.3.1 General concepts

A B machine behaves like a state/transition model whose states are represented by the various
variables of the machine and the transitions are ensured by its operations. To this aim, B applies
the generalized substitution theory, inspired by the Hoare logic (Hoare, 1969) and semantically
built on the weakest precondition (*Wp*) calculus of Dijkstra (1975). Tables 1.1 and 1.2 give
some major substitutions of the B language. Formula [*S*]R determines the *Wp* that ensures the
termination of substitution *S* and such that assertion *R* is true after the termination of *S*. For
example, in the definition of the “becomes equal” substitution, $[x := e]R$ denotes the formula obtained after replacing all free occurrences of $x$ in $R$ by expression $e$. This is defined as $R[e/x]$ (Cf. the B-Book Abrial (1996), § 1.3.3).

<table><thead><tr><th>Substitution</th><th>Formal definition</th><th>B notation</th><th>Semantics (Wp)</th></tr></thead><tbody><tr><td>Becomes equal</td><td>$x := e$</td><td>$x := e$</td><td>$[x := e]R \Leftrightarrow R[e/x]$</td></tr><tr><td>Sequencing</td><td>$S; T$</td><td>$S; T$</td><td>$[S; T]R \Leftrightarrow [S][T]R$</td></tr><tr><td>No effect</td><td>skip</td><td>skip</td><td>$[skip]R \Leftrightarrow R$</td></tr><tr><td>Preconditioned</td><td>$P|S$</td><td>PRE P THEN S END</td><td>$[P|S]R \Leftrightarrow P \land [S]R$</td></tr><tr><td>Bounded choice</td><td>$T[]S$</td><td>CHOICE T OR S END</td><td>$[T[]S]R \Leftrightarrow [T]R \land [S]R$</td></tr><tr><td>Guarded</td><td>$P \Rightarrow S$</td><td>SELECT P THEN S END</td><td>$[P \Rightarrow S]R \Leftrightarrow (P \Rightarrow [S]R)$</td></tr><tr><td>Unbounded choice</td><td>@z ⋅ S</td><td>VAR z IN S END</td><td>$[@z ⋅ S]R \Leftrightarrow \forall z ⋅ [S]R$</td></tr></tbody></table>

Where : $x$ is a variable; $e$ is an expression; $S$ and $T$ are substitutions; $P$ and $R$ are predicates.

<table><caption>Table 1.1: Primitive substitutions</caption><thead><tr><th>B Notation</th><th>Formal definition</th></tr></thead><tbody><tr><td>IF P THEN S ELSE T END</td><td>$P \Rightarrow S[] \neg P \Rightarrow T$</td></tr><tr><td>CHOICE S OR T OR ... OR U END</td><td>$S [] T [] ... [] U$</td></tr><tr><td>ANY z WHERE P THEN S END</td><td>@z ⋅ (P \Rightarrow S)</td></tr><tr><td>$x \in E$</td><td>@z ⋅ (z ∈ E \Rightarrow x := z)</td></tr><tr><td>assert P THEN S END</td><td>$P|(P \Rightarrow S)$</td></tr></tbody></table>

Where $x$ a variable; $E$ a set; $S$, $T$ and $U$ substitutions; and $P$ a predicate.

<caption>Table 1.2: Other substitutions</caption>

### 1.1.3.2 Correctness

One major advantage of B is theorem proving, which refers to the demonstration of logical formulas (called proof obligations, POs) to ensure a correctness claim for a given property (such as an invariant property). Proof obligations are defined by means of $Wp$ formulas that are generated from the various constructs of the B machine.

**POs of the initialisation.** Having the predicates $I$, $R$ and $C$, which denote respectively the invariants, the constants and the constraints of a machine, and $S$ the substitution of the initialisation; then the latter is proved correct, if and only if formula $R \land C \Rightarrow [S]I$ holds. This proof claims that starting of any state $s$ where both the properties of the constants and the constraints over the parameters of the machine are true, then the execution of $S$ from $s$ terminates in a state such that the invariant $I$ is true.

**POs of the operations.** The correctness of an operation guarantees that the invariant remains true after the execution of the operation. The invariant must be also true before. Considering
that the general form of an operation is $r \leftarrow op\_name(p) = \text{PRE } P \text{ THEN } A \text{ END}$ (where $P$ is a precondition and $A$ a substitution), then the underlying PO is: $I \wedge R \wedge C \wedge P \implies [A]I$.

### 1.1.4 Illustration

#### 1.1.4.1 A simple example

To illustrate the notions discussed in the previous subsections, let's consider the simple example of Figure 1.3. This B model is composed of two abstract machines that are related to each other via the inclusion mechanism. The left side of the figure (machine COUNTER) defines a simple counter (an integer) with three basic operations: `setParameter`, `increase`, and `decrease`. The right side is a high level model (machine RESERVATION) of a place reservation system providing two services: `book` and `cancel`.

<figure><img src="image_9.png" /><figcaption>Figure 1.3: A simple example.</figcaption></figure>

The invariant of machine COUNTER is a simple typing invariant. However, to guarantee its correctness operations `increase` and `decrease` must respect the limits `MININT` and `MAXINT`,
which justifies their respective preconditions. The invariant property of machine *RESERVATION* restricts the counter values in the interval 0..*Max*, where *Max* is a parameter of the machine. The dynamic part (initialisation and operations) of machine *RESERVATION* applies the basic operations provided by machine *COUNTER*. This is done via the inclusion mechanism, which provides a read access to the variables of the included machine and gives the possibility to call its operations.

### 1.1.4.2 Verification

The B method is assisted by several verification tools such as provers, animators and model-checkers. Butler et al. (2020) give an overview about these tools, together with their history, evolution and industrial usage. In my works I mainly used AtelierB for theorem proving and ProB (Leuschel and Butler, 2003) for animation and model-checking. Figure 1.4 is a screenshot of the interactive prover of AtelierB showing the POs of machine *RESERVATION*. The "Pre-condition predicate" refers to the claim that an operation preserves the preconditions under which it can call other operations and the "Invariant is reversed" refers to the *Wp* calculus as discussed above. From machine *RESERVATION*, AtelierB generated 6 proof obligations and it was able to prove all of them automatically.

<figure><img src="image_10.png" /><figcaption>Figure 1.4: Screenshot of the AtelierB interactive prover</figcaption></figure>

Regarding model-checking, its aim is to exhaustively explore of the state space of a B machine, which requires bounded data structures (e.g. given sets rather than abstract sets, etc).
Figure 1.5 shows the Java-FX interface of ProB (Leuschel and Butler, 2003) while checking the invariant preservation of machine RESERVATION. In this specification, parameter *Max* is set at three. In addition to the numerous verification and visualisation features of ProB, an open-source Java-based API (Körner et al., 2020) of the tool is also available, which offers convenient access to the core features of ProB via external programs.

<figure><img src="image_11.png" /><figcaption>Figure 1.5: Screenshot of ProB</figcaption></figure>

# 1.2 A quick survey of UML-to-B techniques

## 1.2.1 Existing approaches

The translation of UML diagrams into B specifications has been addressed since several years. The aim is to strengthen the semantics of UML using a mathematical language and to apply tools of the B method during the verification and validation activities. Several research works have been devoted to this topic and have defined various mappings from UML to B: UML2B (Hazem et al., 2004), UML2SQL (Laleau and Mammar, 2000), U2B (Snook and Butler, 2004) and ArgoUML+B (Meyer, 2001). Every approach has its own objectives and characteristics:

* UML2SQL (Laleau and Mammar, 2000, Laleau and Polack, 2002): this work provides a formal framework for the development of database applications. The B specifications are extracted from UML class diagrams, state-transition diagrams and activity diagrams. Refinement tactics are proposed in order to incrementally generate, from the various B
specifications, a correct implementation of a relational database and a set of safe SQL
transactions and queries (such as insertion, deletion, etc).

* U2B (Snook and Butler, 2004, 2006b): this work proposes to produce a B specification, called “natural”, so that the proof obligations are as simple as possible. For example, instead of generating a B machine from each UML class (of a class diagram), the authors generate a unique B machine that gathers the B constructs of the whole package. Integrity constraints are expressed in a new formalism (μB) that is built on the B language. Furthermore, C. Snook and his co-authors in (Snook and Butler, 2006b) bring a touch of originality to this technique by specializing UML concepts using stereotypes. These stereotypes provide some guidance to the translation process. In this work both UML class diagrams and state/transition diagrams are addressed.

* ArgoUML+B (Ledang, 2001, Meyer, 2001): this work tried to take into account complex UML features. It proposed, on the one hand, various solutions for the translation of the UML inheritance mechanism, and on the other hand, a new formalization of state/transition diagrams. The starting point is a UML specification (so-called “complete”) describing both structural and behavioral aspects of a system. The authors associate to each UML-to-B translation rule a derivation schema showing how the UML constructs are mapped to the B model. Other contributions of this work include the coverage of use-case diagrams and transitions with multiple sequenced actions.

1.2.2 Application

Figure 1.6 applies the three translation tools to a simple UML class with one attribute and
shows the resulting B models. One can observe from this figure that there is a consensus about
the core B data produced from a UML class, however the relation between these data is trans-
lated in different ways. The two first approaches transform a class *C* into an abstract set *A*
(clauses SETS of figure 1.6) representing the set of possible instances of the class and a vari-
able *v* (clauses VARIABLES of figure 1.6) representing the set of existing instances of *C*. The
invariant (clauses INVARIANT of figure 1.6) produced by the U2B tool (Snook and Butler,
2004) is *v* ∈ P(*A*) while the invariant produced by the UML2SQL tool (Laleau and Mammar,
2000) is *v* ⊆ *A*. Although these two invariants are semantically similar, they are structurally
different because they result from two different transformation rules. The ArgoUML+B tool
(Meyer, 2001, Ledang, 2001) produces the same invariant as the UML2SQL tool. However, it
adds the set of all possible objects *OBJECTS* and considers that *A* is a constant such that *A* ⊆
*OBJECTS*. This third translation is structurally and semantically different from the two others.

This example shows that an analyst who is working on the formalization of a UML diagram
may be interested by these three transformations depending on the point of view that he/she
wants to address. Indeed, one may imagine a fourth transformation in which the U2B and
the ArgoUML+B approaches are combined together; meaning that we keep set *OBJECTS* and
constant *A* such that *A* ⊆ *OBJECTS*, but we produce the invariant of the U2B tool: *v* ∈ P(*A*).
Similar ideas can be applied to class attributes producing a total function (→) or a relation (↔) depending on the selected approach.

<figure><img src="image_12.png" /><figcaption>Figure 1.6: Several translations of a UML Class into B</figcaption></figure>

### 1.2.3 Discussion

Table 1.3 summarizes the structural features of UML class diagrams that are addressed by the three major UML-to-B approaches. The table shows that each approach has its advantages and limitations and that obviously for a better coverage of UML a combination of the various approaches is needed. The research works of M.-A. Labiadh started from this observation and proposed a Model-Driven Architecture (MDA) in which various transformations can be applied and experimented. The MDE paradigm is suitable in this context since MDE widely addressed languages and techniques to define and execute model transformations. In the MDE literature, most works were interested by the developer point view: "*how to encode the transformation rules and apply the underlying execution engines*".

In this work, we are also interested by the user point of view. When several transformations are possible for a given element in the source model, existing tools restrict the transformation to only one choice in order to make the transformation deterministic. However, the end-user may be interested by various possible choices depending on his/her point of view about the good resulting model. This problem is more general than the particular case of UML-to-B. The extraction of Java programs from UML is a good illustration of this claim. One can get different Java programs by applying different tools. Modelio<fnref n="1" /> for example provides a unique code generation feature, while the IBM RSA tool<fnref n="2" /> provides a configuration feature that allows

<footnote n="1">¹ Modelio: https://www.modelio.org</footnote>

<footnote n="2">² RSA Designer: https://www.ibm.com/products/rational-software-architect-designer</footnote>
the user to personalize the transformation by (un)picking some pre-established options.

<table><thead><tr><th></th><th>UML2SQL</th><th>ArgoUML+B</th><th>U2B</th></tr></thead><tbody><tr><td>Classes (undetermined instances)</td><td>+</td><td>+</td><td>+</td></tr><tr><td>Classes (fixed instances)</td><td>-</td><td>-</td><td>+</td></tr><tr><td>Class attributes</td><td>+</td><td>+</td><td>+</td></tr><tr><td>Distinction between multi/mono-valued attributes</td><td>+</td><td>-</td><td>-</td></tr><tr><td>Inheritance</td><td>+</td><td>+</td><td>+</td></tr><tr><td>Associations multiplicities</td><td>+</td><td>+</td><td>+</td></tr><tr><td>Associations navigation direction</td><td>-</td><td>+</td><td>+</td></tr><tr><td>Roles</td><td>+</td><td>-</td><td>+</td></tr><tr><td>Associations constraints</td><td>+</td><td>+</td><td>-</td></tr><tr><td>Distinction between fixed/non-fixed associations</td><td>+</td><td>-</td><td>-</td></tr><tr><td>Association</td><td>+</td><td>+</td><td>-</td></tr><tr><td>Associative classes</td><td>+</td><td>-</td><td>-</td></tr><tr><td>Parametrized classes</td><td>-</td><td>-</td><td>+</td></tr></tbody></table>

**Legend**: "+" (considered criterion) ; "-" (non considered criterion)

<caption>Table 1.3: Overview of the supported UML structural features</caption>

# 1.3 Towards a unifying method integration approach

## 1.3.1 Model driven engineering and method integration

The model driven engineering (MDE) approach OMG (2003) defines the software development life-cycle as an iterative process based on model refinement and integration. It makes the distinction between Platform Independent Models (PIM) and Platform Specific Models (PSM).

PIM: "A platform independent model is a view of a system from the platform independent viewpoint. A PIM exhibits a specified degree of platform independence so as to be suitable for use with a number of different platforms of similar type." OMG (2003).

PSM: "A platform specific model is a view of a system from the platform specific viewpoint. A PSM combines the specifications in the PIM with the details that specify how that system uses a particular type of platform." OMG (2003).

A software development process built on MDE is therefore seen as a gradual transformation of a PIM model, which specifies the solution of a system independently of the programming technologies, to a PSM model that describes how this solution can be implemented in a given technology. To this purpose, the MDE approach advocates for the use of rules to define the consistency of models and to gradually transform them during the development process.
Platforms that support this approach require a precise description of the various models using
meta-models. Hence, a model transformation rule is a possible projection from a source meta-
model to a target meta-model. In the context of method integration (e.g. UML and B), the MDE
approach has several benefits:

(i) Identify the subset of the input model for which the transformations can be applied;

(ii) Have a well-defined and executable catalog of transformation rules;

(iii) Instrument, via several possible tools, the meta-models and the transformation rules.

1.3.2 The proposed model driven architecture

Existing MDE platforms dedicated to model transformation include a transformation engine that is built on three major elements: (i) the model handler such as EMF<fnref n="3" /> (Steinberg et al., 2009), (ii) the transformation language such as QVT<fnref n="4" /> (Gardner et al., 2003), and (iii) the language interpreter (or compiler) such as QVTo (Eclipse, 2021). Our MDE architecture for UML-to-B is developed within the EMF platform, where model transformations can be defined at different abstraction levels:

* The lowest level, based on the EMF APIs, often applies the Java programming language;

* The highest level applies a high-level transformation language close to QVT, such as ATL (Jouault et al., 2006) and its virtual machine;

* The intermediate level applies a meta-programming language such as XTend (Efftinge, 2006), which is a dialect of Java that compiles into Java compatible source code.

As our intention is to mix the UML-to-B approaches in one unifying framework, then the un-
derlying transformation rules must fulfil some functional requirements according to the end-user
and the rule-writer (the developer) points of view. From a user point of view, the transformation
environment must be configurable and offers therefore the possibility to adapt the transforma-
tion process by combining rules issued from different approaches. From a rule-writer point of
view, the tool must on the one hand offer an extensibility feature to easily introduce new trans-
formations, and on the other hand, provide a way to execute rules that are encoded at different
abstraction levels.

Figure 1.7 illustrates the proposed MDE architecture. It is composed of three components: UML, M2M<fnref n="5" /> and TMF<fnref n="6" />. Component UML can be any Eclipse based UML editor (e.g. Top-Cased, Papyrus, etc). Component M2M constitutes the originality of this work. It includes a transformation engine, so-called “UML/B Transformation Engine”, that manages and executes the UML-to-B transformations at different abstraction levels. The inputs of this engine are:

<footnote n="3">³ Eclipse Modeling Framework: www.eclipse.org/modeling/emf/</footnote>

<footnote n="4">⁴ Query/View/Transformation: https://www.omg.org/spec/QVT/1.3/PDF</footnote>

<footnote n="5">⁵ M2M: Model to model.</footnote>

<footnote n="6">⁶ TMF: Textual modelling framework.</footnote>
(i) the UML and B meta-models (the latter is roughly discussed in the next subsection),

(ii) a catalog of UML-to-B rules that are written in Java (for the lowest level), QVTo (for the highest level) or XTend (for the intermediary level), and

(ii) a user-defined configuration file giving the transformation process and the sequence of rules to apply from the catalog (this point is detailed in section 1.4).

Finally, component TMF generates the textual file from a given instance of the B meta-model (called B model in Figure 1.7). It applies a classical model-to-text transformation.

<figure><img src="image_13.png" /><figcaption>Figure 1.7: Linking UML and B in an MDE architecture</figcaption></figure>

Besides the possibility to reuse and combine rules issued from different UML-to-B approaches, the advantage of this MDE architecture compared with the existing UML-to-B tools (U2B, ArgoUML+B, UML2SQL) is its extensibility. In fact, in order to cover the transformation of UML constructs that have not been considered by the existing approaches, the rule-writer simply adds new rules to the default catalog of transformations that we have implemented; and, if necessary, extends the B meta-model.
### 1.3.3 A meta-model for the B method

The B meta-model is a core element of our platform. This meta-model has been discussed in (Idani, A., 2006, Idani, A. and Coulette, 2008, Idani, A. et al., 2009, Idani, A., 2009). It is used by components M2M and TMF of Figure 1.7, which are respectively dedicated to the translation from UML into B, and the generation of the B textual files from the resulting B model. This meta-model gives a high-level structural view about the abstract syntax of B. I present an excerpt of it here in order to give an overview of its main concepts and show how the dependencies between the various B constructs are defined.

#### 1.3.3.1 Abstract machines

An abstract machine (Figure 1.8), specified by the meta-class *BMachine*, is composed of static and dynamic parts. The static part contains declarations of sets, constants and variables, and a characterization of these data in terms of constants properties (clause *PROPERTIES*) and invariants (clause *INVARIANT*). Meta-class *BData* refers to: abstract sets (*BAbstractSet*), given sets (*BEnumSet*), constants (*BConstant*) and variables (*BVariable*). The dynamic part, is defined by meta-classes *BOperation* and *BInitialisation*, which are used to represent respectively the operations and the initialization of a B machine.

<figure><img src="image_14.png" /><figcaption>Figure 1.8: B abstract machines meta-model</figcaption></figure>

#### 1.3.3.2 Typing

The B typing meta-model is given in Figure 1.9. It represents the abstract syntax of the most commonly used constructs for typing B data. It does not refer to the B theory. For example, a variable *R* can be defined in a B machine as:
$$R = \{r | r \in \mathbb{P}(E_1 \times E_2) \wedge \\ \forall x, y, z \cdot (x, y \in r \wedge x, z \in r \Rightarrow y = z)\}$$

where $E_1$ and $E_2$ are two abstract sets (instances of meta-class *BAbstractSet*). However, such a variable is commonly typed in B with the following invariant:

$$R \in E_1 \rightarrow E_2$$

and corresponds to a partial function. The B meta-model is then suitable for this second definition of variable *R*. In fact, it deals with a subset of the B language which is sufficient to cover all the UML-to-B translations addressed by the existing approaches.

<figure><img src="image_15.png" /><figcaption>Figure 1.9: B typing meta-model</figcaption></figure>

Typed elements (meta-class *BTypedElement*) are: parameters, constants, variables, predefined B values (e.g. TRUE and FALSE) and values of given sets. Class *TypingPredicate* mainly represents: equality, inclusion and membership. Since the meta-model does not represent the B theory, but the B syntax, it distinguishes between the various typing operators.

Basic types of the B language are represented with class *BBasicType*. They include pre-defined primitive types (class *BPrimitiveType*) such as BOOL and NAT, and B sets which are mainly abstract sets (class *BAstractSet*) and given sets (class *BENUMSet*). Meta-class *BPowType* represents a type defined using the power-set type constructor $\mathbb{P}$. Some specializations of this meta-class could be defined such as $\mathbb{P}_1$, $\mathbb{F}$ (finite power-set) and $\mathbb{F}_1$.
### 1.3.3.3 Relations and associations

Class *BComposedType* denotes any type defined from at least two other types. It designates functional relations (e.g. “↔”, “→”, etc) and products. Each *BComposedType* is then defined from the types of its domain (role name **+dom**) and its range (role name **+ran**). Regarding Meta-class *Multiplicity*, it describes the cardinalities of the functional relations (Table 1.4). Although these cardinalities are not explicitly defined in B, they are introduced in the meta-model because of their suitability to the translation of UML associations into B relations.

<table><caption>Table 1.4: Cardinalities associated to specializations of functional relations.</caption><thead><tr><th rowspan="2">ComposedType</th><th colspan="2">multDom</th><th colspan="2">multRan</th></tr><tr><th>lower</th><th>upper</th><th>lower</th><th>upper</th></tr></thead><tbody><tr><td>Relation ↔</td><td>0</td><td>*</td><td>0</td><td>*</td></tr><tr><td>Partial function →</td><td>0</td><td>*</td><td>0</td><td>1</td></tr><tr><td>Total function →</td><td>0</td><td>*</td><td>1</td><td>1</td></tr><tr><td>Partial injection ↔</td><td>0</td><td>1</td><td>0</td><td>1</td></tr><tr><td>Total injection →</td><td>0</td><td>1</td><td>1</td><td>1</td></tr><tr><td>Partial surjection ↔</td><td>1</td><td>*</td><td>0</td><td>1</td></tr><tr><td>Total surjection →</td><td>1</td><td>*</td><td>1</td><td>1</td></tr><tr><td>Partial bijection ↔</td><td>1</td><td>1</td><td>0</td><td>1</td></tr><tr><td>Total bijection →</td><td>1</td><td>1</td><td>1</td><td>1</td></tr></tbody></table>

## 1.4 Multiple transformations

Most of the MDE tools that deal with model transformations apply stand-alone transformations where the transformation is defined as a list (preferably deterministic) of transformation rules. However, often various model transformations need to be composed and integrated during the modeling activities (e.g. UML-to-Java). One naive solution for multiple transformations is to encode all the possible transformations and let the user select the one that satisfies his/her objective. However, this is not suitable for us, because on the one hand, this would lead to a multitude of different UML-to-B transformations, and on the other hand, among our requirements we would like to provide an extensibility mechanism so that one can adapt existing rules or extend them. Thus, the transformation could not be stand-alone, and must be configured by the end-user, who decides which rules to apply. Making the transformation configurable, gives a fine-grained application level to its rules. Rather than selecting a pre-established transformation, the user creates his/her own transformation by selecting the rules to apply.

### 1.4.1 A meta-model for configurable transformations

One major benefit of configurable transformations is that the underlying rules can be reused. In a stand-alone approach common rules must be duplicated, which makes their modification complex and error-prone. However, the difficulty of configurable transformations is to correctly
manage their variations and their uncommon parts. Wagelaar and Straeten (2006) discussed this challenge and presented three techniques that can help manage the composition of model transformations in an MDE context: knowledge-based systems, feature modeling and domain-specific languages (DSLs). These techniques are not directly related to our intention to apply MDE tools in order to deal with multiple transformations. In fact, the underlying solutions are more suitable to model refinements and model refactoring. Nevertheless, they are inspiring as they recommend the definition of a grammar (or a meta-model) that describes the legal configurations of model refinements. This idea is developed and enriched in this work in order to address the multiple transformations of UML into B. Figure 1.10 is a simplified version of our meta-model (Idani, A. et al., 2010a) for configurable transformations. It features two components: *ExecutionContext* and *Configuration*.

<figure><img src="image_16.png" /><figcaption>Figure 1.10: Configurable model transformation meta-model</figcaption></figure>
The execution context (whose entry point is class `ConfigContext`), is apart of the API of our transformation engine. It refers to: the input UML model, the output B model (class `BSpec`), the user configuration (class `Config`), and a trace model (class `Trace`) that registers the executed rules together with their inputs and outputs. Regarding the configuration, as stated in Figure 1.7 (Section 1.3.2, Page 30), in addition to the catalog of UML-to-B rules, the user provides a configuration model (called `Config` in Figure 1.7). This model covers three major notions: (i) transformation process and phasing, (ii) abstraction levels and (iii) transformation rules. Note that most of the concepts of this meta-model are generic and can be reused for other kinds of multiple transformations (e.g. UML-to-Java). To this purpose only a subset of the execution context need to be specialized.

## 1.4.2 Transformation process and phasing

In (Czarnecki and Helsen, 2006, Cuadrado and Molina, 2007) phasing is defined as a scheduling mechanism in which the transformation process is divided in several steps, each of which gathers rules that share a specific purpose. Inspired by these works, we define a transformation (meta-class `Transformation`) as a sequence of phases whose order is specified by the “rule writer”. Attribute `active` of meta-class `Phase` allows one to switch-off a phase and association `require` defines the dependencies that must be checked before running a phase. Figure 1.11 gives a phasing example composed of five steps that depend on the input UML element: packages, classes, associations, attributes and operations.

Top-down arrows represent the ordering of phases, and bottom-up arrows represent the dependencies between them. For example, the transformation of attributes, associations and operations requires the transformation of classes. If the latter is not active then the other phases cannot be executed.

<figure><img src="image_17.png" /><figcaption>Figure 1.11: A transformation process for a UML class.</figcaption></figure>
### 1.4.3 Abstraction levels

For a good flexibility of the UML-to-B transformations, we propose three configuration levels (meta-class `Config` and attribute `level`):

* Meta-model level ($M^2$): means that the transformation rules of a specific configuration are applied uniformly to all elements of the source model. This is the common approach, called MTM (Model Type Mappings) in the initial MDA specification (OMG, 2003).

* Model level ($M^1$): at this level all elements of the source model that are concerned by the configuration are tagged with their corresponding transformation rule. To this purpose our platform embeds a UML profile, which allows one to apply stereotypes to the elements to be transformed.

* Mixed level ($M^{1/2}$): allows us to customize the $M^2$ level by forcing some elements from the source model to be translated differently with a specific transformation rule.

The $M^1$ configuration is hardly applicable to real size models because it needs to tag all the elements of the UML model. It is interesting when a small subset of the source model is translated. The $M^2$ level allows us to apply existing UML-to-B approaches as they are or to define new approaches. The idea is to encode their corresponding rules and simply execute them on a given UML model. The $M^{1/2}$ level is, in our opinion, the most interesting one because it provides the possibility to combine rules issued from several transformation approaches. Indeed, one can select a by-default UML-to-B approach (among the ones discussed in Section 1.2) and apply stereotypes to the elements that have to be transformed with different approaches.

Technically, a configuration is an instance of meta-class `Config` of figure 1.10 where attribute `level` can be either `M2` or `M1/2`. The model level ($M^1$) is applied when all the model elements are stereotyped and the `M1/2` level is selected by the user. Figure 1.12 gives the rule selection process. The choice of the execution level (*identifyExecLevel?*) conditions the transformation according to the two values: `M2` or `M1/2`. For each UML element concerned by the user configuration, the UML/B transformation engine proceeds as follows:

* If attribute `level` is set at `M2`, then the transformation engine applies a transformation strategy (*identifyApproach?*) among two possibilities (attribute `method` of meta-class `Config`): `getRuleByMethod` and `getRuleByAdvice`. The first strategy refers to a well-defined approach, for example the ones discussed in Section 1.2. When this strategy is selected (`method = APPROACH`) the transformation engine automatically unfolds all the underlying rules. The second strategy (`method = RULE`) is intended to experiment user-defined rules, which are additional rules that do not belong to an existing approach, or a customization of existing ones.

* If attribute `level` is set at `M1/2`, then the transformation engine checks whether the UML element is tagged with a stereotype or not. Operation `getRuleByStereotype` applies
the rule referenced by the stereotype according to a UML profile that we defined to address the *M*¹ level. This mechanism allows the user to control the transformation stating, element by element, the rule to be applied. However, the main limitation of this mechanism, in the current version of our platform, is that the dependencies between the rules and their compatibilities, must be entirely managed by the user. If the UML element is not stereotyped, one of the *getRuleByMethod* and *getRuleByAdvice* strategies is applied, depending on the user choice.

<figure><img src="image_18.png" /><figcaption>Figure 1.12: Rule selection process.</figcaption></figure>

### 1.4.4 Transformation rules

A phase is composed of an ordered set of abstract rules (meta-class `AbstractRule`), providing a choice among a set of concrete rules (meta-class `ConcreteRule`). An abstract rule is a mapping from one or several input objects (e.g. a UML element) to one or more output objects (e.g. B elements). Every abstract rule is implemented by one or many concrete rules, which provides several possible behaviours to a given phase. Attribute `URI` in class `ConcreteRule` refers to the location of the concrete rule. The latter can be encoded in Java, XTend or high-level transformation languages (e.g. ATL, QVT); and hence, a transformation can be a mixture of different languages. Our UML/B transformation engine is able to invoke external EMF-based
tools, such as QVTo, as far as a concrete rule respects the signature (inputs and outputs) of the
abstract rule that it implements.

In order to illustrate these notions, let’s consider two transformation approaches. The first
one, inspired by (Snook and Butler, 2004), produces a single B machine for the whole class
diagram. We call this approach *UniqueMachine*. It aims to reduce the modularity of the B
specification and thus to simplify the theorem proving activity. The second approach, inspired
by (Meyer, 2001), produces a B machine from every class, and a root machine that includes
the other ones to represent the class diagram. This approach leads to a modular B specifi-
cation. We call it *MachineByClass*. Both approaches are defined in Figure 1.13 which is an
instance of our configurable transformations meta-model. They are represented with the two
instances of meta-class *Approach*. In this object diagram a transformation is created (obj-
ject *MyTransformation*) with two phases, *Phase1* and *Phase2*, which are dedicated
respectively to the transformation of packages and classes. In this example we assume that
a class diagram is defined in one package. We consider two abstract rules (one per phase):
*TransformPackage* and *TransformClass*. The former is realized by a JAVA-based
concrete rule (*createSysMachine*), and the latter is realized with two concrete rules that
are written in *XTend* (*ClassToBVariable* and *ClassToMachine*).

<figure><img src="image_19.png" /><figcaption>Figure 1.13: An object diagram.</figcaption></figure>

Figure 1.14 shows three configurations applying transformation *MyTransformation*.
By running *config1* the rule selection process executes rule *createSysMachine* fol-
lowed by rule *ClassToBVariable*. Configuration *config2* leads to the execution of
`createSysMachine` followed by `ClassToMachine`. In the first case, when an abstract rule is not realized by any concrete rule that is compliant with the selected approach, the execution process runs the selected default rule (association `selected`). In the second case, the execution process sequentially runs all default rules and does not care about which approaches they are compliant with. For example, `config2` is associated to approach `UniqueMachine`, but it leads to the execution of rule `ClassToMachine`, which is compliant with approach `MachineByClass`. We keep association `selectedApproach` mandatory in order to provide the possibility to quickly switch between the two methods (i.e. `APPROACH` and `RULE`). Regarding `config3` it provides the possibility to execute specific rules to particular classes: by default approach `UniqueMachine` is executed but it allows to translate some classes with rule `ClassToMachine`.

<figure><img src="image_20.png" /><figcaption>Figure 1.14: Example configurations.</figcaption></figure>

### 1.4.5 Application

To illustrate the three configurations we consider the class diagram of Figure 1.15 where class `Client` is tagged with stereotype «`ClassToMachine`».

<figure><img src="image_21.png" /><figcaption>Figure 1.15: A class diagram</figcaption></figure>
The resulting specifications are given in Figure 1.16. Note that the transformation process first extracts an instance of our B meta-model, and then produces the textual files.

<figure><img src="image_22.png" /><figcaption>config2: Machine By Class</figcaption></figure>

<figure><img src="image_23.png" /><figcaption>config3: Mixed approach</figcaption></figure>

<figure><img src="image_24.png" /><figcaption>Figure 1.16: Three different transformations</figcaption></figure>

1.5 Conclusion

A well-known challenge in software engineering is to have a software specification language
that combines precision of formal notations and expressiveness of graphical (or semi-formal)
notations. Several research works have been devoted in order to study possible mappings be-
tween these two kinds of notations. This part of my research works has proposed a model
driven platform that allows one to integrate several approaches in a single tool. The underly-
ing platform can be used, on the one hand, to combine and extend translation rules from UML
diagrams into formal B specifications, and on the other hand, to define transformation rules in
several languages (e.g. Java, XTend, etc).

More generally, model transformation has received a lot of interest from the research com-
munity leading to languages and techniques to encode and execute transformation rules. Most
of these works deal with deterministic transformation rules and hence some transformation
choices are done implicitly by the rule writer. The originality of the proposed solution is that it
deals with multiple transformations and provides a way to the final user to configure the trans-
formation. Multiple transformation means that there are several transformation choices of a
source model element. In the existing MDE tools these choices are often done by developers.
For example, tools that transform an object model into a relational database may produce a
table for every class, however one can be interested by generating tables only from concrete
classes and apply other rules to transform abstract classes. Several other examples can be cited
such as tools that generate a java source code from UML diagrams: StarUML does not generate
getters and setters for private and public attributes while EclipseUML generates automatically
getters and setters for private and also public attributes. However, a user may be interested by
a mixture of these two transformations: generate getters and setters only for private attributes.
The proposal done in this chapter provides a flexible application of model transformation since
the choice amongst transformation rules is done by the end-user, not by the developer.
# Chapter 2

## Formal Model-Driven Security

### Contents

<table><tr><td>2.1 Role-Based Access Control (RBAC)</td><td>46</td></tr><tr><td>2.2 B4MSecure</td><td>52</td></tr><tr><td>2.3 Animation and dynamic analyses</td><td>66</td></tr><tr><td>2.4 Discussion and conclusion</td><td>71</td></tr></table>

Most faults in Information systems (IS) are traced back to deficiencies in specifications (Martin, 2003) and may originate from both functional and non-functional requirements. In a UML-based development process, functional requirements can be defined by means of class diagrams showing the various entities involved in the application logic. Regarding the non-functional requirements my work focuses on security requirements, expressed as access control rules. These rules not only require robust specification methods but also validation and verification techniques to protect systems against malicious attacks. In this context I have been mainly interested by the Role-Based Access Control model (Ferraiolo et al., 2001), which is intended to support access control properties such as confidentiality, integrity, availability and traceability. This topic has been the subject of the PhD thesis of N. Qamar and M.-A. Labiadh that I co-supervised with Y. Ledru and led to the development of the B4MSecure platform (Idani, A. and Ledru, 2015).

In (Qamar et al., 2011a) a comparative study evaluating access-control supported techniques and their validation and verification has been presented and has showed that existing approaches (formal or semi-formal) have significantly dealt with static features. The dynamic features are partially covered and they often do not include functional requirements. In fact, when systems become complex, separation of concerns is often perceived as a good strategy to master complexity. This explains why functional and security models are often validated separately. Although it is definitely useful to first analyse both models in isolation, interactions between
these models must also be taken into account. Indeed, constraints expressed in the security model also refer to information of the functional model. Hence, evolutions of the functional state may influence the security behaviour. Conversely, security constraints can impact the functional behaviour. A typical example is a rule assuming that in order “*to modify a file the current user must be the owner of the file*”:

* “*current user*”: is a security concern referring to a user that is connected to the system.

* “*modify a file*”: is a functional concern dealing with a data, and a possible action.

* “*owner*”: is an **authorization constraint** that grants or forbids file modification.

An **authorization constraint** is a constraint that combines functional and security concerns to grant a permission. The proposed FMDE solution to deal with these constraints covers the functional description of the IS as well as its security policy. The supporting models are based on UML for the functional description and SecureUML (Basin et al., 2006, 2009) for the access control rules. A formal B specification is generated automatically from these models, which allows one to formally reason about the whole system: functional and security models can be first validated separately, and then integrated in order to verify their interactions. This chapter describes our solutions and gives the principles of the B4MSecure platform.

## Related publications

Yves Ledru, Akram Idani, Jérémy Milhau, Nafees Qamar, Régine Laleau, Jean-Luc Richier, and Mohamed-Amine Labiadh. Validation of IS security policies featuring authorisation constraints. *International Journal of Information System Modeling and Design*, 6(1):24–46, 2015a. URL https://doi.org/10.4018/ijismd.2015010102.

Akram Idani and Yves Ledru. B for Modeling Secure Information Systems, The B4MSecure Platform. In Michael J. Butler, Sylvain Conchon, and Fatiha Zaidi, editors, *17th International Conference on Formal Engineering Methods (ICFEM), Paris, France, November 3-5*, volume 9407 of LNCS, pages 312–318. Springer, 2015. URL https://doi.org/10.1007/978-3-319-25423-4_20.

Yves Ledru, Akram Idani, and Jean-Luc Richier. Validation of a security policy by the test of its formal B specification - A case study. In Stefania Gnesi and Nico Plat, editors, *3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, FormaliSE'15, Florence, Italy, May 18*, pages 6–12. IEEE Computer Society, 2015b. URL https://doi.org/10.1109/FormaliSE.2015.9.

Jérémy Milhau, Akram Idani, Régine Laleau, Mohamed-Amine Labiadh, Yves Ledru, and Marc Frappier. Combining UML, ASTD and B for the formal specification of an access control filter. *International Journal on Innovations in Systems and Software Engineering (ISSE)*, 7 (4):303–313, 2011. URL https://doi.org/10.1007/s11334-011-0166-z.
Yves Ledru, Akram Idani, Jérémy Milhau, Nafees Qamar, Régine Laleau, Jean-Luc Richier, and Mohamed-Amine Labiadh. Taking into account functional models in the validation of IS security policies. In Camille Salinesi and Oscar Pastor, editors, *CAiSE'11 Workshops*, London, UK, June 20-24, volume 83 of LNCS, pages 592-606. Springer, 2011a. URL https://doi.org/10.1007/978-3-642-22056-2_62.

Nafees Qamar, Yves Ledru, and Akram Idani. Validation of security-design models using Z. In Shengchao Qin and Zongyan Qiu, editors, *13th International Conference on Formal Engineering Methods (ICFEM)*, Durham, UK, October 26-28, volume 6991 of LNCS, pages 259-274. Springer, 2011a. URL https://doi.org/10.1007/978-3-642-24559-6_19.

Nafees Qamar, Yves Ledru, and Akram Idani. Evaluating RBAC supported techniques and their validation and verification. In *Sixth International Conference on Availability, Reliability and Security (ARES)*, Vienna, Austria, August 22-26, pages 734-739. IEEE Computer Society, 2011b. URL https://doi.org/10.1109/ARES.2011.112.

Yves Ledru, Nafees Qamar, Akram Idani, Jean-Luc Richier, and Mohamed-Amine Labiadh. Validation of security policies by the animation of Z specifications. In Ruth Breu, Jason Crampton, and Jorge Lobo, editors, *16th ACM Symposium on Access Control Models and Technologies (SACMAT)*, Innsbruck, Austria, June 15-17, pages 155-164. ACM, 2011b. URL https://doi.org/10.1145/1998441.1998471.

Yves Ledru, Akram Idani, Rahma Ben Ayed, Abderrahim Ait Wakrime, and Philippe Bon. A separation of concerns approach for the verified modelling of railway signalling rules. In *Third International Conference on Reliability, Safety, and Security of Railway Systems - Modelling, Analysis, Verification, and Certification (RSSRail)*, volume 11495 of LNCS, pages 173-190. Springer, 2019. URL https://doi.org/10.1007/978-3-030-18744-6_11.

Abderrahim Ait Wakrime, Rahma Ben Ayed, Simon Collart Dutilleul, Yves Ledru, and Akram Idani. Formalizing railway signaling system ERTMS/ETCS using uml/event-b. In *8th International Conference on Model and Data Engineering - MEDI*, volume 11163 of LNCS, pages 321-330. Springer, 2018. URL https://doi.org/10.1007/978-3-030-00856-7_21.

## Structure

This chapter is structured as follows:

* Section 2.1 roughly describes the Role-Based Access Control (RBAC) model.
* Section 2.2 presents the principles of the B4MSecure platform.

* Section 2.3 shows how dynamic analyses can be done using B4MSecure and ProB.

* Section 2.4 draws the conclusion and the perspectives of this chapter.

# 2.1 Role-Based Access Control (RBAC)

## 2.1.1 Main concepts

RBAC access control mechanism can be used to ensure important properties of data security i.e. integrity, confidentiality and availability. Figure 2.1 shows the main concepts of the RBAC model: users (USERS), roles (ROLES), objects (OBS), permissions (PRMS) and operations (OPS). A sixth data type, session (SESSIONS), is used to associate roles temporarily to users, which corresponds to the dynamic part of RBAC. The model differentiates between users and roles: a role is considered as a permanent position in an organization whereas a given user might be switched with another user for that role. Thus, permissions are offered to roles instead of users. A permission refers to operations (application-specific user functions) that can be executed on objects (resources to protect). UA is user assignment, RH is role hierarchy and PA is permission assignment. These concepts are defined in (Ferraiolo et al., 2001) as:

- UA $\subseteq$ USERS $\times$ ROLES: a many-to-many mapping between users and roles, UA specifies which roles can be played by a given user;

- PA $\subseteq$ PRMS $\times$ ROLES: a many-to-many mapping permission-to-role, PA expresses which roles may be granted a given permission;

- RH $\subseteq$ ROLES $\times$ ROLES: a partially ordered role hierarchy, a senior role may inherit the permissions from its junior roles;

- user_sessions($u$ : USERS) $\rightarrow$ Fin(SESSIONS): the mapping of user $u$ onto a set of sessions, it lists the current session of a given user;

- session_roles($s$ : SESSIONS) $\rightarrow$ Fin(ROLES): the mapping of session $s$ onto a set of roles, it lists the current roles of a given user in a given session;

- PRMS = OPS $\times$ OBS: the set of permissions.

RBAC includes also the principle of separation of duty (SoD), which is intended to enforce conflict of interest policies. There are two main types of separation of duty: SSD (Static Separation of Duties) and DSD (Dynamic Separation of Duties). A SSD forbids a user to be assigned to conflicting roles. It is therefore related to relation UA (and possibly relation RH). A DSD forbids a given user to take conflicting roles simultaneously in the same session.
<figure><img src="image_25.png" /><figcaption>Figure 2.1: Role-based Access Control (Ferraiolo et al., 2001)</figcaption></figure>

Advanced RBAC models allow the specification of constraints such as SoD properties and other properties on roles (e.g. precedence). In IS, contextual information may also be taken into account when designing an access control policy. This contextual information may correspond to the current state of the information system, or to the history of interactions with the system. This has led to the notion of **authorisation constraint** in SecureUML (Basin et al., 2006, 2009).

## 2.1.2 Modeling RBAC with SecureUML

In the literature there exists a number of RBAC representations. SecureUML (Basin et al., 2006, 2009) is one of those techniques that adapt the principles of RBAC and offer a way to model and specify an access control policy. SecureUML provides a security profile extending UML, and applies OCL to define authorization constraints. It appears a good choice to us since it has most of the concepts needed to sketch a security policy using RBAC. Besides, SecureUML is a model-driven approach applying UML diagrams to represent the structural features of an IS, which is coherent with our FMDE approach and the usage of B and UML together for a formal definition of the IS.

By mixing security engineering and model-driven software development, security requirements can be taken into account at a high level of abstraction. Basin et al. (2009) state that “in this way, it becomes possible to develop security aware applications that are designed with the goal of preventing violations of a security policy”. Further works on SecureUML propose to generate access control infrastructures from SecureUML models and thereby enable a technology independent development of secure systems, which would prevent errors during the realization of access control policies. Figure 2.2 is a UML class diagram representing functional concerns (white classes), to which a SecureUML model is associated for the RBAC rules (grey shaded classes).

This simple model is inspired by a medical IS dealing with patients, doctors, hospitals and
medical records. In this model we suppose that an instance of class *DoctorUser* refers to a user who is assigned to role *Doctor*. Permission *Doctor_Perm* grants a doctor the following actions on a medical record: (i) read attributes *data* and *Valid*, (ii) modify attribute *data*, and (iii) call operation *Validate*. A natural way to deal with authorization constraints in SecureUML is to use OCL. Let us consider, for example, that doctors have the ability to manage only medical records of patients that are admitted in their hospitals. This can be defined by the following OCL expression in the context of permission *Doctor_Perm*.

<figure><img src="image_26.png" /><figcaption>Figure 2.2: Functional model enriched by RBAC rules</figcaption></figure>

context Doctor_Perm inv:
session.currentUser.hospital = medicalRecord patient.currentHospital

Expression `session.currentUser` refers to the currently connected user, and as the permission is assigned to role `doctor`, it can be deduced that the user is an instance of class `DoctorUser`. This constraint navigates through the functional model to retrieve the patient associated to the medical record, and his/her current hospital. It also retrieves the doctor user corresponding to the user asking to access the medical record and retrieves his/her associated hospital. Finally, the constraint compares these two hospitals.

### 2.1.3 V&V of RBAC policies

Verification and Validation (V&V) of access-control policies have been studied for a long time. Numerous tools exist to ensure these tasks at an implementation level. For example, Sarna-Starosta and Stoller (2004) translate a Security-Enhanced Linux (SELinux) policy into a logic
program and perform queries on this program to verify information flow, integrity properties and separation of duty. The shortcoming of these tools is that they only provide a static analysis focusing on the security policy, without taking into account its relationship with an application or a database. Moreover, they are anchored at the implementation level and hence they are platform-dependent, which is not convenient if the application or the policy must be adapted, corrected or maintained.

### 2.1.3.1 UMLSec

Jürjens et al. (2005) advocate for an analysis of permissions and security related topics at an early design stage and provide the UMLsec profile (Jürjens, 2010). The corresponding models use UML class and sequence diagrams, decorated with stereotypes and tagged-values to express permissions. The authors verify the conformance between the permissions' model and the system's information flow. In a similar perspective, the Rubacon tool (Höhn and Jürjens, 2008) aims at verifying that systems configurations comply with security rules. The rules and their underlying permissions are defined by a UML class diagram including data extracted from existing applications. Access-control rules are then evaluated by a Prolog analyser on a given instance of the UML model in order to verify permissions, prohibitions and SoD constraints.

Other tools support UMLSec, such as Carisma tool and its predecessor UMLsecTool. However, these tools do not allow to sequence actions or to check whether a given sequence is permitted. Matulevicius and Dumas (2010) performed a comparison of UMLsec and SecureUML and studied possible transformations between them. One of their conclusions is that UMLsec does not cover the notion of authorisation constraint, which is a central concept in our works.

### 2.1.3.2 OCL-based verification

The Object Constraint Language (Warmer and Kleppe, 1999) is part of UML and allows the specification of invariant constraints on a class diagram as well as pre- and post-conditions of methods. The USE tool (Gogolla et al., 2007) takes as input an object diagram and an OCL constraint. It checks whether the constraint holds on the given object diagram. The tool includes a random generator of object diagrams, and the definition of a sequence of actions creating object diagrams, where pre- and post-conditions can be checked. Sohr et al. (2008) have adapted this tool for the analysis of security policies. Their work is focused on the security aspects, i.e. users, roles, sessions and permissions, constrained with OCL assertions, and takes into account functional information by adding some attributes to the concept of users. For example, if a constraint states that the doctor accessing medical information of a patient must be linked to the hospital of the patient, therefore attribute currentHospital should be added to the definition of users. Unfortunately such extensions of the security model do not really scale up, because they duplicate information included in the functional model. In (Sohr et al., 2008) V&V are done based on object diagrams: the diagram is given to the tool, and the tool checks which constraints are violated. The object diagram can be user-defined, randomly generated, or
resulting from a sequence of actions applying a pre-defined action language.

Other works have addressed the validation of security policies using UML and OCL. For example, Ahn and Hu (2007) present an approach using UML class diagrams, a language dedicated to the specification of role-based authorisation constraints (called RCL2000), and OCL to validate SoD constraints. The approach also verifies the constraints given object diagrams. One important limitation of these techniques is that they do not address realistic functional operations. There is no side effect in OCL pre- and post- conditions, which means that the reachability of a given object diagram is not attested. Their V&V start from a given object diagram, but the latter may not be relevant if it is not produced by a valid sequence of functional operations.

### 2.1.3.3 Applying a formal language

Several formal languages have been adopted to verify the correctness of RBAC variants. A significant amount of works has been carried out using Alloy (Jackson, 2002) and Z (Spivey, 1992). Z has mostly been used to specify RBAC concepts at the meta-level, for example as given in (Yuan et al., 2006); and Alloy has been applied to define and verify security policies at a modeling level. The advantage of Alloy in comparison with other approaches, including semi-formal techniques (e.g. OCL, UML), is that Alloy Analyzer is applied to search instances satisfying complex set of predicates (Power et al., 2010). Alloy offers two kinds of automated analysis i.e., simulation and checking. In simulation, operations are evaluated to compute resulting states, and check that they conform to invariant properties. In checking, Alloy attempts to generate instances of a data structure up to a given (small) maximum size, and can identify counterexamples which do not satisfy a given property. The types of answers that Alloy provides are: "this property always holds for problems up to size X" or "this property does not always hold, and here is a counter example".

Zao et al. (2003) applied Alloy as a constraint analyzer to check inconsistencies among RBAC policies. The authors focus on static properties of the security model and do not take into account evolutions of its state. Schaad and Moffett (2002) address administration tasks of RBAC and arbitrary apply changes to a given model that may result in conflicting situations which may introduce security flaws. Yu et al. (2009) propose scenarios in terms of state transitions to uncover violations in security policies. In this approach, all operation calls take the form of scenarios and a system state is a configuration of objects. Using this technique, one can analyze role activation (and deactivation) and SoD constraints as well. In (Toahchoodee et al., 2009a), functional and security models are merged into a single UML model which is translated into Alloy. Alloy can then be used to find a state which breaks a given property. These properties are mainly of static nature, i.e. they focus on the identification of a state that breaks a property, and do not look for sequences of actions leading to such a state. Nevertheless, Alloy can take into account the behaviour of the actions of the model, and we believe it has the potential to perform such dynamic analyses.
#### 2.1.3.4 SecureMova

The tools presented so far, based on UML, OCL and Alloy, only address the validation of security models, e.g. addressing SoD properties. Most of them do not consider constraints which involve elements of the functional model, and hence they do not consider evolutions of the state of the functional model. Basin et al. (2009) report on SecureMova, a tool which supports SecureUML. The tool allows a designer to create a functional diagram, i.e. a class diagram, and to relate it to permission rules. Constraints can be attached to permissions and may refer to elements of the functional diagram. With SecureMova it is possible to ask questions about a given state, i.e. a given object diagram. These questions are called queries; they return authorised actions for a given role, or a given user. They can also investigate on overlapping permissions, i.e. permissions which have a common set of associated actions. Unfortunately, all examples discussed in (Basin et al., 2009) are of static nature. In fact, it is not possible to sequence actions (either administrative or functional) or to verify that a given sequence is permitted (or not) by the combination of the security and functional models. In the next sections, we will see that a thorough validation of a security policy which includes contextual constraints must also take into account evolutions of the state of the functional model.

### 2.1.4 Discussion

Model-Driven Security advocates for the separation of concerns principle in order to ensure modularity and reduce complexity. This is often achieved by isolating functional and security requirements; which allows one to define, verify and implement the various concerns separately. However, in Information Systems, contextual information may also be taken into account when granting permissions. This contextual information may correspond to the current state of the IS, or to the history of interactions with the system. This has led to the notion of authorisation constraint in SecureUML (Basin et al., 2006), combining functional and security concerns together. This notion reveals therefore the drawback of isolating concerns, and shows the need to align functional and security models in order to validate their interactions. There has been a lot of work on the validation of security policies. Some of these works have an associated tool support. In our work, we are mainly concerned with the V&V of security policies involving authorisation constraints. Therefore, we need tools that can take into account both functional and security aspects in their analyses. Moreover, as will be seen in the next sections, evolutions of the functional state of an information system may change the value of an authorisation constraint. It is thus necessary to consider tools which take into account dynamic aspects of the secure information system. Looking at related work, we did not find approaches which combine the dynamic analysis of both functional and security models, with the support for authorisation constraints.

The constraint of Figure 2.2 states that: "If a doctor wants to modify the medical record of a given patient, he/she must belong to the same hospital as the patient". Let us now consider a malicious doctor, who wants to modify the information of a patient in another hospital. Since the
patient and the doctor belong to different hospitals, the doctor will not be authorised to access
this information. In order to validate the rules of the security policy, one may try several typical
situations and query about the permitted/forbidden actions. Using a tool such as SecureMova,
one would provide an object diagram od₁ with one doctor and one patient linked to two different
hospitals, and query if the doctor may perform action on the patient's medical record.
The tool would answer that the doctor is not authorised to perform this action. Further validation
of this security policy should explore dynamic aspects of the policy. For example, is it possible
for this malicious doctor to eventually modify the patient's information? Using only static
tools, one can check that, given an object diagram od₂ where the malicious doctor belongs to
the same hospital as the patient, he will be granted this access. The next question to investigate
is: *does there exist a sequence of actions which leads a malicious doctor to belong to the same
hospital as the patient?* This requires to animate a sequence of actions which leads from od₁
to od₂. Such a sequence will presumably call an intermediate operation joinHospital which
links the malicious doctor to the hospital of the patient. Here dynamic analyses would allow
one to identify these intermediate actions and check which roles have permissions to perform
these actions. Another way to group the malicious doctor and the patient in the same hospital
is to transfer the patient in the hospital of the doctor. In this second sequence, one should
investigate who has the permission to perform such a transfer. This simple example shows
that the validation of a security policy may require dynamic analyses to identify sequences of
actions leading to an unwanted state. Moreover, these sequences of actions are not restricted
to the standard RBAC functions and may refer to operations defined in the functional model.
This is actually the case when constraints referring to the functional model are expressed on
permissions. Current tools, such as the ones presented in this section, which focus on static
queries or on the dynamic execution of the sole RBAC functions are not sufficient to perform
such dynamic investigations.

## 2.2 B4MSecure

### 2.2.1 Overview

In order to address authorisation constraints in MDS and apply dynamic analysis of the IS,
we have developed the B4MSecure platform<fnref n="1" /> (Akram Idani and Ledru, 2015). The tool is
intended to model the Information System as a whole by covering its functional description,
and its security policy. The supporting models are built on UML for the functional concerns
and SecureUML for the access control rules. A formal B specification is generated from these
models, allowing one to formally reason about the various IS concerns: functional and security
models can be first validated separately, and then integrated in order to verify their interactions.

B4MSecure (Figure 2.3) is built on an MDE architecture in which the input models are
UML class diagrams that are extended with the SecureUML profile. The extraction of B spec-

<footnote n="1">¹ B4MSecure: B for Modeling Secure Information Systems</footnote>
ifications applies a catalog of transformation rules that are defined at a meta-level. The ideas
behind the tool are inspired by existing software products, such as popular commercial database
management systems (e.g. Oracle, Sybase) or webservers (e.g. JBoss, Tomcat). The available
implementations of RBAC act like a filter which intercepts a user request to a resource in order
to permit or deny the access to associated functional actions (e.g. transactions on databases,
file operations, etc). The tool is based on the same principles, but at a modeling level. Each
functional operation is encapsulated in a secure operation checking that the current user has the
required authorizations. The usage of B is motivated by the fact that several tools have been
built to translate UML models into B specifications as discussed in Chapter 1. Indeed, the trans-
lation of the functional model can be done by executing a configuration of UML-to-B rules that
are issued from our approach for multiple transformations. Regarding security models, Sohr
et al. (2008) have already proved that it can be specified in UML+OCL. Since the B language
is based on the same principles as OCL (first order predicate logic and set theory), it is possible
to propose a similar translation of the security model into B specifications.

<figure><img src="image_27.png" /><figcaption>Figure 2.3: Formal V&V activities of functional and security models</figcaption></figure>

The B specifications produced from both security and functional models can therefore be
analyzed using either animation tools such as ProB (Leuschel and Butler, 2003) or proof tools
such as Atelier B. ProB also includes model-checking facilities which can be of interest to
search for malicious sequences of operations. The functional B specification in the left side of
Figure 2.3 applies a classical UML-to-B translation. The lower side of Figure 2.3 represents the formal specification produced from the security model and which is intended to control the functional B operations. Playing scenarios is done by animating the secured operations, which gives only access to the authorized functional operations. This approach allows the validation of the functional model as well as the security policy. In fact, animation of an authorized operation modifies the state of the functional model and hence allows the analyst to validate both models.

Terms “shallow embedding” and “deep embedding” (Wildmoser and Nipkow, 2004) are often used to describe mappings between formalisms. The first notion means a direct translation from a source model into a target model, while the second notion means that the mapping leads to structures that represent data types. Most UML-to-B approaches adopted the “shallow embedding” approach. Indeed, they apply a set of rules to ensure a direct translation from UML into B. Unlike “deep embedding”, this aims to be more straightforward because the resulting formal specifications explicitly include the elements of the source model. The “deep embedding” approach is commonly used to translate elements of a meta-model. To summarize, B4MSecure produces two B models:

1. A first B model issued from a UML class diagram, applying a “shallow embedding” approach. This model can be enriched with invariants and operations and the correctness of the functional model can be established.

2. A second B model that represents the security policy and defines the access to the functional entities. This model is generated through a “deep embedding” approach. We translate an access control meta-model built on the principles of RBAC, and then we inject in it the B specification of a specific access control model.

## 2.2.2 Functional model

To illustrate the B4MSecure approach, we consider the UML class diagram of Figure 2.4, inspired by (Bandara et al., 2010). This model represents functional concerns of a banking IS: it defines customers (class *Customer*) in relation with their accounts (class *Account*).

An account is characterized by its balance (attribute *balance*), the authorized overdraft (attribute *overdraft*) and a unique identifier (attribute *IBAN*). A customer may have a credit card (class *CreditCard*), allowing him/her to withdraw cash. Operation *transferFunds* allows one to transfer an amount of money (parameter *m*) from the current account to any account defined with an *IBAN* number (parameter *NB*). Operations *withdrawCash* and *depositFunds* allow respectively to withdraw or to deposit money. To withdraw an amount of money, the customer must present an active credit card (attribute *inLine* must be equal to *true*).

### 2.2.2.1 Translating the structural features

In this subsection, we are not going to discuss existing UML-to-B approaches. For more details about these approaches, we refer the reader to the previous chapter or to Idani, A. et al. (2010b).
<figure><img src="image_28.png" /><figcaption>Figure 2.4: UML Class Diagram – Functional Model</figcaption></figure>

Nevertheless, we will focus on the translation set up in B4MSecure, in order to give an overview of the B specifications produced by the tool.

In B, abstract sets represent an abstraction of a set of objects from the real world. As this definition is close to the notion of class in UML, it is used by all UML-to-B approaches to formalize UML classes. The main objective of this translation is to allow the definition of constructors and destructors of class instances. For example, class *Customer* produces:

(i) Abstract set<fnref n="2" /> *CUSTOMER* defining the set of possible instances;

(ii) Variable<fnref n="3" /> *Customer* defining existing instances; and

(iii) Invariant<fnref n="4" />: *Customer* ⊆ *CUSTOMER*.

Regarding class attributes, they are translated into B functions relating the set of existing instances to the type of the attribute. The resulting functions depend on the attribute character: mandatory or optional, unique or not unique, single or multiple valued. For example, attribute *IBAN* of class *Account* is single-valued, mandatory and unique. It is therefore translated into a total injection. Table 2.1 gives the various translations of single-valued attributes.

<table><caption>Table 2.1: B relations extracted from single-valued attributes</caption><thead><tr><th></th><th>Optional</th><th>Mandatory</th></tr></thead><tbody><tr><td>Unique</td><td>↔</td><td>→</td></tr><tr><td>Not unique</td><td>↔</td><td>→</td></tr></tbody></table>

The translation of associations follows the same principle. Indeed, each association leads to a functional relation that depends on the multiplicities of the two ends of the association. For

<footnote n="2">² clause SETS.</footnote>

<footnote n="3">³ clause VARIABLES.</footnote>

<footnote n="4">⁴ clause INVARIANT.</footnote>
example, association *AccountOwner* is translated into a partial surjective function since its multiplicities are 0..1 and 1..*. Figure 2.5 presents the typing invariants that are automatically produced by B4MSecure from the example of Figure 2.4.

<figure><img src="image_29.png" /><figcaption>Figure 2.5: Structural invariants produced by B4MSecure</figcaption></figure>

### 2.2.2.2 Extraction of basic operations

The B specifications produced by B4MSecure from a given class diagram are intended to be animated using an animation tool such as ProB (Leuschel and Butler, 2003). This allows one to see the evolution of the IS and observe the impact that an execution scenario could have on the functional state. Thus, B4MSecure generates all basic operations such as creation/deletion of class instances, creation/deletion of links between these instances, getters/setters of attributes, and getters/setters of links. In general, these operations are correct by construction, meaning that they do not violate the generated typing invariants. In fact, the proof of correctness of the functional model means that basic operations preserve the multiplicities of the associations as well as the character of attributes. This proof is true by construction for most basic operations, but needs to be consolidated for some deletion operations.

For example, deleting an instance of class *Customer* is only possible if this instance is not linked to an instance of class *CreditCard*. Several special cases exist, and are not all covered by the translation process in B. In this case the specifications must be updated or completed by the analyst. Figure 2.6 gives an example of a basic operation that is generated by B4MSecure. It is a creation operation of class *Account*. This operation preserves, on the one hand, the mandatory character of attribute *IBAN* because a value is assigned to the attribute when the object is created, and on the other hand, the uniqueness of this attribute thanks to pre-condition:

$$Account\_IBANValue \notin ran(Account\_IBAN)$$

The operation also takes into account the default values of attributes *balance* and *overdraft*; they are respectively initialized to 0 and -100.
<figure><img src="image_30.png" /><figcaption>Figure 2.6: Basic creator generated by B4MSecure</figcaption></figure>

### 2.2.2.3 Enhancing the functional model

Information Systems often include constraints, especially integrity constraints relating to the functional model. These constraints must be taken into account when defining the various use cases of the IS. As the verification activities are specific to each IS, the B model produced automatically must be completed manually by adding new invariants and operations. Let's consider for example, that the balance of an account must be greater than (or equal) to the overdraft of the account. The analyst should therefore add the following invariant to the functional B machine:

<figure><img src="image_31.png" /><figcaption>Figure 2.7: Invariant constraints of the functional model</figcaption></figure>

After adding this invariant to the specifications, the analyst must check the proof obligations (POs) generated by AtelierB and correct the underlying B specifications. This would identify the basic operations that violate the user defined invariants and correct them accordingly. Consider for example, the modification operation of attribute *balance* that is presented in Figure 2.8. In order to correct this operation, the analyst must strengthen its precondition by adding the following predicate:

<figure><img src="image_32.png" /></figure>

The enhancement of the functional model is done by adding invariant properties and the underlying preconditions in order to keep correct the basic operations. The user-defined operations, such as operations *transferFunds* and *withdrawCash* of class *Account*, must also be defined. Figure 2.9 presents the B specification of operation *transferFunds*. It takes an account number (parameter *N*) and a positive amount (parameter *m*) and performs the transfer of funds if the following conditions are met: the current account and the beneficiary account are held
by customers, *N* corresponds to an existing account other than the current account, and the
authorized overdraft will not be exceeded by this transfer.

The B specifications issued from our functional class diagram are about 300 lines of B
code from which 80 POs were generated by AtelierB for typing invariants. Among these POs,
4 were proved interactively. Furthermore, adding invariant properties produced a total of 94
proof obligations of which only 18 did not pass the automatic prover. Therefore we introduced
preconditions to some basic operations in order to have a formal model preserving all its invari-
ants. This formal verification effort may vary depending on the complexity of the IS; for this
simple example the verification task was reasonably easy to do.

```
Account_SetBalance(Instance, Account_balanceValue) ==
PRE
    Instance ∈ Account ∧ Account_balanceValue ∈ ℤ
    ∧ (Instance ↦ Account_balanceValue) /∈ Account_balance
THEN
    Account_balance(Instance) := Account_balanceValue
END;
```

<caption>Figure 2.8: Basic setter of class Account</caption>

```
Account_transferFunds(Instance, N, m) ==
PRE
    Instance ∈ Account ∧ N ∈ N ∧ m ∈ N₁
    ∧ AccountOwner[{Instance}] ≠ ∅
    ∧ N ∈ ran({Instance} ≪ AccountaltyIBAN)
    ∧ AccountOwner[{AccountityIBAN⁻¹(N)}] ≠ ∅
    ∧ Account_balance(Instance) - m ≥ Account_overdraft(Instance)
THEN
    Account_balance :=
        {(Instance ↦ (Account_balance(Instance) - m))}
        ∪ {(Account IBAN⁻¹(N) ↦ (Account_balance(Account IBAN⁻¹(N)) + m))}
        ∪ ({Instance, Account IBAN⁻¹(N)} ≪ Account_balance)
END;
```

<caption>Figure 2.9: Operation transferFunds of class Account</caption>

### 2.2.3 Security model

The approach adopted in B4MSecure is a model-driven approach that favours the separation
of concerns principle. The objective is to first allow reasoning about the correctness of the
functional model without any security concern, and afterwards, to analyze the security model independently of the functional concerns, and finally to check the connections between both models.

UML and SecureUML models can be designed using the graphical editor of TopCased<fnref n="5" /> or that of Eclipse Papyrus<fnref n="6" />. Thus, the security policy concrete syntax uses classes and stereotypes to refer to RBAC concepts. Figure 2.10 is a SecureUML model associated to the class diagram of Figure 2.4.

<figure><img src="image_33.png" /><figcaption>Figure 2.10: SecureUML model in B4MSecure</figcaption></figure>

This model defines three roles: *CustomerUser*, *AccountManager* and *ATM*. They respectively represent the customer of the system, the financial manager in charge of the bank's customers, and the automatic teller machine. The underlying access control rules are:

1. Customers can read their personal data (permission *CustomerUserPerm1*), transfer money, deposit and withdraw cash (permission *CustomerUserPerm2*);

2. The account manager, in charge of the clients, has a full access (read and write) on class *Customer* (permission *AccountManagerPerm1*). He/She can thus create customers, read or modify their data. However, his/her rights on class *Account* are limited to the creation of new accounts (permission *AccountManagerPerm2*);

<footnote n="5">⁵ http://www.topcased.org</footnote>

<footnote n="6">⁶ https://www.eclipse.org/papyrus/</footnote>
3. Role ATM has the permission to call activation and deactivation operations of class *CreditCard* (permission *ATMPerm*).

An authorization constraint is associated to permissions *CustomerUserPerm1* and *CustomerUserPerm2* in order to grant the corresponding actions to the sole holder of the account on which they are invoked. In this security policy, the account manager has no access, neither read nor write, to the attributes of class *Account*. We also consider three users and a DSD constraint as presented in Figure 2.11. *Bob* is assigned to role *AccountManager*, and *Paul* and *Martin* are possible users without any assigned role. Note that the assignment of *Paul* and *Martin* to role *CustomerUser* is done when these two users are created as instances of the functional class *Customer*. In fact, in some cases functional classes refer to roles and vice-versa. Hence, we consider that set *CUSTOMER* of possible instances is a subset of set *USERS* that represents possible users of the system. Finally, the DSD constraint of Figure 2.11 means that a user cannot log in the system by being both *AccountManager* and *CustomerUser* in the same session.

<figure><img src="image_34.png" /><figcaption>Figure 2.11: Users and Role assignment</figcaption></figure>

The B specification issued from the SecureUML model is dedicated to grant or forbid func-
tional operations given the set of roles that are activated by a user. For example, if *Paul* is a
*CustomerUser*, therefore he can only read his personal data by calling basic getters of class
*Customer*. The other operations (modification, creation, etc) are forbidden to him. In order
to translate the security model, our approach follows two steps: (i) propose a “stable” formal-
ization of a RBAC meta-model, then (ii) translate a given security model and inject it into the
formalization of the meta-model. Each operation of the functional model is encapsulated in a
secure operation checking that the current user is allowed (or not) to call this operation.

2.2.3.1 Formal modeling of user assignments and role activation

Figure 2.12 presents the structural part of the B model (Machine *UserAssignments*) that defines the right side for Figure 2.1. It refers to: *ROLES*, *USERS* and *SESSIONS*. The assignment of roles to users is defined with relation *roleOf*. Contrary to users and roles, which are explicitly represented with sets, sessions are defined by means of a relation between users and roles. We consider that a user cannot open several sessions in the system. When a user *u* belongs to the domain of relation *Session*, thus a session is created for him and *Session[{u}]* gives the
set of roles that are activated by user *u*. Other RBAC concepts, such as role hierarchy, static separation of duties and dynamic separation of duties, are also defined by this specification. Variable *currentUser* is useful during the animation of the model because it allows us to identify the operations that are being executed by a given user. Note that we do not consider concurrent accesses during animation.

<figure><img src="image_35.png" /><figcaption>Figure 2.12: Users assignment: typing invariants</figcaption></figure>

Figure 2.13 provides some security invariants of machine *UserAssignments*. For example, cycles in a role hierarchy are not allowed even if this is graphically possible. In our approach, B4MSecure creates the valuations of the various data structures and then ProB is applied to verify that security invariants are preserved. The second invariant guarantees the conformance between role assignments and role activations. It means that, in a session, a user can only activate roles among those that are assigned to him. The other invariants guarantee SSD and DSD constraints. They are somehow redundant: the former refers to relation *roleOf* and the latter refers to relation *Session*.

Machine *UserAssignments* provides several utility operations that are useful during the animation. Figure 2.14 gives the B specifications of operations *safeConnect*, *addSafeRole* and *setCurrentUser*. Operation *safeConnect* creates a session to a given user in which a set of roles is activated. This operation is done under several conditions: (i) the user is not concerned by any existing session, (ii) if a role *r*₁ is a super-role of a role *r*₂, therefore the user can activate *r*₁ or *r*₂ but not both of them {*r*₁, *r*₂}, and (iii) the DSD constraints are preserved. Operation *addSafeRole* adds a new role to a given user and preserves SSD constraints. This operation is useful when roles are created dynamically because of the evolution of the functional state. For example when a customer is created, role *CustomerUser* must be added to the corresponding user. Operation *setCurrentUser* selects the user who will execute the system.
<figure><img src="image_36.png" /><figcaption>Figure 2.13: Users assignment: security invariants</figcaption></figure>

### 2.2.3.2 Formal modeling of permission assignments

To formally define permissions, we first apply a deep embedding approach to the entities of the model that are associated to permissions. Machine *RBAC Model* of Figure 2.15 gives an excerpt of the B data structures that are generated by B4MSecure. Sets *ENTITIES*, *Attributes*, *Operations* and *KindsOfAtt* represent concepts of the meta-model dealing with the functional concerns. For example, set *ENTITIES* represents classes of the functional model. Relations between these sets are: *AttributeKind* (private or public), *AttributeOf* (for class attributes), *OperationOf* (for class operations), *constructorOf* (for class constructors), *destructorOf* (for class deletion), *setterOf* (for attribute setters) and *getterOf* (for attribute getters). The other data structures of machine *RBAC Model* define RBAC concerns. The machine also includes the functional model and machine *UserAssignments*, and promotes operations *safeConnect*, *disconnect* and * CurrentUser*.

Relation *isPermitted* defines pairs $(r \mapsto o)$ that are calculated from the RBAC model in order to establish for every role *r* and operation *o* whether *r* is allowed to call *o* or not. For example, *CustomerUserPerm1* leads to two pairs $(CustomerUser \mapsto Customer_GetName)$ and $(CustomerUser \mapsto Customer_GetAddress)$. Indeed, this permission is related to role *Cus-
safeConnect(user, roleSet) =
PRE
  user ∈ USERS ∧ user /∈ dom脂(Session)
  ∧ roleSet ∈ P₁ (ROLES) ∧ roleSet ⊆ roleOf(user)
  /* avoid hierarchical redundancy in the roleSet */
  ∧ ∀ (r1,r2).(r1 ∈ roleSet ∧ r2 ∈ roleSet ∧ r1 ≠ r2
    ⇒ r2 /∈ closure1 (Roles_Hierarchy)[{r1}])
  /* avoid DSD violation */
  ∧ ∀ rs.(rs ∈ P₁ (ROLES) ∧ rs ∈ dom(DSD_mutex) ⇒
        card((Roles_Hierarchy)⁺[roleSet] ∪ roleSet ∩ rs) < DSD_mutex(rs)
  )
THEN
  Session := Session ∪ ({user} × roleSet)
END;

addRoleSafe(user, role) =
LET newRoles BE newRoles = roleOf(user) ∪ {role} IN
PRE
  user ∈ USERS
  ∧ role ∈ ROLES ∧ role /∈ (roleOf(user) ∪ (Roles_Hierarchy⁻¹)⁺[roleOf(user)])
  /* avoid SSD violation */
  ∧ ∀ rs.(rs ∈ P₁ (ROLES) ∧ rs ∈ dom(SSD_mutex) ⇒
        card(((Roles_Hierarchy)⁺[newRoles] ∪ newRoles) ∩ rs) < SSD_mutex(rs)
  )
THEN
  roleOf := ({user} ≺ roleOf) ∪ ({user ↦→ newRoles})
END
END;

setCurrentUser(user) =
PRE
  user ∈ USERS ∧ user ≠ currentUser ∧ user ∈ dom脂(Session)
THEN
  currentUser := user
END;

<caption>Figure 2.14: Users assignment: utility operations</caption>

tomerUser and refers to an *EntityAction* of type *read*, and to class *Customer*. Two attributes are defined in this class (*Name* and *Address*) and their getters are respectively *Customer_GetName* and *Customer_GetAddress*. The calculation of relation *isPermitted* is carried out in the initiali-
sation clause of machine RBAC_Model based on the other B data of this machine.

MACHINE RBAC_Model
INCLUDES Functional_Model, UserAssignments
PROMOTES safeConnect, disconnect, setCurrentUser
SETS
ENTITIES; Attributes; Operations; KindsOfAtt = {public, private};
PERMISSIONS; ActionsType = {read, create, modify, delete, fullAccess}
CONSTANTS
AttributeKind, AttributeOf, OperationOf,
constructorOf, destructorOf, setterOf, getterOf,
PermissionAssignement, EntityActions, MethodActions,
VARIABLES
isPermitted
PROPERTIES
AttributeKind ∈ Attributes → KindsOfAtt ∧
AttributeOf ∈ Attributes → ENTITIES ∧
OperationOf ∈ Operations → ENTITIES ∧
constructorOf ∈ Operations ↦→ ENTITIES ∧
declassOf ∈ Operations ↦→ ENTITIES ∧
setterOf ∈ Operations ↦→ Attributes ∧
getterOf ∈ Operations ↦→ Attributes ∧
setterOf ∩ getterOf = ∅ ∧
PermissionAssignement ∈ PERMISSIONS → (ROLES × ENTITIES) ∧
EntityActions ∈ PERMISSIONS ↦→ P (ActionsType) ∧
MethodActions ∈ PERMISSIONS ↦→ P (Operations) ∧
INVARIANT
isPermitted ∈ ROLES ↔ Operations

<caption>Figure 2.15: Structural part of RBAC machine</caption>

### 2.2.3.3 Formal modeling of secure operations

B4MSecure produces for every functional operation, a secured operation that verifies (using a security guard) whether the current user is allowed to call the functional operation. The secure operation also verifies the authorization constraints, if they are defined in the underlying permissions, and updates the assignment of roles when required.

Figure 2.16 shows the secure operations associated to Account_transferFunds and Customer_NEW. The security guard is defined in clause SELECT. It verifies that the functional operation belongs to set `isPermitted(currentRoles]`, where definition `currentRoles` refers to the roles activated by `currentUser` (in a session) as well as their super-roles:
```
currentRoles ==
    Session[{currentUser}] ∪
    ran Session[{currentUser}] ⊳ (Roles_Hierarchy)⁺
```

```
secureAccount_transferFunds(aAccount, NB, m) =
PRE
    aAccount ∈ Account ∧ NB ∈ N ∧ m ∈ N₁ [∧...]
THEN
    SELECT
        Account_transferFunds_ ∈ isPermitted(currentRoles)
        ∧ (CustomerUser ∈ currentRoles ⇒ AccountOwner(aAccount) = currentUser)
THEN
    Account_transferFunds(aAccount, NB, m)
END
END;
```

```
secure Customer_NEW(aCustomer, theAccount) =
PRE
    aCustomer ∈ CUSTOMER ∧ theAccount ∈ F(Account) [∧...]
THEN
    SELECT
        Customer_NEW_ ∈ isPermitted(currentRoles)
        THEN
            Customer_NEW(aCustomer, theAccount) ||
            addRoleSafe(aCustomer, CustomerUser)
        END
    END;
```

<caption>Figure 2.16: Operational part of RBAC machine</caption>

The security guard of `secureAccount_transferFunds` is strengthened with the authorization constraint of permission `CustomerUserPerm2`. For every permission `p` associated to a role `r` and a constraint `c`, the tool adds guard ($r \in currentRoles \Rightarrow c$) to all operations that are concerned with `p`. Note that in the graphical model the constraint is directly written in B. In this case the constraint is: `AccountOwner(aAccount) = currentUser`. Regarding operation `secure Customer_NEW`, it is not concerned with an authorization constraint. But, as class `Customer` and role `CustomerUser` are aligned, the operation applies `addSafeRole` to update relation `roleOf` when a customer is created.

These two operations show how B4MSecure takes into account the relationship between functional and security models. In one case the permission is granted to users when some functional conditions hold and in the other case the creation of some objects may grant new permissions to users since they may acquire additional roles.
## 2.3 Animation and dynamic analyses

The example in the previous section highlights the need for dynamic analyses of both functional and security models. When the security policy refers to functional elements, a dynamic analysis should not only cover the RBAC functions, but also take into account the behaviour of the functional model. Dynamic analyses can take two forms: test and model-checking. Tests correspond to the execution of a sequence of actions on the various models, or on their implementations. The test sequence is either defined by the security policy designer, possibly on the basis of use cases, or it may be the output of a test generation tool.

However, tests can only check a limited number of behaviours. When absolute guarantees are required, such as ensuring that all threats are handled, verification techniques, such as model-checking and theorem proving, should be considered. Theorem proving can show that constraints are satisfiable, or establish that some property, like SoD, is an invariant of the model. However, as we are interested by the reachability of particular states that may open breaches and favour security threats, theorem proving is not an efficient technique. We apply theorem proving to guarantee that the functional model is correct regarding its invariants as discussed in Section 2.2.2, and also to guarantee that the pre-established security operations are correct with respect to the RBAC constraints (i.e. Role hierarchy, SSD, DSD, etc).

### 2.3.1 Animation in B4MSecure

In order to favour dynamic analyses in one integrated framework, B4MSecure applies ProB Java API as presented in Figure 2.17.

<figure><img src="image_37.png" /><figcaption>Figure 2.17: Animation in B4MSecure</figcaption></figure>
Note that the B specifications that are extracted by the tool can also be verified outside B4MSecure using ProB standalone. The State View (bottom-left) gives the values of the B variables in the current state, i.e. after animating the sequence of the History View (bottom-right). The Execution View (top-right) shows the B operations that can be triggered in the current state. The content of these views is computed by the Java API of ProB; B4MSecure just provides some convenient actions to ensure animation and/or model-checking via the API.

Figure 2.17 shows a sequence of functional operations that creates customers Paul and Martin, as well as their respective accounts *cpt1* and *cpt2*. An amount of 200€ is added to Martin's account and then 300€ are transferred from this account to Paul's account.

<figure><img src="image_38.png" /><figcaption>Figure 2.18: Valid functional sequence and its target state</figcaption></figure>

The scenario of Figure 2.18 that is animated in B4MSecure (Figure 2.17) corresponds to a normal use case of the IS. Playing with functional scenarios shows that use cases are feasible with the current specification, and helps identify missing steps in the use cases or the specification. A similar animation can be performed by calling the secured version of the use case (machine *RBAC_Model*). This eases the understanding and validation of the security policy and shows that the security policy does not prevent the execution of functional use cases.

### 2.3.2 Testing the security policy

Having an operational formal model of the security policy, it becomes possible to carry out security tests, by testing permissions and/or prohibitions. For example, when a test consists of reading an object, one can simply check that the getter (or a reading operation) is allowed (or not) in a given state. Several testing objectives can be addressed when testing a secure operation: with a role that does not have access to this operation, without satisfying an authorization constraint, or outside the operation precondition.

In order to perform security tests, we structure the animation of secure operations, according to their permissions. We consider three parts: preamble, nominal/robustness and call. The “preamble” sequence leads to a state allowing the execution of a permitted operation. The
"nominal/robustness" varies the users and the roles that are concerned by the permission granting access to the operation. The "nominal" sequence corresponds to a positive test, and sequence "robustness" presents a slight variation compared to the nominal case, which must lead to a failure (negative test). Finally, the "call" part applies the operation that we want to test in order to see that it can be effectively called if it is authorized. For example, if we want to test operation *depositFunds*, granted by permission *CustomerUserPerm2* to role *CustomerUser*, we consider the sequences of Figure 2.19.

<figure><img src="image_39.png" /><figcaption>Figure 2.19: Structuring security tests</figcaption></figure>

Positive tests verify that a user can execute the permitted operation if he/she activates the corresponding role and satisfies the functional preconditions as well as the authorization constraint. For example, sequence « preamble ; nominal ; call » is a positive test and the resulting state is represented with the object diagram of Figure 2.20. In this sequence, Paul deposits money into his own account.

<figure><img src="image_40.png" /><figcaption>Figure 2.20: Initial object diagram</figcaption></figure>

Positive tests that fail during the animation may reveal some defects in the definition of security rules. For example, a use case where the account manager modifies the allowed overdraft of an account should be feasible. However, the following test sequence, which is therefore a positive test, cannot be animated:
```pascal
safeConnect(Bob, {AccountManager});
 CurrentUser(Bob);
secureAccount_NEW(cpt1, 111);
secureAccount_setOverDraft(cpt1, -500)
```

Operation *Account_setOverDraft* is a basic operation, generated by B4MSecure in order to modify the value of attribute *OverDraft* of class *Account*; but there is no permission granting access to this operation. Failure of this test reveals that a permission has been forgotten.

Regarding negative tests, they are close to positive tests, but they invalidate one of the elements of the permission: role, precondition or authorization constraint. Contrary to positive tests, a negative test cannot fully run, since it contains an illegal call to a secure operation. A negative scenario, should not be allowed by the animator. For example, sequence « preamble ; robustness ; call » is a negative test that invalidates the authorization constraint. In this sequence, Martin tries to deposit money into an account that does not belong to him.

### 2.3.3 Attack scenarios

The advantage of theorem proving and testing, discussed in the previous sections, is that when looking for threats, the security analyst has the guarantee that flaws are not issued from invariant violations, but rather from the functional or the security logic. In this sense, the identification of attack scenarios is mainly a validation task, which can be done by model-checking. Indeed, an exhaustive model exploration may exhibit a malicious sequence of operations leading to a given state (where a property holds) from which a bad action may be done.

To show a possible malicious scenario based on our simple example, we start the exploration from a normal state, that of Figure 2.20, reached by sequence « preamble ; nominal ; call ». In this state *Paul* is a customer and owns account *cpt1* whose balance is equal to 500. *Bob* as *AccountManager* cannot execute operations *transferFunds* or *withdrawCash* on *cpt1*. The answer to a static query such as "Is Bob able to transfer funds from Paul's account?" would be NO, since the permission given to a manager on class *Account* only allows instance creation. However, the good question should be "Is there a sequence of operations that can be executed by Bob in order to become able to transfer funds from Paul's account?". To answer the question we use the model-checking feature of ProB to explore the state space and find states that satisfy property: *AccountOwner*(*cpt1*) = *Bob*. We are therefore looking for a sequence of operations executed by Bob allowing him to become the owner of *cpt1*. After finding the state we use ProB to verify whether it is possible to come back into a state where *cpt1* is owned by *Paul*. The objective is to check if the attacker can execute the reverse actions in order to hide his attack.

Sequence of Figure 2.21 has been exhibited by ProB after exploring more than 36000 reachable states. We structure it in four steps. In **step 1** *Bob* adds himself to the system as a customer. As the creation of a customer requires at least one account, *Bob* creates the fictive account *cpt3* and then he calls operation *secureendeNew*. In **step 2**, the attacker becomes the owner of *cpt1*. To this purpose he must first remove the link between *Paul* and *cpt1*.
But, in the functional model a customer must have at least one account, consequently operation `secureendept(Customer, {customer})` is possible only if Paul has another account. For this reason, Bob creates another fictive account `cpt4` and adds it to Paul's accounts. The last action of step 2 reaches the malicious state where Bob is the owner of `cpt1`. Finally, step 3 realizes the attack and step 4 brings the system back to a normal state.

```c
/* step 1: create customer Bob */
safeConnect(Bob, {AccountManager});
 CurrentUser(Bob);
secureAccount_NEW(cpt3, 333);
secureCustomer_NEW(Bob, {cpt3});

/* step 2: get the ownership of Paul's Account */
secureAccount_NEW(cpt4, 444);
secureCustomer_AddAccount(Paul, {cpt4});
secureCustomer RemovingAccount(Paul, {cpt1});
secureCustomer_AddAccount(Bob, {cpt1});

/* step 3: attack */
disConnect(Bob);
safeConnect(Bob, {CustomerUser});
secureAccount TransferFunds(cpt1, 333, 500);

/* step 4: hide the attack */
disConnect(Bob);
safeConnect(Bob, {AccountManager});
secureCustomer RemovingAccount(Bob, {cpt1});
secureCustomer_AddAccount(Paul, {cpt1});
secureCustomer RemovingAccount(Paul, {cpt4});
secureCustomer_Free(Bob)
```

<figure><img src="image_41.png" /><figcaption>Figure 2.22: Malicious state reached after the execution of steps 1 and 2</figcaption></figure>
This malicious scenario can be countered by enhancing the functional model and/or the security model. If the analyst assumes that the flaw is favored by the functional logic, one possible solution would be to introduce the following invariant:

$$ \mathit{Account\_balanceValue} \neq 0 \Rightarrow \mathit{AccountOwner}[\{\mathit{Instance}\}] \neq \emptyset $$

In fact, operation `secure_Customer_RemoveAccount(Paul, {cpt1})` is the dangerous operation. This invariant means that accounts whose balance is not equal to zero must be owned by a customer. By introducing this invariant, several functional operations must be corrected and proved, such as: `Customer_RemoveAccount` and `Account_SetBalance`. In other words, to remove the ownership relation between `cpt1` and `Paul`, the account of `Paul` must be empty.

If the analyst assumes that the flow is favored by the security logic, a possible solution would be to limit the scope of permission `AccountManagerPerm1` because it currently grants a full access to role `AccountManager` on customer's data, including the deletion of his accounts.

## 2.4 Discussion and conclusion

One of the advantages of B4MSecure (Akram Idani and Ledru, 2015) is its extensibility; besides an extension to Event-B has been proposed in (Wakrime et al., 2018) and an extension covering other security features such as organisations and contextual rules has been defined by Yangui (2016). Not only the translation of functional models is built on existing UML-to-B works that are approved by the formal methods community and that are combined together in one unifying framework, but also the translation of RBAC models can be configured leading to various translations. This chapter has been focused on one possible translation providing an overview of our Formal Model-Driven Security approach.

The major motivation behind the tool is that MDS (Basin et al., 2006) advocates for the separation of concerns principle and suggests the validation of functional and security models in isolation. However, access control rules often include authorisation constraints, which requires dynamic analyses dealing with elements of both models. Our proposal is built on the B method and allows the validation and verification of RBAC policies involving constraints. This work has been applied and experimented in several research projects, the major ones are: ANR Selkis (2008-2012) and NExTRegio of IRT Railenium (2015-2019). The first project addresses medical information systems and the second project deals with railway applications.

**ANR Selkis (2008-2012).** The first versions of B4MSecure have been developed during this project, and have involved two PhD students (N. Qamar and M.-A. Labiadh) and two M2 students that I co-supervised with my colleague Y. Ledru. In (Ledru et al., 2015a) we reported on the application of B4MSecure to Res@mu, a case study issued from this project. Res@mu is a medical IS developed by Ifremmont<fnref n="7" />. It supports every stage of a medical urgency, from the

<footnote n="7">⁷ Ifremmont (http://www.ifremmont.com/): Institut Français de recherche en Médecine de Montagne.</footnote>
phone call to an emergency call center, to the management of emergency teams during a mission. The starting point of this study was a set of UML class diagrams and use cases describing the data structures and main functionalities of the IS. These include 77 classes and more than 100 use cases. The application of B4MSecure was focused on 12 classes. We discarded classes that do not influence medical acts, our security target, like those describing rescue vehicles or their base station, or the motivation and circumstances of emergency missions. A total of 34 positive tests and 87 negative test have been defined and played against the models using ProB. They helped us incrementally define the security policy, following a TDD approach. Thanks to these tests, errors have been identified in functional use cases, in the initial version of our access control rules or in manually defined assertions of B models. We believe that the success of these tests gives reasonable guarantees in the quality of our security policy. We have also defined 4 attack scenarios, and several associated variants. They correspond to 7 positive tests and 13 negative ones. They all try to compromise the confidentiality of medical acts. In these scenarios, users with high privileges (e.g. team doctor or regulator) try to get access to the medical acts of a patient by joining the intervention team during or after the intervention. All attacks failed, which increased our confidence in the security policy. These attacks showed the usefulness of protecting not only the security target, but also related classes involved in authorisation constraints. However, the scenarios describing these attacks are generally complex and ProB was not able to compute the enabledness for most of them (18/20 tests), experiencing time-outs or memory errors. We had to break these tests down into smaller test steps that were played in sequence. The next chapter discusses some solutions to these issues, such as combining abstraction and theorem proving, to automate the extraction of attack scenarios.

**NExTRegio (2015-2019).** Papers (Ledru et al., 2019) and (Wakrime et al., 2018) show how B4MSecure has been used in the railway field. During this collaboration with IFSTTAR<fnref n="8" /> and IRT Railenium<fnref n="9" /> we proposed a modelling approach for railway signalling rules being inspired by MDS and IS security. The approach models the agents that perform railway operations and the conditions that must be satisfied before performing these operations. These models are expressed in SecureUML diagrams enhanced with B assertions, and then translated, using B4MSecure, into B machines. ProB is applied to verify the model via model-checking and animation in order to assess the reachability of desired states, and verify the absence of accidents. Furthermore, the approach proceeds by introducing human errors, checking their consequences, and deploying counter-measures. For this case study the separation of concerns principle was useful to define first an uncontrolled model only governed by the laws of physics, where accidents may happen, and second a model controlled by signalling rules, where bad things should not happen. This is similar to the distinction made in secure IS and MDS between data and associated functions, described in a so-called “functional” model, and the permissions that rule the accesses of users to these data, described in a “security” model. Each operation of the un-

<footnote n="8">⁸ IFSTTAR: Institut français des sciences et technologies des transports, de l'aménagement et des réseaux, https://www.ifsttar.fr/</footnote>

<footnote n="9">⁹ IRT Railenium: https://railenium.eu</footnote>
controlled model has a controlled version in the control model. This version adds guards to check the relevant permissions. For example, trains, tracks, lights and their associated operations correspond to the uncontrolled model. Train drivers and traffic agents must follow the rules that constrain the call to these operations, which is a kind of role-based access control. Having this formal specification, the existence of accidents is assimilated to insider threats. Indeed, the verification of signalling rules assumes that users follow the rules, i.e. they only access operations that are permitted, and follow authorisation constraints. These assumptions are not valid in the case of human errors, for example (1) the train driver can overlook an off light and enter a forbidden track portion or (2) the traffic agent can switch on a light ignoring the corresponding safety constraints. Such human errors can be the consequence of tiredness. In 2016, Infrabel, the Belgian railway company, reported that 91 trains (out of 1,3 million) ignored a red light (Infrabel, 2017).
# Chapter 3

## Looking for malicious behaviours

### Contents

<table><tr><td>3.1 Running Example</td><td>76</td></tr><tr><td>3.2 Dynamic analysis</td><td>78</td></tr><tr><td>3.3 Symbolic Search</td><td>83</td></tr><tr><td>3.4 Related Work</td><td>90</td></tr><tr><td>3.5 Conclusion</td><td>92</td></tr></table>

This chapter is an update of these two papers:

Amira Radhouani, Akram Idani, Yves Ledru, and Narjes Ben Rajeb. Symbolic Search of Insider Attack Scenarios from a Formal Information System Modeling. LNCS Transactions on Petri Nets and Other Models of Concurrency, 10:131–152, 2015. URL https://doi.org/10.1007/978-3-662-48650-4_7.

Amira Radhouani, Akram Idani, Yves Ledru, and Narjes Ben Rajeb. Extraction of insider attack scenarios from a formal Information System Modeling. In 5th International Workshop on Formal Methods for Security (FMS), 2014.

The early detection of potential threats during the modelling and design phase of a Security Information System is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during system execution. This paper deals with internal attacks which can be made by people inside the organization.
Such attacks are difficult to detect because insiders have authorized system access and also may be familiar with system policies and procedures. We are interested in finding attacks which conform to the access control policy, but lead to unwanted states. These attacks are favoured by policies involving authorization constraints, which grant or deny access depending on the evolution of the functional Information System state. In this context, we propose to model functional requirements and their Role Based Access Control (RBAC) policies using B machines and then to formally reason on both models. In order to extract insider attack scenarios from these B specifications, our approach first investigates symbolic behaviours. Then, the use of a model-checking tool allows to exhibit, from a symbolic behaviour, an observable concrete sequence of operations that can be followed by an attacker. In this chapter, we show how this combination of symbolic analysis and model-checking allows one to find out such insider attack scenarios.

**3.1 Running Example**

In this section we use a running example issued from (Basin et al., 2009) and which deals with
a SecureUML model associated to a functional UML class diagram.

**3.1.1 Functional model**

The functional UML class diagram (presented in Figure 3.1) describes a meeting scheduler
dedicated to manage data about two entities: Persons and Meetings.

<figure><img src="image_42.png" /><figcaption>Figure 3.1: Functional model of meeting scheduler system</figcaption></figure>

A meeting has one and only one owner (association *MeetingOwner*), a list of participants (association *MeetingParticipants*), a duration, and a starting date. A person can be the owner of several meetings and may participate to several meetings. Operations *notify* and *cancel* are user-defined, and allow respectively to send messages to participants and to delete a meeting after notifying their participants by e-mail. Constructors, setters and getters are implicitly defined for both classes and both associations.

**3.1.2 Access control rules**

The access control model is given in Figure 3.2 using the secureUML syntax. It features three different roles:
* **SystemUser**: defines persons who are registered on the system and then have permission `UserMeetingPerm` which allows them to create and read meetings. Deletion and modification of meetings (including operation *cancel*) are granted to system users by means of permission `OwnerMeetingPerm`, featuring an authorization constraint checking that the user who tries to run these actions is the meeting owner.

* **Supervisor**: defines system users with more privileges because they can run actions notify and cancel on any meeting even if they are not owners.

* **SystemAdministrator**: having a full access on entity Person, an administrator manages system users. Full access grants him the right to create a new person, remove or modify an existing one. Furthermore, a system administrator has only a read access on meetings: he is not expected to create or modify meetings.

<figure><img src="image_43.png" /><figcaption>Figure 3.2: Security model of meeting scheduler system</figcaption></figure>

### 3.1.3 Validation

This example is intended to be validated in (Basin et al., 2009) based on a set of static queries that investigate a given system state in order to grasp some useful information like *"which user"*
can perform an action on a concrete resource in a given state”.

Authorization constraint associated to **OwnerMeetingPerm** requires information from the functional model because it deals with the *MeetingOwner* association. In the remainder, we consider three users John, Alice and Bob such that user assignments are as defined by Figure 3.3. We also consider a given initial state in which Alice is owner of meeting $m_1$, Bob is a participant of $m_1$. In such a state, the above static query establishes that only Alice is allowed to modify or delete $m_1$ because she is the owner of $m_1$.

<figure><img src="image_44.png" /><figcaption>Figure 3.3: Users assignment</figcaption></figure>

In (Ledru et al., 2014) a dynamic analysis approach based on animation of a formal specification showed that validation should not only be based on a given static state, but should search for sequences of actions modifying this state and breaking the authorization constraint. For example, starting from the above state, a static query would only report that John, and also Bob, can't modify $m_1$ because none of them satisfies the authorization constraint. A dynamic analysis would ask if there exists a sequence of operations enabled by John, or Bob, that allows them to modify $m_1$. This paper contributes towards automatically finding these malicious sequences. To perform these analysis, we applied the B4MSecure tool to the UML and SecureUML diagrams and generated a B specification counting 946 lines. This tool generates automatically a specification for all basic functional operations, which is enriched manually by some user-defined operations (i.e. cancel, notify).

## 3.2 Dynamic analysis

### 3.2.1 Trace Semantics for B Specifications

In order to find malicious behaviours of an operational secure IS model, we rely on the set of finite observable traces of our B specifications. Indeed, B specifications can be approached by means of a trace semantics composed of an initialization substitution *init*, a set of operations $\mathcal{O}$ and a set of state variables $\mathcal{V}$. We note *val* a possible state predicate allowed by the invariant and *op* an operation from $\mathcal{O}$. A functional behaviour is an observable sequence $Q$

$$Q \hat{=} init ; op_1 ; op_2 ; \dots ; op_m$$
such that $\forall i.(i \in 1..m \Rightarrow op_i \in \mathcal{O})$ and there exists a sequence $S$ of state predicates which does not violate invariant properties:

$$S \hat{=} val_0 ; val_1 ; \dots ; val_m$$

in which $val_0$ is an initial state, and $op_i$ is enabled from state $val_{i-1}$ and state $val_i$ is reached by $op_i$, starting from state $val_{i-1}$.

The security model filters functional behaviours by analysing access control premises which are triplets $(u, R, c)$ where $u$ is a user, $R$ is a set of possible roles assigned to $u$, and $c$ is an authorization constraint. An observable secure behaviour is a sequence $Q$, where for every step $i$, premise $(u_i, R_i, c_i)$ is valid (expressed as $(u_i, R_i, c_i) \models true)$. This means that roles $R_i$ activated by user $u_i$ grant him/her the right of running operation $op_i$ and if a constraint $c_i$ exists, then it must be satisfied. The following premises sequence $P$ must be valid for $Q$:

$$P \hat{=} (u_1, R_1, c_1) ; (u_2, R_2, c_2) ; \dots ; (u_m, R_m, c_m)$$

### 3.2.2 Tools to exhibit behaviours from B specifications

Model-checking and symbolic proof techniques are of interest in order to exhibit a relevant behaviour from an operational B specification. Proof techniques deal with infinite systems and can prove constraint satisfiability, or establish that some operation can be enabled from an abstract state predicate. Model-checking is based on model exploration of finite systems, and can be used to find a sequence of actions leading to a given state or property. In our approach, we combine both techniques in order to overcome their shortcomings: complexity of proofs for the first one, and state explosion for the second one. In this sub-section, we illustrate both tools.

**Model checking and animation (the ProB tool).** ProB (Leuschel and Butler, 2003) is an animation and a model-checker of B specifications that explores the concrete state space of the specification and generates accessibility graphs. Then, every predicate $val_i$ (where $i \in 0...m$) of sequence $S$ is a valuation of variables issued from $V$. For example, considering $V = \{person, meeting, meetingOwner, meetingParticipants\}$ and starting from an initial state $val_0$ such that:

$$\begin{align*}
val_0 &\hat{=} person = \emptyset \\
&\wedge meeting = \emptyset \\
&\wedge meetingOwner = \emptyset \\
&\wedge meetingParticipant = \emptyset
\end{align*}$$

and having $\mathcal{O} = \{personNew, meetingNew, meetingAddParticipants\}$, the scenario of table 3.1 is successfully animated using ProB. Column “reached states” gives only modified B variables from the previous step.

In step 1, the tool animates operation $personNew$ which modifies variable person (initially equal to $\emptyset$) and this action was performed by user John using role SystemAdministrator without
need of authorization constraint. In step 4, the tool adds participant Bob to the meeting $m_1$ by animating operation meetingAddParticipants, after verification that authorization constraint is True for Alice using role SystemUser. Indeed, Alice is the owner of $m_1$.

<table><caption>Table 3.1: animation of a normal scenario with ProB</caption><thead><tr><th>step</th><th>Sequence Q</th><th>Reached states S</th><th>RBAC premises P</th></tr></thead><tbody><tr><td>1</td><td>personNew</td><td>person={Alice}</td><td>John<br>SystemAdministrator<br>no constraint</td></tr><tr><td>2</td><td>personNew</td><td>person={Alice, Bob}</td><td>John<br>SystemAdministrator<br>no constraint</td></tr><tr><td>3</td><td>meetingNew</td><td>meeting={m<sub>1</sub>}</td><td>Alice<br>SystemUser<br>no constraint</td></tr><tr><td>4</td><td>meetingAddParticipants</td><td>meetingParticipants={(m<sub>1</sub>, Bob)}</td><td>Alice<br>SystemUser<br>Constraint: Alice is<br>the owner of m<sub>1</sub></td></tr></tbody></table>

**Symbolic proof (the GeneSyst tool).** ProB is useful to animate scenarios identified during requirements analysis, or to exhaustively explore a finite subset of state space. As we are interested in finding malicious scenarios that exhibit a potential internal attack, the ProB technique may be useful only if it explores the right state space subset in the right direction, which is not obvious for infinite systems. Symbolic proof techniques, such as that of GeneSyst by Bert et al. (2005), are more interesting because they allow one to produce symbolic transition systems that represent a potentially infinite set of values and a set of predicate states. Such tools reason on the enabledness properties of an operation *op* from a symbolic state *E* and the reachability properties of a symbolic state *F* by *op* from *E*. In (Bert et al., 2005), three enabledness properties and three reachability properties are defined in terms of the following proof obligations, where *E* and *F* are two disjoint state predicates and *x* is the set of variables of the system:

$$ (1) \text{ always enabled: } \forall x.E \Rightarrow \mathrm{Pre}(op) $$

$$ (2) \text{ never enabled: } \forall x.E \Rightarrow \neg \mathrm{Pre}(op) $$

$$ (3) \text{ possibly enabled } (\neg (1) \land \neg (2)): \exists x.E \land \mathrm{Pre}(op) $$

$$ (4) \text{ always reached: } \forall x.E \land \mathrm{Pre}(op) \Rightarrow [\mathrm{Action}(op)]F $$

$$ (5) \text{ never reachable: } \forall x.E \land \mathrm{Pre}(op) \Rightarrow [\mathrm{Action}(op)]\neg F $$

$$ (6) \text{ possibly reached } (\neg (4) \land \neg (5)): \exists x.E \land \mathrm{Pre}(op) \land \neg [\mathrm{Action}(op)]\neg F $$
Where $Pre(op)$ is a predicate representing the preconditions under which the operation $op$ becomes feasible (Abrial and Mussat, 1998), and $Action(op)$ is a generalized substitution (Abrial, 1996) representing its action.

The first three proof obligations deal with enabledness property. Proof obligation (1) means that whenever the state $E$ is satisfied, the precondition of the operation $op$ is true, then $op$ is always enabled from $E$. Whereas, according to the proof obligation (2), the $op$ precondition is false when $E$ is satisfied which means that $op$ can never be enabled from $E$. Proof obligation (3) means that there exists a subset in $E$ from which the precondition is satisfied, then $op$ is possibly enabled from $E$.

In the generalized substitution theory, formula $[S]R$ means that substitution $S$ always establishes predicate $R$, and $\neg[S]\neg R$ means that substitution $S$ may establish predicate $R$. Hence, proof (4) means that $F$ is always reached by the operation $op$ from $E$. Proof (5) means that $F$ is never reached by actions of $op$ from state $E$. Finally, proof (6) means that state $F$ may be reached by actions of $op$, when the operation precondition is true in state $E$. Note that reachability properties do not make sense if the enabledness property is not proved. Let us consider, for example, the functional operation *meetingNew*:

```
meetingNew(m, p) =
    PRE
        m \notin meeting \land p \in person
    THEN
        meeting := meeting \cup \{m\}
        || meetingOwner := meetingOwner \cup \{(m \mapsto p)\}
    END
```

This operation adds a new meeting $m$ and links it to an owner $p$. If we define states $E$ and $F$ such that:

$$E \hat{=} meetingOwner[\{m_1\}] = \emptyset$$

$$F \hat{=} meetingOwner[\{m_1\}] \neq \emptyset$$

Therefore, proof obligation produced by GeneSyst for property (6) is successfully proved via AtelierB showing that operation *meetingNew* when enabled from a state where $m_1$ does not exist and there exists at least one person in the system, may lead to a state where $m_1$ is created and has an owner.

As illustrated above, our work will focus on proof (6) which states the reachability of a target state from an initial one by some operations that are proved enabled from this one according to proof (3). We assume it is sufficient to decide whether an operation is potentially useful for a malicious behaviour. Proofs (4) and (5) can be used if one would like to assume that a state can never be reached, or it is always reached, by an operation.
### 3.2.3 Malicious Behaviour

Based on the security requirements, several operations can be identified as critical. For example, operations that perform (un)authorized modifications of meetings (e.g. MeetingSetStart) are critical because they may affect the integrity of meeting information. A malicious behaviour executed by a user u is an observable secure behaviour Q with m steps such that:

* $op_m$ is a critical operation to which an authorization constraint $c_m$ is associated.

* user u is malicious and would like to run $op_m$ by misusing his/her roles $R_u$.

* $val_0$: is an initial state where $(u, R_u, c_m) \models false$

* for every step $i$ ($i \in 1..m$) premise $(u, R_u, c_i) \models true$

In other words, malicious user u is not initially allowed to execute the critical operation, but he/she is able to run a sequence of operations leading to a state from which he/she can execute this operation. In our investigation we assume that user u executes this malicious sequence without collusion with another user. This problem is left to a future work.

Section 3.1.3 gave an example where neither Bob nor John are allowed to run a modification operation, such as meetingSetStart which modifies attributes of class Meeting, from the initial state due to the authorization constraint. This initial state is:

$$ 
\begin{aligned}
val_0 &\hat{=} \\
person &\equiv \{Alice, Bob\} \\
\wedge meeting &\equiv \{m_1\} \\
\wedge meetingOwner &\equiv \{(Alice \mapsto m_1)\} \\
\wedge meetingParticipant &\equiv \{(m_1 \mapsto Bob)\}
\end{aligned}
$$

In the following, we denote as $init_0$ the sequence of operations leading to $val_0$ as presented in table 3.1. We used the model-checking facility of ProB in order to explore exhaustively the state space and automatically find a path starting from $val_0$ and leading to a state where operation meetingSetStart becomes permitted to John. We asked ProB to find a sequence where John becomes the owner of $m_1$:

$$ meetingOwner(m_1) = John $$

After exploring more than 1000 states, ProB found a scenario in which John executes sequentially operations personNew, personAddMeetingOwner and meetingSetStart. Indeed, John, as a system administrator, has a full access to entity Person. This permission allows him to create, modify, read and delete any instance of class Person. First, using his system administration role, he creates an instance John of class Person that corresponds to him by running operation personNew(John). Then he adds meeting $m_1$ to the set of meetings owned by John, by running operation personAddMeetingOwner(John, $m_1$) which is a basic modification operation of class Person. These two actions allowed him to become the owner of $m_1$ and then he was able to modify the meeting of Alice using his system user role.
Like all model-checking techniques, when ProB explores exhaustively the state space, it faces the combinatorial explosion problem which depends on the number of operations provided to the tool and the state space size. In order to address this problem, our approach proposes a symbolic search which finds a sequence of potentially useful operations on which the model-checker should be focused.

## 3.3 Symbolic Search

The proposed symbolic search is performed by an algorithm (Figure 3.4) that looks for an observable symbolic sequence $Q \hat{=} init_0 ; op_1 ; \dots ; op_m$ such that operations are not instantiated. The searched sequence is executed by a user $u$, where $(u, R_u, c_m)$ is not valid for a critical operation $op_m$ in the initial state $val_0$ but becomes valid for state $val_{m-1}$ where $op_m$ can be enabled. It is a backward search algorithm, starting from the goal state $val_{m-1}$ from which the critical operation $op_m$ can be enabled: $val_{m-1} \hat{=} c_m \wedge Pre(op_m)$; and working backwards until the initial state $val_0$ is encountered. The algorithm ends when sequence $Q$ is found or when all operations are verified without encountering the initial state. We consider that $val_0$ is a completely valuated state such as the one where Alice is the owner of $m_1$, and Bob is a participant to $m_1$. This prevents the initial state from being included in both states $val_{m-1}$ and $val_{m-2}$, which would never verify the condition of the while loop.

### 3.3.1 Termination

Termination of our algorithm is ensured by the termination of the while loop conditions:

$$ val_0 \neq val_{m-1} \text{ and } val_{m-1} \neq \text{false} \text{ and } Opset \neq \emptyset $$

* $val_0 \neq val_{m-1}$: means that the initial state is not yet encountered. If the initial state is included in $val_{m-1}$ ($val_0 \Rightarrow val_{m-1}$), then our algorithm concludes that a sequence is found.

* $val_{m-1} \neq \text{false}$: means that precondition of the last computed operation is not reduced to false. If this condition becomes false, then the algorithm concludes that there is no further state enabling the last computed operation, and then it raises exception "no sequence found".

* $Opset \neq \emptyset$: means that there still exist operations that are not exploited. Every operation is called at the most once in a symbolic sequence because the algorithm iteratively removes operations from set $Opset$ ($Opset = Opset \setminus \{o_i\}$). Hence, when a sequence is found, the maximum size of a computed scenario is $n$ such that $n$ is the system operations number. This last condition guarantees termination when none of the previous conditions becomes false after exploiting all operations.
1. $Q \hat{=} op_m$;

2. $val_{m-1} \hat{=} c_m \wedge Pre(op_m)$;

3. $val_{m-2} \hat{=} \neg val_{m-1}$;

4. $Opset \hat{=} O$;

5. **while** ($val_0 \not\Rightarrow val_{m-1}$ **and** $val_{m-1} \not\models false$ **and** $Opset \not\models \emptyset$) **do**

6. **choose any** $o_i \in Opset$ **where**

7. $(u, R_u, c_i) \models true \wedge$

8. $\exists x. val_{m-2} \wedge Pre(o_i) \wedge //PO3$

9. $\exists x. val_{m-2} \wedge Pre(o_i) \wedge \neg [Action(o_i)] \neg val_{m-1} //PO6$

10. **do**

11. $Q \hat{=} o_i ; Q ;$

12. $val_{m-1} \hat{=} val_{m-2} \wedge Pre(o_i)$;

13. $val_{m-2} \hat{=} val_{m-2} \wedge \neg Pre(o_i)$;

14. $Opset \hat{=} Opset \setminus \{o_i\}$;

15. **else**

16. **raise exception:** No sequence found;

17. **enddo**

18. **endwhile**

19. **if** $val_0 \Rightarrow val_{m-1}$ **then**

20. $Q \hat{=} init ; Q ;$

21. **else**

22. **raise exception:** No sequence found;

23. **endif**

<caption>Figure 3.4: A symbolic search proof based algorithm</caption>

### 3.3.2 Completeness

Although our algorithm succeeds in finding attacks (see Section 3.3.4), it lacks completeness in two cases. First, since operations are deleted from set *Opset* as soon as they are used, it is not able to extract attack scenarios in which an operation occurs more than once. Second, the algorithm expects operations to have non trivial preconditions, and may stop too early if the sequence includes operations with *true* as a precondition. In fact, the algorithm builds symbolic states step by step. Based on the precondition of the extracted operation on a given step it infers the previous states as follows:

$$val_{m-1} \hat{=} val_{m-2} \wedge Pre(o_i);$$

$$val_{m-2} \hat{=} val_{m-2} \wedge \neg Pre(o_i);$$

Due to the precondition negation, the algorithm stops when it extracts an operation without precondition (i.e. $Pre(o_i) \hat{=} true$). Consequently, the algorithm may extracts just a part of an existing sequence.
However, experiments shows that it does well for many case studies and it is able to extract symbolic sequences that don't include repetition of operations or operations without precondition or operations with the same preconditions. Because of these restrictions, we propose to combine the symbolic search with model checking. Thus, the symbolic sequence found by our algorithm is then used to guide a model-checker which will instantiate the parameters of operations, and may identify sequences with operation repetition.

### 3.3.3 Step by Step Illustration

We take advantage of abstraction and step by step we refine the $val_{m-2}$ symbolic state:

1. At the first step of the algorithm, the state space is represented by two symbolic states: the first one $val_{m-1}$ includes all states where the authorization constraint $c_m$ is true and which are enabling $op_m$, and the second one $val_{m-2}$ is the negation of $val_{m-1}$ which is then $\neg c_m \lor \neg Pre(op_m)$. As they are two disjoint state predicates, we conduct proofs (3) and (6) in order to find an operation $o_i$ that belongs to $O$ and which is possibly enabled from $val_{m-2}$ and reaches the first state $val_{m-1}$ and such that premise $(u, R_u, c_i)$ is valid. If $o_i$ does not exist, then no sequence could be found for the expected attack and we can try proof (5) for each operation attesting that all operations never reach $val_{m-1}$ from $val_{m-2}$. Figure 3.5 provides a state machine diagram that illustrates this first iteration. In this representation, states are predicates and transitions are symbolic operations.

<figure><img src="image_45.png" /><figcaption>Figure 3.5: First iteration algorithm illustration</figcaption></figure>

2. At the second step of the algorithm, if proofs (3) and (6) succeed for some operation $op_{m-1}$, then an observable sequence may exist, leading to the critical operation where access control premise $(u, R_u, c_m)$ is valid.

3. If $val_0$ is inside $Pre(o_i)$ then the algorithm stops. Otherwise, as showed in Figure 3.6, the algorithm looks inside state $val_{m-2}$ in order to find out the previous operations that can be invoked in the attack scenario. State $val_{m-2}$ is partitioned into two sub-states which are:
$$val_{m-2} \wedge Pre(op_{m-1}) \equiv \neg(c_m \wedge Pre(op_m)) \wedge Pre(op_{m-1})$$

$$val_{m-2} \wedge \neg Pre(op_{m-1}) \equiv \neg(c_m \wedge Pre(op_m)) \wedge \neg Pre(op_{m-1})$$

4. Then, we look for operations that reach the first sub-state from the second one.

<figure><img src="image_46.png" /><figcaption>Figure 3.6: Second iteration algorithm illustration</figcaption></figure>

5. The algorithm proceeds iteratively (Figure 3.7) by partitioning the second state into two sub-states until either it finds a state that includes the initial state, which corresponds to a successful search, or fails the search because $val_{m-1}$ is empty or all operations have been invoked once. In the best case, our algorithm gives some symbolic attack scenario, which consists of sequence $(init_0; op_n; op_{n+1}; \dots; op_m)$ invoked by the same user $u$ and where:

$$val_{n-1} \hat{=} \neg(c_m \wedge Pre(op_m)) \wedge \neg Pre(op_{m-1}) \wedge \neg Pre(op_{m-2}) \wedge \dots \wedge Pre(op_n)$$

and such that $val_0 \Rightarrow val_{n-1} \wedge \forall i.(i \in (n..m) \Rightarrow (u, R_u, c_i) \models true)$

### 3.3.4 Application

We apply our algorithm to the meeting scheduler example starting from the following initial state $val_0$:

$$val_0 \hat{=} person = \{Alice, Bob\}$$

$$\wedge meeting = \{m_1\}$$

$$\wedge meetingOwner = \{(Alice \mapsto m_1)\}$$

$$\wedge meetingParticipant = \{(m_1 \mapsto Bob)\}$$

In this state user John is not allowed to modify meeting $m_1$ because the authorization constraint allows modification only by the owner of $m_1$. A malicious scenario would lead
<figure><img src="image_47.png" /><figcaption>Figure 3.7: Last iteration algorithm illustration</figcaption></figure>

to a state where John becomes able to execute a modification operation such as operation `meetingSetStart` on meeting $m_1$. In this state we have to verify:

$$ \begin{gathered} \text{Pre}(\text{meetingSetStart}(m_1, \text{start})) \hat{=} m_1 \in \text{meeting} \\ \text{and } (\text{John}, \text{SystemUser}, \text{MeetingOwner}(m_1) = \text{John}) \models \text{true} \end{gathered} $$

1. First iteration: considering the following symbolic states

$$ val_{m-1} \hat{=} (\text{MeetingOwner}(m_1) = \text{John}) \wedge m_1 \in \text{Meeting} $$

$$ val_{m-2} \hat{=} \neg val_{m-1} $$

we have:

$$ val_0 \not\Leftrightarrow val_{m-1} \text{ because, in state } val_0, \text{MeetingOwner}(m_1) = \text{Alice}, $$

and

PO (6) is discharged automatically by AtelierB prover for operation `meetingNew` which may be executed by `John` as system user, and also for `personAddMeetingOwner` when `John` is system administrator. In addition, manual proofs has been done to demonstrate that `meetingNew` satisfies the PO for instantiation `meetingNew(m_1, John)` and that `personAddMeetingOwner` leads to $val_{m-1}$ if and only if it is executed with parameters $(John, m_1)$. We have also checked PO (5) to verify that all other operations never reach $val_{m-1}$ from $val_{m-2}$. Then, we may go on with the second iteration of the algorithm for each of these two operations.