Search

International audience; This paper presents a formal model of the case study proposed for the ABZ2018 conference, which concerns the Hybrid ERTMS/ETCS Level 3 Standard. This standard allows trains to communicate with a train supervisor to report their integrity and positions, thanks to an onboard train integrity monitoring system. The supervisor assigns trains a movement authority to control traffic and to avoid collisions. The standard also provides for trains that cannot communicate with the supervisor; these trains are detected by sensors on tracks and obey traffic signals set by the supervisor along the trackside. Using communication allows for a finer grain control of the tracks. Our model is derived using stepwise refinement with the Event-B method. We take into account the main features of the case study (VSS management, timers, ERTMS and non-ERTMS trains). Our model is decomposed into four refinements. All proof obligations have been discharged using the Rodin provers, except those related to the computation of the VSS state machine, which was found to be ambiguous (nondeterministic). Our model has been validated using ProB. The main safety property, which is that ERTMS trains do not collide, is proved. Our model focuses on the discrete control logic aspects of the case study.

International audience; This paper introduces an Event-B formal model of the adaptive exterior light system for cars, a case study proposed in the context of the ABZ2020 conference. The system describes the different provided lights and the conditions under which they are switched on/off in order to improve the visibility of the driver without dazzling the oncoming ones. The system can be viewed as a lights controller that reads different information form the available sensors (key state, exterior luminosity, etc.) and takes the adequate actions by acting on the actuators of the lights in order to ensure a good visibility for the driver according to the information read. Our model is built using stepwise refinement with the Event-B method. We consider all the features of the case study, all proof obligations have been discharged using the Rodin provers. Our model has been validated using ProB by applying the different provided scenarios. This validation has permitted us to point out and correct some mistakes, ambiguities and oversights in the first versions of the case study.

Hybrid systems are one of the most common mathematical models for Cyber-Physical Systems (CPSs). They combine discrete dynamics represented by state machines or finite automata with continuous behaviors represented by differential equations. The measurement of continuous behaviors is performed by sensors. When these sensors have a continuous access to these measurements, we call such model an Event-Triggered model. The properties of this model are easier to prove, while its implementation is difficult in practice. Therefore, it is preferable to introduce a more realistic model, called Time-Triggered model, where the sensors take periodic measurements. Contrary to Event-Triggered models, Time-Triggered models are much easier to implement, but much more difficult to verify. Based on the differential refinement logic (dR\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {L}$$\end{document}), a dynamic logic for refinement relations on hybrid systems, it is possible to prove that a Time-Triggered model refines an Event-Triggered model. The major limitation of such logic is that it is not supported by any prover. In this paper, we propose a correct-by-construction approach that implements the reasoning on hybrid programs particularly the reasoning of dR\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {L}$$\end{document} in Event-B to take advantage of its associated tools.

This paper presents SGAC (Solution de Gestion Automatisée du Consentement / automated consent management solution), a new healthcare access control model and its support tool, which manages patient wishes regarding access to their electronic health records (EHR). This paper also presents the verification of access control policies for SGAC using two first-order-logic model checkers based on distinct technologies, Alloy and ProB. The development of SGAC has been achieved within the scope of a project with the University of Sherbrooke Hospital (CHUS), and thus has been adapted to take into account regional laws and regulations applicable in Québec and Canada, as they set bounds to patient wishes: for safety reasons, under strictly defined contexts, patient consent can be overriden to protect his/her life (break-the-glass rules). Since patient wishes and those regulations can be in conflict, SGAC provides a mechanism to address this problem based on priority, specificity and modality. In order to protect patient privacy while ensuring effective caregiving in safety-critical situations, we check four types of properties: accessibility, availability, contextuality and rule effectivity. We conducted performance tests comparison: implementation of SGAC versus an implementation of another access control model, XACML, and property verification with Alloy versus ProB. The performance results show that SGAC performs better than XACML and that ProB outperforms Alloy by two order of magnitude thanks to its programmable approach to constraint solving.

International audience; We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hocmathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards

HighlightsWe propose to merge a set of business process fragments to construct new processes.We extend path matrices to systematically compile fragments' components.We ensure that the behavior of initial fragments is preserved.We ensure that the designer is alerted of undesirable behaviors.We prove the effectiveness of our approach through experimentations. In the field of business process management, adopting efficient building strategies can improve the quality of companies' business processes. The reuse of existing business processes or even fragments of them is a practical approach to build complete business processes or coarser-grained process fragments. In the present paper, we deal with the merge of a set of business process fragments for the construction of new complete processes. Our merge mechanism relies on a particular path matrix, that we call gateway path matrix. We use gateway path matrices to represent business process fragments to systematically compose shared components with individual ones. Moreover, our approach ensures that the resulting business process fragments subsume the behavior of initial ones and allows for adding new execution scenarios while controlling undesirable ones. In fact, we detect newly generated behaviors, and alert process designers of undesirable ones through behavioral constraints. We provide extensive experimental results derived from an implementation of our approach applied on a well-known industrial library of business process fragments.

International audience; Cloud computing is a new computing paradigm used for building on demand free and open source software (FOSS) applications. However, due to the lack of an explicit and formal description of the resource perspective in the existing FOSS applications, the correctness of Cloud resources management cannot be verified. The main objective of this paper is to propose a formal definition of the resource perspective in FOSS applications as a step towards ensuring a correct and consistent Cloud resource allocation in FOSS application modeling. Hence, we developed a Cloud Resources Allocation Model (CRAM4FOSS) for FOSS applications using the Event-B method. This model is used to formally validate the consistency of Cloud resource allocation for FOSS applications at design time, and to analyze and check its correctness according to the user’s requirements and the resource’s capabilities. The correctness and the consistency of our CRAM4FOSS model have been established into two phases : first, the ProB model-checker is used to detect the most obvious errors and validate the Event-B model by playing some scenarios, then a proof activity is performed to discharge the generated proof obligations that ensure the correctness of the model.

In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.

International audience; This paper presents a specification of the hybrid ERTMS/ ETCS level 3 standard in the framework of the case study proposed for the 6th edition of the ABZ conference. The specification is based on the method and tools, developed in the ANR FORMOSE project, for the modeling and formal verification of critical and complex system requirements. The requirements are specified with SysML/KAOS goal diagrams and are automatically translated into B System specifications, in order to obtain the architecture of the formal specification. Domain properties are specified by ontologies with the SysML/KAOS domain modeling language, based on OWL and PLIB. Their automatic translation completes the structural part of the formal specification. The only part of the specification, which must be manually completed, is the body of events. The construction is incremental, based on the refinement mechanisms existing within the involved methods. The formal specification of the case study is composed of seven refinement levels and all the proofs have been discharged with the Rodin prover

Context: Nowadays, Information Systems (IS) are at the heart of most companies and constitute then a critical element that needs an adequate attention regarding security issues of sensitive data it manages. Objective: This paper presents a formal approach for the development of a filter to secure access to sensitive resources of information systems. Method: The proposed approach consists of three complementary steps. Designers start by modeling the functionalities of the system and its security requirements using dedicated UML diagrams. These diagrams are then automatically translated into a formal B specification suitable not only for reasoning about data integrity checking but also for the derivation of a trustworthy implementation. Indeed, a formal refinement process is applied on the generated B specification to obtain a relational-like B implementation which is then translated into an AspectJ implementation, connected to a SQL Server (release 2014) relational database system. Such a generation is performed following the aspect oriented programming paradigm which permits a separation of concerns by making a clear distinction between functional and security aspects. Results: A systematic formal approach to derive a secure filter that regulates access to the sensitive data of an information system. The filter considers both static and dynamic access rules. A tool that supports the proposed approach is also provided. Conclusion: The approach has been applied on several case studies that demonstrate that the development of a tool permits to free the developers from tedious and error-prone tasks since they have just to push a button to generate the AspectJ code of an application.

This article describes the Event-B modeling of a landing gear system of an aircraft whose complete description can be found in Boniol and Wiels (The Landing Gear System Case Study, ABZ Case Study, Communications in Computer Information Science, vol 433, Springer, Berlin, 2014). This real-life case study has been proposed by the ABZ'2014 track that took place in Toulouse, the European capital of the aeronautic industry. Our modeling is based on the Parnas and Madey's 4-Variable Model that permits to consider the different parts of a system. These parts are incrementally introduced using the Event-B refinement technique. The entire development has been carried out with the Rodin toolset. To ensure the correctness of the different components, we use several verification techniques (animation, model checking and proof) depending on the complexity and the kind of the properties to verify. Basically, prior to the proof phase that can be tedious and complex, we use the animator AnimB and the model checker ProB that permit to discover some trivial inconsistencies. Once no error is reported, we start the proof phase by using the Atelier B and SMT provers which we installed on Rodin. We conclude the article by drawing up some key findings of and lessons learned from this experience.

Dynamic properties are very useful in the specification of Information Systems (IS) and security policies. They allow the user to express properties that involve several states of a system. Indeed, invariance properties do not permit to cover such kind of properties. In this paper, we suggest a formal approach, based on the use of the B method, to verifying absence properties of the form $\mathsf{Abs}(P_2, \ \mathsf{From}\ P_1\ \mathsf{Until}\ P_3)$ that express that some states, represented by predicate $P_2$, should not be reached starting from a state that satisfies $P_1$ until a state satisfies $P_3$ is reached. Our proposal consists in defining two proof obligations based on weakest preconditions that are sufficient and necessary to prove that a system verifies such a property.

International audience; Context: Formal methods are very useful in the software industry and are becoming of paramount importance in practical engineering techniques. They involve the design and modeling of various system aspects expressed usually through different paradigms. These different formalisms make the verification of global developed systems more difficult. Objective: In this paper, we propose to combine two modeling formalisms, in order to express both functional and security timed requirements of a system to obtain all the requirements expressed in a unique formalism. Method: First, the system behavior is specified according to its functional requirements using Timed Extended Finite State Machine (TEFSM) formalism. Second, this model is augmented by applying a set of dedicated algorithms to integrate timed security requirements specified in Nomad language. This language is adapted to express security properties such as permissions, prohibitions and obligations with time considerations. Results: The proposed algorithms produce a global TEFSM specification of the system that includes both its functional and security timed requirements. Conclusion: It is concluded that it is possible to merge several requirement aspects described with different formalisms into a global specification that can be used for several purposes such as code generation, specification correctness proof, model checking or automatic test generation. In this paper, we applied our approach to a France Telecom Travel service to demonstrate its scalability and feasibility.

International audience; This paper presents a technique for vulnerability detection in C programs. It is based on a vulnerability formal model called "Vulnerability Detection Conditions" (VDCs). This model is used together with passive testing techniques for the automatic detection of vulnerabilities. The proposed technique has been implemented in a dynamic code analysis tool, TestInv-Code, which detects the presence of vulnerabilities on a given code, by checking dynamically the VDCs on the execution traces of the given program. The tool has been applied to several C applications containing some well known vulnerabilities to illustrate its effectiveness. It has also been compared with existing tools in the market, showing promising performances

International audience; This paper proposes an approach to prove reachability properties of the form AG psi => EF phi using substitution refinement in classical B. Such properties denote that there exists an execution path for each state satisfying psi to a state satisfying phi. These properties frequently occur in security policies and information systems. We show how to use Morgan's specification statement to represent a property and refinement laws to prove it. The idea is to construct by stepwise refinement a program whose elementary statements are operation calls. Thus, the execution of such a program provides an execution satisfying AG psi => EF phi. Proof obligations are represented using assertions (ASSERT clause of B) and can be discharged using Atelier B

International audience; Formal methods are very useful in software industry and are becoming of paramount importance in practical engineering techniques. They involve the design and the modeling of various system aspects expressed usually through different paradigms. In this paper, we propose to combine two modeling formalisms in order to express both functional and security timed requirements of a system. First, the system behavior is specified based on its functional requirements using TEFSM (Timed Extended Finite State Machine) formalism. Second, this model is augmented by applying a set of dedicated algorithms to integrate timed security requirements specified in Nomad language. This language is well adapted to express security properties such as permissions, prohibitions and obligations with time considerations. The resulting secure model can be used for several purposes such as code generation, specification correctness proof, model checking or automatic test generation. In this paper, we applied our approach to a France Telecom(France Telecom is the main telecommunication company in France) Travel service in order to demonstrate its feasibility

International audience; This paper describes the formal verification of an interlocking system. We have formally proved the non-derailing and non-collision safety properties for an existing interlocking system operating on Paris Metro's line 3Bis. These high-level properties have first been refined to an intermediate level permitting their expression in terms of the control system's inputs and outputs. The resulting properties have then been formalised in the Prover iLock Verifier engine's internal language. The Prover iLock Verifier engine is a COTS commercialised by Prover Technology. For this project some specific features have been added to the engine to provide certified proofs that can be used, instead of testing, in the SIL-4 qualification process of interlocking systems.

This paper presents a formal approach for the development of trustworthy database applications. This approach consists of three complementary steps. Designers start by modeling applications using UML diagrams dedicated to database applications domain. These diagrams are then automatically translated into B specifications suitable not only for reasoning about data integrity checking but also for the derivation of trustworthy implementations. In this paper, we present a process based on the B refinement technique for the derivation of a SQL relational implementation, embedded in the JAVA language (JAVA/SQL), from a B specification obtained by the first translation phase.

International audience; UB2SQL is a tool for designing and developing database applications using UML and B formal method. The approach supported by UB2SQL consists of two successive phases. In the first phase, with the design of applications using class, state and collaboration diagrams, B specifications are automatically generated from UML diagrams; the diagrams are then augmented with these B specifications in place. The second phase deals with the refinement of these B specifications into a relational database implementation, for which UML representation is constructed. In both phases, proofs are achieved to ensure correctness of the obtained B specification and correctness of the refinement process. To overcome the lack of rules and tactics in the B prover, UB2SQL defines specific rules and tactics making the proof task seem like a push-button activity. To increase the usability of UB2SQL in both academic and industrial contexts, the tool has been integrated as a plug-in to the Rational Rose CASE tool. Such integration allows users to develop and be able to visualize graphical UML diagrams and formal B notation in a single environment

International audience; This article describes a formal approach to specify and develop database applications. This approach consists of two complementary phases. In the first phase, B specifications are automatically generated from UML class, state and collaboration diagrams describing the data and the transactions of the system we are developing. In the second phase, these specifications are successively refined until they become close enough to a relational implementation. The tool supporting this approach is implemented as an extension of the Rational Rose tool to develop and visualize graphical (UML) and formal (B) notations in a single environment.

The paper introduces an approach to the specification, the verification and the validation of B2B transactions. Based on the usage of a subset of formally defined UML diagrams complemented with business rules, we introduce two facilities offered by the supporting Efficient toolset, namely the checking of formal properties expected from the produced models as well as the animation tool allowing business experts to understand and ‘play' with business transactions models before they are implemented. The overall approach is illustrated through the experiences gained in the performance of a real transactional Import/Export business case.

This paper presents, through an example, an overview of our method which generates B specifications from an application described using UML notations. We are interested in data intensive applications. This allows us to automatically generate basic update operations from class diagrams. Then these operations are combined to elaborate more complex transactions described in UML by state and collaboration diagrams. The obtained B machines are directly usable in AtelierB and proofs can be performed allowing the consistency of the application to be checked. Finally the outlines of the prototype support tool are described.

The cybersecurity ecosystem continuously evolves with the number, the diversity, and the complexity of cyber attacks. Generally, we have three IDS types: anomaly-based detection, signature-based detection, and hybrid detection. Anomaly detection is based on the usual behavior description of the system, typically in a static manner. It enables detecting known or unknown attacks, but generating also a large number of false positives. Signature based detection enables detecting known attacks by defining rules that describe known attacker's behavior. It needs a good knowledge of attacker behavior. Hybrid detection relies on several detection methods including the previous ones. It has the advantage of being more precise during detection. Tools like Snort and Zeek offer low level languages to represent rules for detecting attacks. The number of potential attacks being large, these rule bases become quickly hard to manage and maintain. Moreover, the representation of stateful rules to recognize a sequence of events is particularly arduous. In this thesis, we propose a stateful approach to identify complex attacks. We consider the hierarchical state-transition diagram approach, using the ASTDs. ASTDs allow a graphical and modular representation of a specification that facilitates maintenance and understanding of rules. We extend the ASTD notation with new features to represent complex attacks. Next, we specify several attacks with the extended notation and run the resulting specifications on event streams using an interpreter to identify attacks. We also evaluate the performance of the interpreter with industrial tools such as Snort and Zeek. Then, we build a compiler in order to generate executable code from an ASTD specification, able to efficiently identify sequences of events., L'écosystème de la cybersécurité évolue en permanence en termes du nombre, de la diversité, et de la complexité des attaques. De ce fait, les outils de détection deviennent inefficaces face à certaines attaques. On distingue généralement trois types de système de détection d'intrusions: détection par anomalies, détection par signatures et détection hybride. La détection par anomalies est fondée sur la caractérisation du comportement habituel du système, typiquement de manière statistique. Elle permet de détecter des attaques connues ou inconnues, mais génère aussi un très grand nombre de faux positifs. La détection par signatures permet de détecter des attaques connues en définissant des règles qui décrivent le comportement connu d'un attaquant. Cela demande une bonne connaissance du comportement de l'attaquant. La détection hybride repose sur plusieurs méthodes de détection incluant celles sus-citées. Elle présente l'avantage d'être plus précise pendant la détection. Des outils tels que Snort et Zeek offrent des langages de bas niveau pour l'expression de règles de reconnaissance d'attaques. Le nombre d'attaques potentielles étant très grand, ces bases de règles deviennent rapidement difficiles à gérer et à maintenir. De plus, l'expression de règles avec état dit stateful est particulièrement ardue pour reconnaître une séquence d'événements. Dans cette thèse, nous proposons une approche stateful afin d'identifier des attaques complexes. Nous considérons l'approche diagramme état-transition hiérarchique, en utilisant les ASTDs. Les ASTDs permettent de représenter de façon graphique et modulaire une spécification, ce qui facilite la maintenance et la compréhension des règles. Nous étendons la notation ASTD avec de nouvelles fonctionnalités pour représenter des attaques complexes. Ensuite, nous spécifions plusieurs attaques avec la notation étendue et exécutons les spécifications obtenues sur des flots d'événements à l'aide d'un interpréteur pour identifier des attaques. Nous évaluons aussi les performances de l'interpréteur avec des outils industriels tels que Snort et Zeek. Puis, nous réalisons un compilateur afin de générer du code exécutable à partir d'une spécification ASTD, capable d'identifier efficacement les séquences d'événements.

The SysML/KAOS method allows to model system requirements through goal hierarchies. B System is a formal method used to construct, verify and validate system specifications. A B System model consists of a structural part (abstract and enumerated sets, constants with their associated properties, and variables with their associated invariant) and a behavioral part (events). Correspondence links are established in previous work between SysML/KAOS and B System to produce a formal specification from requirements models. This specification serves as a basis for formal verification and validation tasks to detect and correct inconsistencies. However, it is required to manually provide the structural part of the B System specification.This thesis aims at enriching SysML/KAOS with a language that allows tomodel the application domain of the system and which would be compatible withthe requirements modeling language. This includes the definition of the domainmodeling language and of mechanisms for leveraging domain modeling to providethe structural part of the B System specification obtained from requirements models.The defined language uses ontologies to allow the formal representation of systemdomain. Moreover, the established correspondence links and rules, formally verified,allow both propagation and backpropagation of additions and deletions, betweendomain models and B System specifications. An important part of the thesis is alsodevoted to assessment of the SysML/KAOS method on case studies. Furthermore,since the systems naturally break down into subsystems (enabling the distribution ofwork between several agents: hardware, software and human), SysML/KAOS goalmodels allow the capture of assignments of requirements to subsystems responsibleof their achievement. This thesis therefore describes the mechanisms required toformally guarantee that each requirement assigned to a subsystem will be wellachieved by the subsystem, within the constraints defined by the high-level systemand subsystem specifications.The SysML/KAOS method, thus enriched, has been implemented within an opensource tool using the model federation platform Openflexo, and has been evaluated on various industrial scale case studies. It enables the formal verification of requirements and facilitates their validation by the various stakeholders, including those with less or no expertise in formal methods. However, both the specification of the body of B System events and domain model logical formulas (that give B System properties and invariants) and the formal assessment (verification and validation) of the specification can only be manual. They are time consuming and require experts in formal methods. But this is the price to pay to achieve a formal verification and validation of requirements., La méthode SysML/KAOS permet de modéliser les exigences d’un système sous forme d’hiérarchies de buts. B System est une méthode formelle qui permet de construire, vérifier et valider la spécification d’un système. Un modèle B System est constitué d’une partie structurelle (ensembles abstraits et énumérés, constantes et leurs propriétés, et variables et leur invariant) et d’une partie comportementale (évènements). Lors de travaux antérieurs, des liens de correspondance ont été établis entre SysML/KAOS et B System afin de produire une spécification formelle à partir de la modélisation des exigences. Cette spécification sert de base pour les tâches de vérification et de validation formelle afin de détecter et corriger les potentielles erreurs de spécification. Toutefois, il est nécessaire de fournir manuellement la partie structurelle du modèle B System.L’objectif de cette thèse est d’enrichir SysML/KAOS avec un langage permettant de modéliser le domaine du système et qui serait compatible avec le langage de modélisation des exigences. Ceci inclut non seulement la définition du langage, mais aussi des mécanismes permettant d’exploiter la modélisation du domaine pour fournir la partie structurelle de la spécification B System issue de la formalisation des exigences. Le langage défini exploite la notion d’ontologie pour permettre la représentation formelle du domaine. Bien plus, les liens et règles de correspondance établis et formellement vérifiés permettent tant la propagation que la rétropropagation des ajouts et suppressions, entre modèles de domaine et spécifications B System. Un autre aspect essentiel de la thèse réside dans l’évaluation de la méthode SysML/KAOS sur des études de cas. Par ailleurs, les systèmes, au vu de leur complexité, se doivent d’être décomposés en sous-systèmes. La thèse décrit en conséquence des mécanismes permettant de garantir formellement que chaque exigence affectée à un sous-système sera bien satisfaite par ce dernier, dans la limite définie par la spécification du système et des sous-systèmes.La méthode SysML/KAOS, ainsi enrichie, a été implémentée au sein d’un outil libre en utilisant la plateforme de fédération de modèles Openflexo, et a été évaluée sur différentes études de cas d’envergure industrielle. Elle permet la vérification formelle des exigences et facilite leur validation par des parties prenantes non spécialistes de méthodes formelles. Toutefois, les tâches de spécification des formules logiquesdu modèle de domaine, qui donnent lieu aux propriétés et invariants du modèle BSystem, et du corps des évènements B System, ainsi que les tâches de vérification etvalidation formelles sont coûteuses en temps et nécessitent l’implication d’expertsen méthodes formelles. Il s’agit là du prix à payer pour des exigences formellementcorrectes.

Nowadays, organizations rely more and more on information systems to collect, manipulate, and exchange their relevant and sensitive data. In these systems, security plays a vital role. Indeed, any security breach may cause serious consequences, even destroy an organization's reputation. Hence, sufficient precautions should be taken into account. Moreover, it is well recognized that the earlier an error is discovered, the easier and cheaper it is debugged. The objective of this thesis is to define adequate security policies since the early development phases and ensure their correct deployment on a given technological infrastructure. Our approach starts by specifying a set of security requirements, i.e. static and dynamic rules, along with the functional aspect of a system based on the Unified Modeling Language (UML). Fundamentally, the functional aspect is expressed using a UML class diagram, the static security requirements are modeled using SecureUML diagrams, and the dynamic rules are represented using secure activity diagrams. We then define translation rules to obtain B specifications from these graphical models. The translation aims at giving a precise semantics to these diagrams, thus proving the correctness of these models and verifying security policies with respect to the related functional model using the AtelierB prover and the ProB animator. The obtained B specification is successively refined to a database-like implementation based on the AOP paradigm. The B refinements are also proved to make sure that the implementation is correct with respect to the initial abstract specification. Our translated AspectJ-based program allows separating the security enforcement code from the rest of the application. This approach avoids scattering and tangling the application's code, thus it is easier to track and maintain. Finally, we develop a tool that automates the generation of the B specification from UML-based models and of the AspectJ program connected to a relational database management system from the B implementation. The tool helps disburden developers of the difficult and error-prone task and improve the productivity of the development process, Aujourd’hui, les organisations s'appuient de plus en plus sur les systèmes d'information pour collecter, manipuler et échanger leurs données. Dans ces systèmes, la sécurité joue un rôle essentiel. En effet, toute atteinte à la sécurité peut entraîner de graves conséquences, voire détruire la réputation d'une organisation. Par conséquent, des précautions suffisantes doivent être prises en compte. De plus, il est bien connu que plus tôt un problème est détecté, moins cher et plus facile il sera à corriger. L'objectif de cette thèse est de définir les politiques de sécurité depuis les premières phases de développement et d’assurer leur déploiement correct sur une infrastructure technologique donnée.Notre approche commence par spécifier un ensemble d'exigences de sécurité, i.e. des règles statiques et dynamiques, accompagnées de l'aspect fonctionnel d'un système basé sur UML (Unified Modeling Language). L'aspect fonctionnel est exprimé par un diagramme de classes UML, les exigences de sécurité statiques sont modélisées à l'aide de diagrammes de SecureUML, et les règles dynamiques sont représentées en utilisant des diagrammes d'activités sécurisées.Ensuite, nous définissons des règles de traduction pour obtenir des spécifications B à partir de ces modèles graphiques. La traduction vise à donner une sémantique précise à ces schémas permettant ainsi de prouver l'exactitude de ces modèles et de vérifier les politiques de sécurité par rapport au modèle fonctionnel correspondant en utilisant les outils AtelierB prover et ProB animator. La spécification B obtenue est affinée successivement à une implémentation de type base de données, qui est basée sur le paradigme AOP. Les affinements B sont également prouvés pour s'assurer que l’implémentation est correcte par rapport à la spécification abstraite initiale. Le programme d’AspectJ traduit permet la séparation du code lié à la sécurité sécurité du reste de l'application. Cette approche permet d’éviter la diffusion du code de l'application, et facilite ainsi le traçage et le maintien.Enfin, nous développons un outil qui génère automatiquement la spécification B à partir des modèles UML, et la dérivation d'une implémentation d'AspectJ à partir de la spécification B affinée. L'outil aide à décharger les développeurs des tâches difficiles et à améliorer la productivité du processus de développement

In healthcare, data digitization and the use of the Electronic Health Records (EHR) offer several benefits, such as reduction of the space occupied by data, or the ease of data search or data exchanges. IT systems must gradually act as the archivists who manage the access over sensitive data. Those have to be checked to be consistent with patient privacy wishes, hospital rules, and laws and regulations.SGAC, or Solution de Gestion Automatisée du Consentement, aims to offer a solution in which access to patient data would be based on patient rules, hospital rules and laws. However, the freedom granted to the patient can cause several problems: conflicts, hiding of the needed data to heal the patient or simply data-capture error. Therefore, verification and validation of policies are crucial: to conduct this verification, formal methods provide reliable ways to verify properties like proofs or model checking.This thesis provides verification methods applied on SGAC for the patient: it introduces the formal model of SGAC, verification methods of properties such as data reachability or hidden data detection. To conduct those verification in an automated way, SGAC is modelled in B and Alloy; these different models provide access to the tools Alloy and ProB, and thus, automated property verification with model checking, Dans le domaine médical, la numérisation des documents et l’utilisation des dossiers patient électroniques (DPE, ou en anglais EHR pour Electronic Health Record) offrent de nombreux avantages, tels que le gain de place ou encore la facilité de recherche et de transmission de ces données. Les systèmes informatiques doivent reprendre ainsi progressivement le rôle traditionnellement tenu par les archivistes, rôle qui comprenait notamment la gestion des accès à ces données sensibles. Ces derniers doivent en effet être rigoureusement contrôlés pour tenir compte des souhaits de confidentialité des patients, des règles des établissements et de la législation en vigueur. SGAC, ou Solution de Gestion Automatisée du Consentement, a pour but de fournir une solution dans laquelle l’accès aux données du patient serait non seulement basée sur les règles mises en place par le patient lui-même mais aussi sur le règlement de l’établissement et sur la législation. Cependant, cette liberté octroyée au patient est source de divers problèmes : conflits, masquage des données nécessaires aux soins ou encore tout simplement erreurs de saisie. C’est pour cela que la vérification et la validation des règles d’accès sont cruciales : pour effectuer ces vérifications, les méthodes formelles fournissent des moyens fiables de vérification de propriétés tels que les preuves ou la vérification de modèles.Cette thèse propose des méthodes de vérification adaptées à SGAC pour le patient : elle introduit le modèle formel de SGAC, des méthodes de vérifications de propriétés telles l’accessibilité aux données ou encore la détection de document inaccessibles. Afin de mener ces vérifications de manière automatisée, SGAC est modélisé en B et Alloy ; ces différentes modélisations donnent accès aux outils Alloy et ProB, et ainsi à la vérification automatisée de propriétés via la vérification de modèles ou model checking

In general, computer software vulnerabilities are defined as special cases where an unexpected behavior of the system leads to the degradation of security properties or the violation of security policies. These vulnerabilities can be exploited by malicious users or systems impacting the security and/or operation of the attacked system. Since the literature on vulnerabilities is not always available to developers and the used tools do not allow detecting and avoiding them; the software industry continues to be affected by security breaches. Therefore, the detection of vulnerabilities in software has become a major concern and research area. Our research was done under the scope of the SHIELDS European project and focuses specifically on modeling techniques and formal detection of vulnerabilities. In this area, existing approaches are limited and do not always rely on a precise formal modeling of the vulnerabilities they target. Additionally detection tools produce a significant number of false positives/negatives. Note also that it is quite difficult for a developer to know what vulnerabilities are detected by each tool because they are not well documented. Under this context the contributions made in this thesis are: Definition of a formalism called template. Definition of a formal language, called Vulnerability Detection Condition (VDC), which can accurately model the occurrence of a vulnerability. Also a method to generate VDCs from templates has been defined. Defining a second approach for detecting vulnerabilities which combines model checking and fault injection techniques. Experiments on both approaches, De manière générale, en informatique, les vulnérabilités logicielles sont définies comme des cas particuliers de fonctionnements non attendus du système menant à la dégradation des propriétés de sécurité ou à la violation de la politique de sécurité. Ces vulnérabilités peuvent être exploitées par des utilisateurs malveillants comme brèches de sécurité. Comme la documentation sur les vulnérabilités n'est pas toujours disponible pour les développeurs et que les outils qu'ils utilisent ne leur permettent pas de les détecter et les éviter, l'industrie du logiciel continue à être paralysée par des failles de sécurité. Nos travaux de recherche s'inscrivent dans le cadre du projet Européen SHIELDS et portent sur les techniques de modélisation et de détection formelles de vulnérabilités. Dans ce domaine, les approches existantes sont peu nombreuses et ne se basent pas toujours sur une modélisation formelle précise des vulnérabilités qu'elles traitent. De plus, les outils de détection sous-jacents produisent un nombre conséquent de faux positifs/négatifs. Notons également qu'il est assez difficile pour un développeur de savoir quelles vulnérabilités sont détectées par chaque outil vu que ces derniers sont très peu documentés. En résumé, les contributions réalisées dans le cadre de cette thèse sont les suivantes: Définition d'un formalisme tabulaire de description de vulnérabilités appelé template. Définition d'un langage formel, appelé Condition de Détection de Vulnérabilité (VDC). Une approche de génération de VDCs à partir des templates. Définition d'une approche de détection de vulnérabilités combinant le model checking et l'injection de fautes. Évaluation des deux approches

The properties that we would like to express on data-intensive applications cannot be limited to static properties, called invariance properties, which depend on states taken at the same time. Indeed, some properties, called dynamic properties, may refer to the past or the future states of the system. Existing work on the verification of such properties typically use model checking whose effectiveness for data-intensive applications is rather limited due to the combinatorial explosion of the state space. In addition, the techniques, based on the proof, require fairly advanced knowledge and mathematical reasoning especially that they are not always supported by tools. To overcome these limitations, we propose in this thesis proof-based verification approaches that use the B formal method. We are mainly interested in reachability and precedence properties for which we defined formal rules to generate proof obligations that permit to discharge them. A reachability property expresses that there is at least one execution scenario that permits to reach a target state from a given initial state while a precedence property ensures that a given system state is always preceded by another state. To make these different approaches workable, we have developed a support tool that permits to discharge the users from tedious and error-prone tasks, Les propriétés que l’on souhaite exprimer sur les applications système d’information ne peuvent se restreindre aux propriétés statiques, dites propriétés d’invariance, qui portent sur des états du système pris au même moment. En effet, certaines propriétés, dites propriétés dynamiques, peuvent faire référence à l’état passé ou futur du système. Les travaux existants sur la vérification de telles propriétés utilisent généralement le model checking dont l’efficacité pour le domaine des systèmes d’information est plutôt réduite à cause de l’explosion combinatoire de l’espace des états. Aussi, les techniques, fondées sur la preuve, requièrent des connaissances assez avancées en termes de raisonnement mathématique et sont donc difficiles à mettre en œuvre d’autant plus que ces dernières ne sont pas outillées. Pour palier ces limites, nous proposons dans cette thèse des méthodes de vérification de propriétés dynamiques basées sur la preuve en utilisant la méthode formelle B. Nous nous intéressons principalement aux propriétés d’atteignabilité et de précédence pour lesquelles nous avons défini des méthodes de génération d’obligations de preuve permettant de les prouver. Une propriété d’atteignabilité permet d’exprimer qu’il existe au moins une exécution du système qui permet d’atteindre un état cible à partir d’un état initial donné. Par contre, la propriété de précédence permet de s’assurer qu’un état donné du système est toujours précédé par un autre état. Afin de rendre ces différentes approches opérationnelles, nous avons développé un outil support qui permet de décharger l’utilisateur de la tâche de génération d’obligations de preuve qui peut être longue et fastidieuse