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.

International audience; In this paper, we show the application of ASTDs to intrusion detection. ASTD is an executable, modular and graphical notation that allows for the composition of hierarchical state machines with process algebra operators to model complex attack phases. Overall, ASTD attack specifications are more concise than industrial tools like Snort, Zeek, and other attack languages in the literature. For intrusion detection, iASTD (the ASTD interpreter) and Zeek provided similar results. iASTD produced less false positives and a smaller number of true positives per attack than Snort, which is an important factor to deal with huge amounts of events. The processing time of iASTD on the real-time testbed is slower than Snort and Zeek, but it can be improved by compiling ASTD specifications into Zeek scripts.

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; This paper describes a case study of the SysML/KAOS method for a road transportation system for the City of Montreal (VdM), the second-largest city in Canada. The transportation system was developed from unstructured requirements represented in textual and schematic documents. Therefore, the VdM wanted to investigate new ways of organising and analysing the requirements of traffic projects, in order to increase the level of confidence in their safety, usability and reusability. This paper describes the formal specification, verification and validation of system requirements and provides an appraisal of the SysML/KAOS requirements engineering method on an industrial-scale case study. SysML/KAOS is designed within the ANR FORMOSE project to bridge the gap between stakeholder needs and the formal specification of system functionalities and domain constraints. The method has proven useful to deal with the seven refinement levels, twelve components (human, hardware, software and cyber-physical) and a hundred functional and non-functional goals that constitute the specification of the road transportation system, mainly focused on the safe movement of vehicles on road. It especially facilitated their validation with VdM stakeholders who had never dealt with formal methods and requirements engineering. Animation tools (ProB and B-Motion Studio) were also used to validate the formal specification with VdM stakeholders. This paper also reports improvements identified to enhance the expressiveness of SysML/KAOS goal modeling languages during validation sessions with VdM stakeholders. This includes the introduction of a non-functional goal refinement strategy based on logical formulas and of an obstacle modeling language.

International audience; This paper is about the formal specification of requirements of a rail communication protocol called Saturn, proposed by ClearSy systems engineering, a French company specialised in safety critical systems. The protocol was developed and implemented within a rail product, widely used, without modeling, verifying and even documenting its requirements. This paper outlines the formal specification, verification and validation of Saturn’s requirements in order to guarantee its correct behavior and to allow the definition of slightly different product lines. The specification is performed according to SysML/KAOS, a formal requirements engineering method developed in the ANR FORMOSE project for critical and complex systems. System requirements, captured with a goal modeling language, give rise to the behavioral part of a B System specification. In addition, an ontology modeling language allows the specification of domain entities and properties. The domain models thus obtained are used to d erive the structural part of the B System specification obtained from system requirements. The B System model, once completed with the body of events, can then be verified and validated using the whole range of tools that support the B method. Five refinement levels of the rail communication protocol were constructed. The method has proven useful. However, several missing features were identified. This paper also provides a formally defined extension of the modeling languages to fill the shortcomings.

International audience; Nowadays, network technologies are essential for transferring and storing various information of users, companies, and industries. However, the growth of the information transfer rate expands the attack surface, offering a rich environment to intruders. Intrusion detection systems (IDSs) are widespread systems able to passively or actively control intrusive activities in a defined host and network perimeter. Recently, different IDSs have been proposed by integrating various detection techniques, generic or adapted to a specific domain and to the nature of attacks operating on. The cybersecurity landscape deals with tremendous diverse event streams that exponentially increase the attack vectors. Event stream processing (ESP) methods appear to be solutions that leverage event streams to provide actionable insights and faster detection. In this paper, we briefly describe domains (as well as their vulnerabilities) on which recent papers were-based. We also survey standards for vulnerability assessment and attack classification. Afterwards, we carry out a classification of IDSs, evaluation metrics, and datasets. Next, we provide the technical details and an evaluation of the most recent work on IDS techniques and ESP approaches covering different dimensions (axes): domains, architectures, and local communication technologies. Finally, we discuss challenges and strategies to improve IDS in terms of accuracy, performance, and robustness.

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.

International audience; Algebraic State-Transition Diagrams (ASTDs) are extensions of common automata and statecharts that can be combined with process algebra operators like sequence, choice, guard and quantified synchronization. They were previously introduced for the graphical representation, specification and proof of information systems. In an attempt to use ASTDs to specify cyber attack detection, we have identified a number of missing features in ASTDs. This paper extends the ASTD notation with state variables (attributes), actions on transitions, and a new operator called flow which corresponds to AND states in statecharts and is a compromise between interleaving and synchronization in process algebras. We provide a formal structured operational semantics of these extensions and illustrate its implementation in an OCaml-based interpreter called iASTD and the model checker ProB. Extended ASTDs are illustrated in a case study in cyber attack detection

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 is about the extension of the SysML/KAOS requirements engineering method with domain models expressed as ontologies. More precisely, it concerns the translation of these ontologies into B System for system construction. The contributions of this paper are twofold. The first one is a formal semantics for the ontology modeling language. The second one is the formal definition of translation rules between ontologies and B system specifications in order to provide the structural part of the formal specification. These translation rules are modeled in Event-B. Their consistency and completeness are proved using Rodin. We show that they are structure preserving (two related elements within the source model remain related within the target model), by proving various isomorphisms between the ontology and the B System specification

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.

Cloud environments are being increasingly used for the deployment and execution of complex applications and particularly component-based ones. They are expected to provide elasticity, among other characteristics, in order to allow a deployed application to rapidly change the amount of its allocated resources in order to meet the variation in demand while ensuring a given Quality of Service (QoS). However, establishing a correct elastic component-based application is not guaranteed in Cloud. Indeed, applying elasticity mechanisms should preserve functional properties and improve non-functional properties related to QoS, performance and resource consumption. In this paper, we propose an approach for the verification and deployment of elastic component-based applications. Our approach is based on the Event-B formal method. In fact, we formally model the component artifacts using Event-B and we define the Event-B events that model the elasticity mechanisms (scaling up and down) for component-based applications. Furthermore, we formally verify that our approach preserves the semantics of the component-based applications by using the proof obligations and the ProB animator. Once the elastic component-based applications are validated, they can be deployed in a Cloud environment using an elastic deployment framework which we have developed.

International audience; This paper investigates the verification ofaccess control policies for SGAC, a new healthcare access-control model, using Alloy and ProB, two first orderlogic model checkers based on distinct technologies.SGAC supports permission and prohibition, ruleinheritance among subjects and resources and conflictsresolution. In order to protect patient privacy while ensuringeffective caregiving in safety-critical situations, we check different properties such as accessibility, ineffectiverule detection. Our performance results showthat ProB performs two orders of magnitude betterthan Alloy. Results are promising enough to considerProB for verifying patient policies in SGAC.

International audience; Configurable process models are recently gaining momentum as a basis for process design by reuse. Such models are designed in a generic manner to group common and variable parts of similar processes. Since these processes are usually large and complex, their configuration becomes manifestly a difficult task. This is why, an increasing attention is being paid to help achieving the process models configuration in a correct and domain-compliant manner. In this work, we propose an Event-B based formal approach that guides the process analyst to easily derive correct process variants while considering business domain constraints provided by configuration guidelines. To show the effectiveness of our approach, we conduct experiments on a case study

International audience; A configurable process model captures a family of similar processes. Such models can be configured to obtain a process variant according to specific requirements. With this aim, several approaches have been proposed for the configuration of process models. Nevertheless, an increasing attention is being paid to achieve this in a sound manner due to the complex inter-dependencies between the configuration decisions. In this work, we aim to guide the process analyst to easily configure process models while preserving soundness. To do so, we propose a formal approach for ensuring correctness of business process configurations while considering structural constraints they have to obey. Specifically, using the Event-B language, we formally define a configurable process model, its correctness-preserving conditions and its configuration constraints

International audience; This paper presents SGAC (\textit{Solution de Gestion Automatisée du Consentement, automatised consent management solution}), a new healthcare access control model and its support tool, that manages patient wishes regarding access to their electronic health record (EHR). The development of this model has been achieved in the scope of a project with the Sherbrooke University Hospital, and thus has been adapted to take into account laws and regulations applicable in Québec and Canada, as they set bounds to patient wishes: under strictly defined contexts, patient consent can be overridden to protect his/her life. Moreover, since patient wishes and laws can be in conflict, SGAC provides a mechanism to address this problem. Besides, laws do not cover all cases where consent should be overridden to ensure patient safety. To this end, we define a formal model of SGAC which allows for property verification, making it possible to detect these cases. A performance comparison with XACML (WSO2/Balana) is presented and demonstrates the superior performances of SGAC

International audience; Currently, it is well recognized that coupling graphical and formal notations offers several advantages. Indeed, even if a graphical representation permits to design a visual, synthetic and user-friendly view of the system, it may be source of ambiguity and does not permit any formal verification. Formal methods help to remedy these shortcomings by giving a precise semantics to graphical notations such that it becomes possible to verify a large range of properties and even to generate correct implementations. Nevertheless, users cannot take a full advantage of the benefits of such a combination if it is not supported by an automatic tool that liberates them from the tedious translation activity. Following this direction, the present paper describes the main functionalities of a tool that automatically generates a formal secure access control filter for information systems. The goal of the filter is to regulate the access to data of an information system according to a set of static and dynamic rules. Data are described using a UML class diagram, whereas the static and dynamic rules are modeled using \textsc{SecureUML} and UML activity diagrams respectively. Basically, the tool automatically generates the B formal specification corresponding to these diagrams and the filter

International audience; Nowadays, a growing number of companies are using Cloud Computing to optimize their business processes by using dynamically scalable and often virtualized resources on demand. Nevertheless, due to the lack of explicit and formal description of the resource perspective in existing business processes, Cloud resource allocation behavior cannot be efficiently and correctly managed. In this paper, we aim at formally verifying resource allocation in business processes using Event-B. More precisely, our aim is to specify the resource allocation behavior both at design time and at runtime, and to check its correctness according to users' needs. Our model also takes into account different cloud properties such as elasticity and shareability. In order to show its feasibility, our approach has been tested using a use case study from an industrial partner

International audience; With the advent of the internet, most organizations offer more and more access to their information systems in order to increase their benefits. However, such an opening may cause security issues if sufficient precautions are not taken. An adequate solution to secure access to information systems consists in (1) defining the sufficient security policies and (2) ensuring their correct deployment on a given technological infrastructure. The present paper deals with the first point by introducing a formal approach that permits to develop a secure filter for an information system that respects different kinds of security rules: functional, static and dynamic rules. The proposed approach uses the \texttt{SecureUML} language to express the static rules and adapts the UML activity diagrams for dynamic ones while the structure of the manipulated data and the functionalities are expressed using a UML class diagram. Starting from these graphical notations, the approach consists in mapping them into a B formal specification to ensure their consistency and validate the system. Finally, a proved filter, which permits to take into account different security rules, is formally derived using the B refinement technique

International audience; In UML modeling, class diagrams permit to capture the entities involved in a system but also the associations they have with each other. These associations are characterized by a multiplicity on each role to state the min-max number of instances of the opposite class that can be linked to each instance of the class associated with the role. Since these multiplicities may be conflicting, it becomes necessary to check the global consistency of a class diagram. Such verification will ensure that it is possible to find an instantiation of the diagram that satisfies all the multiplicities. In this paper, we describe an automatized approach that permits to validate a class diagram by exhibiting a particular instance. Basically, this approach proceeds in two main steps: first, the multiplicities are represented as a mathematical model, then a constraint solver is used to determine whether it has at least one solution. The correctness of the approach, which is supported by an automatic tool, has been carried out using the B formal method

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.

International audience; This chapter presents the proof process used by Thales and Autonomous Operator of Parisian Transports (RATP) to demonstrate the safety of the signaling systems used for the RATP network in Paris. It introduces the rail application concerned by the author's proof activities, the Thales system used for the metro. The chapter then presents the models used in the formal proof process, before describing the proof suite designed by Prover Technology. The results of application of the proof process to the Thales signaling system for RATP line are described and discussed in detail, before considering a number of potential improvements. The chapter presents a brief overview of the architecture of the PMI system. It discusses the computerized interlocking module (CIM) subsystem, which constitutes the operational core of the signaling system

International audience; Temporal properties are very common in various classes of systems, including information systems and security policies. This paper investigates two verification methods, proof and model checking, for one of the most frequent patterns of temporal property, the absence pattern. We explore two model-based specification techniques, B and Alloy, because of their adequacy for easily specifying systems with complex data structures, like information systems. We propose a first-order, assertion-based, sound and complete strategy to verify the absence pattern. This enables the proof of the absence pattern using conventional first-order provers. We show that the use of assertions significantly increases the size of the models that can be checked, when compared to traditional LTL model checking techniques. The approach is illustrated throughout a case study.

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 proposes an approach to prove interference freedom for a reach ability property of the form AG (psi => EF phi) in a B specification. Such properties frequently occur in security policies and information systems. Reach ability is proved by constructing using stepwise algorithmic refinement an abstract program that refines AG (psi => EF phi). We propose proof obligations to show non-interference, ie, to prove that other operations can be executed in interleaving with this program while preserving the reach ability property, to cater for the multi-user aspect of information systems. Proof obligations are discharged using conventional B provers (eg, Atelier B). Since refinement preserves these reach ability properties and non-interference, proofs can be conducted on abstract machines rather than implementation code

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; Traditionally, a security policy is defined from an informal set of requirements, generally written using natural language. It is then difficult to appreciate the compatibility degree of the manually generated security policy with the informal requirements definition. The idea of this paper is to automate the process of deriving the formal security policy, using a more structured specification of the security objectives issued by the administrator of the information system to be secured. We chose the goal-oriented methodology KAOS to express the functional objectives, then based on the results of a risk analysis, we integrate the security objectives to the obtained KAOS framework. Finally, through a process of transformation applied to this structured security objectives specification, we automatically generate the corresponding security policy. This policy is consistent with the access control model OrBAC (Organization Access Control).

International audience; This paper gives an overview of a formal approach for detecting vulnerabilities in C programs using the B formal method. Vulnerabilities denote faults that may be introduced unintentionally into programs making them behave incorrectly. Such faults (or programing errors) may lead to unpredictable behavior and even worse well-motivated attackers may exploit them later to cause real damages. Basically, the proposed approach consists in translating the vulnerable aspects of a C program into a B specification. On this B specification proof and model checking activities are performed in order to detect the presence or absence of vulnerabilities. Compared to the existing vulnerability detection techniques, a proof-based approach permits to eliminate false alarms and denial of service attacks

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; Maintaining integrity constraints in information systems is a real issue. In our previous work, we have defined a formal approach that derives B formal specifications from a UML description of the system. Basically, the generated B specification is composed of a set of variables modeling data and a set of operations representing transactions. The integrity constraints are directly specified as B invariant properties. So far, the operations we generate establish only a reduced class of constraints. In this paper, we describe a systematic approach to identify preconditions that take a larger class of invariants into account. The key idea is the definition of rewriting and simplification rules that we apply to the B invariants.

International audience; Security and reliability are of paramount importance in designing and building real-time systems because any security failure can put the public and the environment at risk.In this paper, we propose a framework to take timed security requirements into account from the design stage of the system building. Our approach consists of two main steps.First, the system behavior is specified based on its functional requirements using TEFSM (Timed Extended Finite StateMachine) formalism. Second, this model is augmented by applying a set of dedicated algorithms to integrate timed security properties specified in Nomad language. Nomad is a formal language well adapted to express timed security properties with timed constraints. We also briefly present a France Telecom1 Travel system as a case study to demonstrate the reliability of our framework

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 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 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.

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 to model the application domain of the system and which would be compatible with the requirements modeling language. This includes the definition of the domain modeling language and of mechanisms for leveraging domain modeling to provide the structural part of the B System specification obtained from requirements models. The defined language uses ontologies to allow the formal representation of system domain. Moreover, the established correspondence links and rules, formally verified, allow both propagation and backpropagation of additions and deletions, between domain models and B System specifications. An important part of the thesis is also devoted to assessment of the SysML/KAOS method on case studies. Furthermore, since the systems naturally break down into subsystems (enabling the distribution of work between several agents: hardware, software and human), SysML/KAOS goal models allow the capture of assignments of requirements to subsystems responsible of their achievement. This thesis therefore describes the mechanisms required to formally guarantee that each requirement assigned to a subsystem will be well achieved by the subsystem, within the constraints defined by the high-level system and 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 logiques du modèle de domaine, qui donnent lieu aux propriétés et invariants du modèle B System, et du corps des évènements B System, ainsi que les tâches de vérification et validation formelles sont coûteuses en temps et nécessitent l’implication d’experts en méthodes formelles. Il s’agit là du prix à payer pour des exigences formellement correctes.

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