Le formalisme des réseaux de Petri hybrides fonctionnels, notés HFPN pour Hybrid Functional Petri Nets en anglais, a démontré sa capacité à simuler les systèmes biologiques. L’inconvénient d’un formalisme aussi expressif est la difficulté d’exécuter des vérifications de propriétés dynamiques. Dans cette thèse, nous proposons une procédure de model-checking pour les réseaux de Petri hybrides temporisés, notés THPN pour Timed Hybrid Petri Nets en anglais, une sous-classe des HFPN. Cette procédure est basée sur la traduction du modèle THPN et de la propriété étudiée en automates temps-réel. Ceci est alors appliqué pour modéliser les régulations responsables de la métamorphose amphibienne. / The formalism of Hybrid Functional Petri Nets (HFPN) has proved its convenience for simulating biological systems. The drawback of the noticeable expressiveness of HFPN is the difficulty to perform formal verifications of dynamical properties. In this thesis, we propose a model-checking procedure for Timed Hybrid Petri Nets (THPN), a sub-class of HFPN. This procedure is based on the translation of the THPN model and of the studied property into real-time automata. It is applied to model regulations responsible for amphibian metamorphosis.

Les logiciels multi-partis sont des applications distribuées sur le web qui mettent en oeuvre des fonctions collaboratives. Ces applications sont les principales cibles des attaquants qui exploitent des vulnérabilités logicielles dans le cadre d'activités malveillantes. Récemment, un type moins connu de vulnérabilité, les anomalies logiques, a attiré l'attention des chercheurs. Sur la base d'informations tirées de la documentation des applications, il est possible d'appliquer deux techniques de test: la vérification du modèle, autrement appelé ``model checking'', et les tests de sécurité de type ``boîte noire''. Le champs d'application du model checking ne prend pas en suffisamment en compte les implémentations actuelles, tandis que les tests de type boîte noire ne sont pas assez sophistiqués pour découvrir les vulnérabilités logique. Dans cette thèse, nous présentons deux techniques d'analyse modernes visant à résoudre les inconvénients de l'état de l'art. Pour commencer, nous présentons la vérification de deux protocoles de sécurité utilisant la technique du model checking. Ensuite, nous nous concentrons sur l'extension du model checking pour soutenir les tests automatisés d'implémentations. La seconde technique consiste en une analyse boîte noire qui combine l'inférence du modèle, l'extraction du processus et du flot de donnée, ainsi qu'une génération de tests basés sur les modèles d'attaque d'une application. En conclusion, nous discutons de l'application de techniques développées au cours de cette thèse sur des applications issues d'un contexte industrielle. / Multi-party business applications are distributed computer programs implementing collaborative business functions. These applications are one of the main target of attackers who exploit vulnerabilities in order to perform malicious activities. The most prevalent classes of vulnerabilities are the consequence of insufficient validation of the user-provided input. However, the less-known class of logic vulnerabilities recently attracted the attention of researcher. According to the availability of software documentation, two testing techniques can be used: design verification via model checking, and black-box security testing. However, the former offers no support to test real implementations and the latter lacks the sophistication to detect logic flaws. In this thesis, we present two novel security testing techniques to detect logic flaws in multi-party business applicatons that tackle the shortcomings of the existing techniques. First, we present the verification via model checking of two security protocols. We then address the challenge of extending the results of the model checker to automatically test protocol implementations. Second, we present a novel black-box security testing technique that combines model inference, extraction of workflow and data flow patterns, and an attack pattern-based test case generation algorithm. Finally, we discuss the application of the technique developed in this thesis in an industrial setting. We used these techniques to discover previously-unknown design errors in SAML SSO and OpenID protocols, and ten logic vulnerabilities in eCommerce applications allowing an attacker to pay less or shop for free.

Zugl.: Darmstadt, Techn. Univ., Diss., 2006

Techn. Univ., Diss--Darmstadt, 2006.

Freiburg (Breisgau), University, Diss., 2001.

Nous étudions le problème de la synthèse automatique de programmes dans des architectures multi-composants tels qu'elles respectent les spécifications par construction. Le principal objectif de cette thèse est de développer des procédures pour résoudre le problème de synthèse qui peut conduire à des implémentations efficaces. Chaque composant a une observation partielle sur l'état global du système multi-composants. Le problème est alors de fournir des protocoles basés sur les observations tel que les composants synthétisés assurent les spécifications pour tout le comportement de leur environnement. L'environnement peut être antagoniste, ou peut avoir ses propres objectifs et se comporter de façon rationnelle. Nous étudions d'abord le problème de synthèse lorsque l'environnement est présumé antagoniste. Pour ce contexte, nous proposons une procédure "Safraless" pour la synthèse d'un composant partiellement informé et un environnement omniscient à partir de spécications KLTL+. Elle est implémentée dans l'outil Acacia-K. Ensuite, nous étudions le problème de synthèse lorsque les composants de l'environnement ont leurs propres objectifs et sont rationnels. Pour le cadre plus simple de l'information parfaite, nous fournissons des complexités serrées pour des objectifs omega-réguliers particuliers. Pour le cas de l'information imparfaite, nous prouvons que le problème de la synthèse rationnelle est indécidable en général, mais nous regagnons la décidabilité si on demande à synthétiser un composant avec observation partielle contre un environnement multi-composante, omniscient et rationnel / We study the problem of automatic synthesis of programs in multi-component architectures such that they satisfy the specifications by construction. The main goal of the thesis is to develop procedures to solve the synthesis problem that may lead to efficient implementations.Each component may have partial observation on the global state of the multi-component system.Therefore, the synthesis problem asks to provide observation-based protocols for the components that have to be synthesized that ensure that specifications hold on all interactions with their environment.The environment may be antagonist, or may have its own objectives and behave rationally.We first study the synthesis problem when the environment is presumed to be completely antagonist. For this setting, we propose a "Safraless" procedure for the synthesis of one partially informed component and an omniscient environment from KLTL+ specifications. It is implemented in the tool Acacia-K. Secondly, we study the synthesis problem when the components in the environment have their own objectives and are rational. For the more relaxed setting of perfect information, we provide tight complexities for particular omega-regular objectives. Then, for the case of imperfect information, we prove that the rational synthesis problem is undecidable in general, but we gain decidability if is asked to synthesize only one component against a rational omniscient environment

Les multiprocesseurs et microprocesseurs multicœurs modernes mettent en oeuvre des modèles mémoires dits faibles ou relâchés, dans dans lesquels l'ordre apparent des opérations mémoire ne suit pas la cohérence séquentielle (SC) proposée par Leslie Lamport. Tout programme concurrent s'exécutant sur une telle architecture et conçu avec un modèle SC en tête risque de montrer à l'exécution de nouveaux comportements, dont certains sont potentiellement des comportements incorrects. Par exemple, un algorithme d'exclusion mutuelle correct avec une sémantique par entrelacement pourrait ne plus garantir l'exclusion mutuelle lorsqu'il est mis en oeuvre sur une architecture plus relâchée. Raisonner sur la sémantique de tels programmes s'avère très difficile. Par ailleurs, bon nombre d'algorithmes concurrents sont conçus pour fonctionner indépendamment du nombre de processus mis en oeuvre. On voudrait donc pouvoir s'assurer de la correction d'algorithmes concurrents, quel que soit le nombre de processus impliqués. Pour ce faire, on s'appuie sur le cadre du Model Checking Modulo Theories (MCMT), développé par Ghilardi et Ranise, qui permet la vérification de propriétés de sûreté de programmes concurrents paramétrés, c'est-à-dire mettant en oeuvre un nombre arbitraire de processus. On étend cette technologie avec une théorie permettant de raisonner sur des modèles mémoires faibles. Le résultat ce ces travaux est une extension du model checker Cubicle, appelée Cubicle-W, permettant de vérifier des propriétés de systèmes de transitions paramétrés s'exécutant sur un modèle mémoire faible similaire à TSO. / Modern multiprocessors and microprocesseurs implement weak or relaxed memory models, in which the apparent order of memory operation does not follow the sequential consistency (SC) proposed by Leslie Lamport. Any concurrent program running on such architecture and designed with an SC model in mind may exhibit new behaviors during its execution, some of which may potentially be incorrect. For instance, a mutual exclusion algorithm, correct under an interleaving semantics, may no longer guarantee mutual exclusion when implemented on a weaker architecture. Reasoning about the semantics of such programs is a difficult task. Moreover, most concurrent algorithms are designed for an arbitrary number of processus. We would like to ensure the correctness of concurrent algorithms, regardless of the number of processes involved. For this purpose, we rely on the Model Checking Modulo Theories (MCMT) framework, developed by Ghilardi and Ranise, which allows for the verification of safety properties of parameterized concurrent programs, that is to say, programs involving an arbitrary number of processes. We extend this technology with a theory for reasoning about weak memory models. The result of this work is an extension of the Cubicle model checker called Cubicle-W, which allows the verification of safety properties of parameterized transition systems running under a weak memory model similar to TSO.

Model checking is used to aid in the design and verification of complex concurrent systems. An abstracted finite state model of a system and a set of mathematically based correctness properties based on the design specifications are defined. The model checker then performs an exhaustive state space search of the model, checking that the correctness properties hold at each step. This thesis describes how the SPIN model checker has been used to find and correct problems in the software design of a distributed marine vessel control system currently under development at a control systems specialist in New Zealand. The system under development is a mission critical control system used on large marine vessels. Hence, the requirement to study its architecture and verify the implementation of the system. The model checking work reported here focused on analysing the implementation of the Time-Triggered Controller-Area-Network (TTCAN) protocol, as this is used as the backbone for communications between devices and thus is a crucial part of their control system. A model of the ISO TTCAN protocol has been created using the SPIN model checker. This was based on work previously done by Leen and Heffernan modelling the protocol with the UPPAAL model checker [Leen and Heffernan 2002a]. In the process of building the ISO TTCAN model, a set of general techniques were developed for model checking TTCAN-like protocols. The techniques developed include modelling the progression of time efficiently in SPIN, TTCAN message transmission, TTCAN error handling, and CAN bus arbitration. These techniques then form the basis of a set of models developed to check the sponsoring organisation’s implementation of TTCAN as well as the fault tolerance schemes added to the system. Descriptions of the models and properties developed to check the correctness of the TTCAN implementation are given, and verification results are presented and discussed. This application of model checking to an industrial design problem has been successful in identifying a number of potential issues early in the design phase. In cases where problems are identified, the sequences of events leading to the problems are described, and potential solutions are suggested and modelled to check their effect of the system.

Title: GIMPLE Model Checker Author: Ondrej Krč-Jediný Department: Department of Distributed and Dependable Systems Supervisor: RNDr. Ondřej Šerý Ph.D. Supervisor's e-mail address: Ondrej.Sery@mff.cuni.cz The goal of the thesis is a prototype implementation of explicit-state model checker of C - an advanced tool for finding errors in programs. This tool ex- plores all possible paths of program execution as well as all thread interleavings. It is based on GIMPLE - output of front-end of GCC compiler, which is the input language for GMC. The thesis is based on the previous work 'Memory represen- tation for GIMPLE Model Checker', that implements work with memory for this tool. Since it is based on GIMPLE, it makes it possible to verify systems directly in C. In addition, it is easily extensible to other languages supported by GCC. Keywords: model checking, GIMPLE, GCC, C 1

Dans ce mémoire, on généralise la notion de vérification automatique de modèles au contexte flou. On définit des structures de Kripke floues et on leur associe des logiques temporelles floues, dénotées NCTL * et NCTL. On vérifie que les opérateurs de la logique NCTL sont monotones et qu'il y a moyen de faire de la vérification de modèles dans ce contexte. On en fait alors la démonstration.