Academic literature on the topic 'Sécurité des systèmes – Vérification de modèles (informatique)'

Les principaux objectifs poursuivis au cours de cette thèse sont en premier lieu de pouvoir combiner les avantages de l’apprentissage graphique probabiliste de modèles et de la vérification formelle afin de pouvoir construire une nouvelle stratégie pour les évaluations de sécurité. D’autre part, il s’agit d’évaluer la sécurité d’un système réel donné. Par conséquent, nous proposons une approche où un "Recursive Timescale Graphical Event Model (RTGEM)" appris d’après un flux d’évènements est considéré comme représentatif du système sous-jacent. Ce modèle est ensuite utilisé pour vérifier une propriété de sécurité. Si la propriété n’est pas vérifiée, nous proposons une méthodologie de recherche afin de trouver un autre modèle qui la vérifiera. Nous analysons et justifions les différentes techniques utilisées dans notre approche et nous adaptons une mesure de distance entre Graphical Event Models. La mesure de distance entre le modèle appris et le proximal secure model trouvé nous donne un aperçu d’à quel point notre système réel est loin de vérifier la propriété donnée. Dans un soucis d’exhaustivité, nous proposons des séries d’expériences sur des données de synthèse nous permettant de fournir des preuves expérimentales que nous pouvons atteindre les objectifs visés<br>The main objective of this thesis is to combine the advantages of probabilistic graphical model learning and formal verification in order to build a novel strategy for security assessments. The second objective is to assess the security of a given system by verifying whether it satisfies given properties and, if not, how far is it from satisfying them. We are interested in performing formal verification of this system based on event sequences collected from its execution. Consequently, we propose a model-based approach where a Recursive Timescale Graphical Event Model (RTGEM), learned from the event streams, is considered to be representative of the underlying system. This model is then used to check a security property. If the property is not verified, we propose a search methodology to find another close model that satisfies it. We discuss and justify the different techniques we use in our approach and we adapt a distance measure between Graphical Event Models. The distance measure between the learned "fittest" model and the found proximal secure model gives an insight on how far our real system is from verifying the given property. For the sake of completeness, we propose series of experiments on synthetic data allowing to provide experimental evidence that we can attain the desired goals

Dans cette thèse, nous nous intéressons à la vérification des protocoles de sécurité. Ce sont des programmes dont le but est d'établir une communication sûre entre plusieurs agents. Quasiment toutes les applications modernes ont besoin des protocoles de sécurité pour assurer leur bon fonctionnement, ce qui rend d'autant plus importante la question de leur correction et demande une réponse basée sur des arguments rigoureux. Les méthodes formelles, où les messages et les opérations sont abstraits par une algèbre de termes, se sont avérées cruciales dans cette démarche. Cependant, pour avoir une modélisation fidèle de la réalité, l'algèbrene peut être libre, mais doit incorporer des propriétés des algorithmes utilisées pour construire les messages. Dans ce contexte, motivés à la fois par des besoins pratiques et des intérêts théoriques, nous étudions les techniques générales pour la vérification des propriétés de sécurité de protocoles modulo une théorie équationnelle, à travers la résolution de contraintes de déductibilité<br>To enable formal and automated analysis of security protocols, one has to abstract implementations of cryptographic primitives by terms in a given algebra. However, the algebra can not be free, as cryptographic primitives have algebraic properties that are either relevant to their specification or else they can be simply observed in implementations at hand. These properties are sometimes essential for the execution of the protocol, but they also open the possibility for an attack, as they give to an intruder the means to deduce new information from the messages that he intercepts over the network. In consequence, there was much work over the last few years towards enriching the Dolev-Yao model, originally based on a free algebra, with algebraic properties, modelled by equational theories. In this thesis, driven by both practical and theoretical interests, we propose general decision procedures for the insecurity of protocols, that can be applied to several classes of equational theories

Alors que les systèmes embarqués sont de plus en plus nombreux, complexes, connectés et chargés de tâches critiques, la question de comment intégrer l'analyse précise de sécurité à la conception de systèmes embarqués doit trouver une réponse. Dans cette thèse, nous étudions comment les méthodes de vérification formelle automatiques peuvent aider les concepteurs de systèmes embarqués à évaluer l'impact des modifications logicielles et matérielles sur la sécurité des systèmes. Une des spécificités des systèmes embarqués est qu'ils sont décrits sous la forme de composants logiciels et matériels interagissant. Vérifier formellement de tels systèmes demande de prendre tous ces composants en compte. Nous proposons un exemple d'un tel système (basé sur Intel SGX) qui permet d'établir un canal sécurisé entre un périphérique et une application. Il est possible d'en vérifier un modèle de haut-niveau ou une implémentation bas-niveau. Ces deux niveaux diffèrent dans le degré d'intrication entre matériel et logiciel. Dans le premier cas, nous proposons une approche orientée modèle, à la fois au niveau partitionnement et conception logicielle, permettant une description à haut niveau d'abstraction du matériel et du logiciel et permettant une transformation de ces modèles en une spécification formelle sur laquelle une analyse de sécurité peut être effectuée avec l'outil ProVerif. Dans le second cas, nous considérons une implémentation logicielle et un modèle matériel plus concret pour effectuer des analyses de sécurité plus précises toujours avec ProVerif<br>As embedded systems become more complex, more connected and more involved in critical tasks, the question of how strict security analysis can be performed during embedded system design needs to be thoroughly addressed. In this thesis, we study how automated formal verification can help embedded system designers in evaluating the impact of hardware and software modifications on the security of the whole system. One of the specificities of embedded system design-which is of particular interest for formal verification-is that the system under design is described as interacting hardware and software components. Formally verifying these systems requires taking both types of components into account. To illustrate this fact, we propose an example of a hardware/software co-design (based on Intel SGX) that provides a secure channel between a peripheral and an application. Formal verification can be performed on this system at different levels: from a high-level view (without describing the implementations) or from a low-level implementation. These two cases differ in terms of how tightly coupled the hardware and software components are. In the first case, we propose a model-based approach-for both the partitioning and software design phases- which enables us to describe software and hardware with high-level models and enables a transformation of these models into a formal specification which can be formally analyzed by the ProVerif tool. In the second case, we consider a software implementation and a more concrete

Les protocoles de sécurité modernes peuvent impliquer un participant humain de façon à ce qu'il compare ou copie de courtes chaines de caractères faisant le pont entre différents appareils. C'est par exemple le cas des protocoles basés sur une authentification à facteur multiples comme les protocoles Google 2 factor ou 3D-Secure.Cependant, de telles chaines de caractères peuvent être sujettes à des attaques par force brute. Dans cette thèse nous proposons un modèle symbolique qui inclut les capacités de l'attaquant à deviner des secrets faibles et à produire des collisions avec des fonctions de hachage dont de l'application résulte une courte chaine de caractères. Nous proposons une nouvelle procédure de décision pour analyser un protocole (restreint à un nombre borné de sessions) qui se base sur de courtes chaines de caractères. Cette procédure a été intégré dans l'outil AKISS et testé sur les protocoles du standard ISO/IEC 9798-6:2010<br>Modern security protocols may involve humans in order to compare or copy short strings betweendifferent devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-Secure are typical examplesof such protocols. However, such short strings may be subject to brute force attacks. In this thesis we propose asymbolic model which includes attacker capabilities for both guessing short strings, and producing collisions whenshort strings result from an application of weak hash functions. We propose a new decision procedure for analyzing(a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in theAKISS tool and tested protocols from the ISO/IEC 9798-6:2010 standard

La criticité croissante des systèmes industriels les expose davantage aux menaces du monde cyber. En particulier les menaces persistantes avancées ou Advanced Persistent Threats (APT) sont des attaquants sophistiqués dotés de ressources conséquentes et ciblant spécifiquement les systèmes critiques. Les méthodologies de cyber-défense actuelles permettent de protéger les systèmes contre les cyber-menaces classiques mais elles peinent à contrer efficacement les APT. En effet, les APT usent de stratégies complexes et de tactiques de dissimulation qui les rendent difficile à contrecarrer. Pour répondre à ce besoin, la méthodologie d’Operational Design tirée des stratégies militaires permet de mieux comprendre l’établissement de stratégie de ces attaquants sophistiqués. Cette méthodologie axée sur la mission et adaptée au contexte des APT repose sur la fédération de plusieurs processus de spécification, de modélisation et d’analyse pour produire une stratégie opérationnelle. Pour évaluer cette approche, un outillage fédéré complet a été conçu et appliqué à un cas d’étude d’une mission d’attaque de système de pompage d’eau<br>Critical industrial systems are prime targets of cyber threats. In particular the Advanced Persistent Threats (APT) are sophisticated and well-resourced attacks targeting valuable assets. For APTs both the attack and the defense require advanced planning and strategies similar to military operations. The existing cyber-security-aware methodologies achieve valuable results for regular cyberthreats, however they fail to adequately address APTs due to their refined strategies and evasive tactics. The Operational Design methodology of military forces helps in better understanding how APTs devise their strategies. This mission-driven methodology adapted to the APT context relies on the federationof several processes of specification, modeling and analysis in order to produce an operational strategy. To evaluate this approach, a complete federation framework has been developed and applied to the case study of a mission of attack on a water pumping station

Les architectures de systèmes à logiciel posent des défis pour les experts de sécurité. nombreux travaux ont eu pour objectif d’élaborer des solutions théoriques, des guides méthodologiques et des recommandations, pour renforcer la sécurité et protéger ces systèmes.Une solution proposée est d’intégrer des patrons de sécurité comme solutions méthodologiques à adapter aux spécificités des architectures considérées. Une telle solution est considérée fiable si elle résout un problème de sécurité sans affecter les exigences du système.Une fois un modèle d’architecture implante les patrons de sécurisé, il est nécessaire de valider formellement ce nouveau modèle au regard des exigences attendues. Les techniques de model checking permettent cette validation en vérifiant, d’une part, que les propriétés des patrons de sécurité sont respectées et, d’autre part, que les propriétés du modèle initial sont préservées.Dans ce travail de thèse, nous étudions les méthodes et les concepts pour générer des modèles architecturaux respectant des exigences de sécurité spécifiques. Àpartir d’un modèle d’architecture logicielle, d’une politique de sécurité et d’une librairie des patrons de sécurité, nous souhaitons générer une architecture sécurisée. Chaque patron de sécurité est décrit par une description formelle de sa structure et de son comportement, ainsi qu’une description formelle des propriétés de sécurité associées à ce patron.Cette thèse rend compte des travaux sur l’exploitation de techniques de vérification formelle des propriétés, par model-checking. L’idée poursuivie est de pouvoir générer un modèle d’architecture qui implante des patrons de sécurité, et de vérifier que les propriétés de sécurité, comme les exigences de modèle, sont respectées dans l’architecture résultante.En perspective, les résultats de notre travail pourraient s'appliquer à définir une méthodologie pour une meilleure validation de la sécurité des systèmes industriels comme les SCADA<br>Software-based architectures pose challenges for security experts. Many studieshave aimed to develop theoretical solutions, methodological guides and recommendations to enhance security and protect these systems.One solution proposed is to integrate security patterns as methodological solutions to adapt to the specificities of the considered architectures. Such a solution is considered reliable if it solves a security problem without affecting systemrequirements. Once an architecture model implements the security patterns, it is necessary to formally validate this new model against the expected requirements. Model checking techniques allow this validation by verifying, on one hand, that theproperties of the security patterns are respected and, on the other hand, that the properties of the initial model are preserved.In this thesis work, we study the methods and concepts to generate architectural models that meet specific security requirements. Starting with a software architecture model, a security policy and a library of security patterns, we want to generate a secure architecture. Each security pattern is described by aformal description of its structure and behavior, as well as a formal description of the security properties associated with that pattern.This thesis reports work on the technical exploitation of formal verification of properties, using model-checking.The idea is to be able to generate an architecture model that implements security patterns, and to verify that the security properties, as well as the model requirements, are respected in the resulting architecture.In perspective, the results of our work could be applied to define a methodology for a better validation of the security of industrial systems like SCADA

Dans le domaine de la sécurité informatique, de nombreux travaux théoriques concernent les modèles et les règlements de sécurité en se situant très en amont des systèmes réellement implémentés. Cette thèse s'appuie sur les bases théoriques offertes par ces travaux pour fonder une méthode de vérification statique de logiciels applicatifs. Nous proposons pour cela des algorithmes d'analyse qui s'appliquent aux programmes sources et nous démontrons qu'ils sont corrects en les dérivant d'un modèle de sécurité formel. Ils sont utilisés concrètement pour analyser des programmes écrits en langage C. Après une présentation de la problématique de sécurité informatique, nous effectuons un inventaire des menaces et des attaques récemment constatées et nous montrons qu'il existe un besoin en matière de validation statique de logiciels existants. Nous proposons ensuite une méthodologie de vérification de programmes écrits en langage C par annotation de leur code source puis analyse automatique de celui-ci. Dans une seconde partie, nous cherchons à démontrer la correction des algorithmes d'analyse. Pour cela, nous partons d'un modèle formel de sécurité : le modèle de la causalité. Nous le modifions pour en faire un modèle calculatoire, puis nous l'appliquons à la sémantique opérationnelle d'un langage impératif. Nous démontrons alors que l'analyse de la sécurité, exprimée comme une sémantique non standard du langage, est correcte par rapport au modèle de sécurité. Nous examinons enfin les difficultés pratiques posées par l'analyse statique du langage C. Nous nous attachons à analyser ses particularités en termes de structures de donnée et de structures de contôle. Nous proposons des techniques pour résoudre les problèmes posés, en particulier par les variables de type pointeur et les instructions déstructurantes de type saut inconditionnel.

La SNCF cherche à mettre en place des solutions innovantes permettant d’améliorer la sécurité et les conditions de travail des chargés d’études lors des travaux d’automatisation. En partant de l’étude théorique du projet jusqu’à sa validation sur site, en passant par la mise en œuvre des programmes, du câblage des armoires, et de leur vérification sur plateforme et en usine, ces différentes tâches s’avèrent souvent être longues, complexes, et répétitives, ce qui a pour effet d’augmenter la charge de travail des chargés d’études. En vue d’améliorer les conditions de travail des chargés d’études, ce projet de recherche vise principalement à améliorer leurs méthodologies de vérification des programmes API (aspects fonctionnels et sécuritaires) et du câblage des armoires électriques. Ce projet intitulé « Vérification formelle et simulation pour la validation des programmes API des EALE » se décompose en deux axes :  la vérification hors ligne des programmes API : basée sur une approche formelle, la méthode s’appuie sur une modélisation de l’installation électrique, des programmes API et du cahier de recette dans le model-checker Uppaal. Le principe consiste à vérifier automatiquement si les programmes satisfont aux tests du cahier de recette.  la vérification en ligne du câblage des armoires de contrôle/commande/ protection grâce à un simulateur de partie opérative interfacé avec les armoires de contrôle/commande/protection (via une armoire de test). La vérification se fera de manière automatique et en ligne, toujours avec les tests du cahier de recette, et permettra de valider le câblage des armoires et les réglages des appareils de protection numérique<br>In order to keep its leadership in French rail market and to improve working conditions of its systems engineers during automation projects, the SNCF (French acronym for National Society of French Railways) wants to develop solutions increasing the productivity. One of these improvements focuses on the current methodology used by the systems engineers to verify and validate the control command system of electrical installations. This task remains one of the most important during an automation project because it is supposed to ensure installations safety, but it should be optimized. Through an industrial thesis financed by SNCF, the aim of this research project is to improve this method and reduce time validation of control command system by providing tools which will help systems engineers to verify and validate quickly and automatically the control command system during any automation project. It is composed of two axes : - Offline verification of PLC programs with model checking - Online validation of electrical cabinets with virtual commissioning

Garantir la sécurité d’une application tout au long de son cycle de vie est une tâche fastidieuse. Le choix, l’implémentation et l’évaluation des solutions de sécurité est difficile et sujette a des erreurs. Les compétences en sécurité ne sont pas répondues dans toutes les équipes de développement. Afin de réduire ce manque de compétences en sécurité, les développeurs ont a leurs disposition une multitude de documents décrivant des problèmes de sécurité et des solutions requises (i.e., vulnérabilités, attaques, principes de sécurité, patrons sécurité, etc.). Abstraites et informelles, ces documents sont fournis par des sources différentes et leur nombre est en constante croissance. Les développeurs sont noyés dans une multitude de documents ce qui fait obstruction à leur capacité à choisir, implémenter et évaluer la sécurité d’une application. Cette thèse aborde ces questions et propose un ensemble de méthodes pour aider les développeurs à choisir, implémenter et évaluer les solutions de sécurité face aux problèmes de sécurité. Ces problèmes sont matérialisés par les failles, les vulnérabilités, les attaques, etc. et les solutions fournies par des patrons de sécurité. Cette thèse introduit en premier une méthode pour aider les développeurs dans l’implémentation de patrons de sécurité et l’estimation de leur efficacité face aux vulnérabilités. Puis elle présente trois méthodes associant les patrons de sécurité, les vulnérabilités, les attaques, etc. au sein d’une base de connaissance. Cette dernière permet une extraction automatique de classifications de patrons et améliore la rapidité et la précision des développeurs dans le choix des patrons de sécurité face à une vulnérabilité ou une attaque. En utilisant la base de connaissance, nous présentons une méthode pour aider les développeurs dans la modélisation des menaces ainsi que la générations et l’exécution des cas de test de sécurité. La méthode est évaluée et les résultats montrent que la méthode améliore l’efficacité, la compréhensibilité et la précision des développeurs dans le choix des patrons de sécurité et d’écriture des cas de test de sécurité<br>Ensuring the security of an application through its life cycle is a tedious task. The choice, the implementation and the evaluation of security solutions is difficult and error prone. Security skills are not common in development teams. To overcome the lack of security skills, developers and designers are provided with a plethora of documents about security problems and solutions (i.e, vulnerabilities, attacks, security principles, security patterns, etc.). Abstract and informal, these documents are provided by different sources, and their number is constantly growing. Developers are drown in a sea of documentation, which inhibits their capacity to design, implement, and the evaluate the overall application security. This thesis tackles these issues and presents a set of approaches to help designers in the choice, the implementation and the evaluation of security solutions required to overcome security problems. The problems are materialized by weaknesses, vulnerabilities, attacks, etc. and security solutions are given by security patterns.This thesis first introduces a method to guide designers implement security patterns and assess their effectiveness against vulnerabilities. Then, we present three methods associating security patterns, attacks, weaknesses, etc. in a knowledge base. This allows automated extraction of classifications and help designers quickly and accurately select security patterns required to cure a weakness or to overcome an attack. Based on this nowledge base, we detaila method to help designers in threat modeling and security test generation and execution. The method is evaluated and results show that the method enhances the comprehensibility and the accuracy of developers in the security solutions choice, threat modeling and in the writing of security test cases

Avec la complexité croissante des systèmes informatiques se pose la question de la mise en oeuvre de méthodes automatiques pour leur vérification formelle. Parmi ces méthodes, le model-checking se fonde sur l'exploration exhaustive du comportement d'un système. Plus celui-ci sera complexe, plus cette exploration se traduira par une explosion combinatoire de l'espace des états du système. Diverses approches ont été proposées pour résoudre ce problème, notamment les méthodes symboliques qui sont bases sur une représentation compacte d'ensembles d'états. Depuis les travaux de R. E. Bryant et la définition des Diagrammes de Décision Binaires (BDD), de nombreuses représentations en DAG d'espaces d'états ont vu le jour, parmi celles-ci, on trouve les Diagrammes de Décision de Données (DDD), qui procurent une représentation compacte d'ensemble d'états et sont pourvus de mécanismes de parcours définis localement pour la réalisation des modifications sur ces états et des opérations ensemblistes. Parallélement, les travaux de G. J. Holzmann ont abouti à la création de l'outil de vérification SPIN, basé sur des méthodes énumératives explicites, pour des systèmes décrits en langage Promela. Ces systèmes sont proches de ceux qui sont utilisés pour la synthèse de haut niveau. Nous proposons une approche de vérification symbolique de systèmes matériels décrits dans un sous-ensemble du langage Promela. La représentation symbolique d'ensembles d'états est basée sur les Diagrammes de Décision de Données qui évitent de d'écrire le système au niveau booléen. Nous présentons d'abord la sémantique du langage Promela ainsi que les DDD puis les mécanismes mis en oeuvre pour la vérification de propriétés de logique CTL. Les conclusions tirées de cette première étape conduisent à proposer l'utilisation des Diagrammes de Décision d'Ensembles (SDD) pour améliorer les performances de la vérification automatique. Nous montrons que, bien que pourvus d'une implémentation et d'une terminologie différentes, il se prévalent du même formalisme que les DDD tout en procurant un étiquetage symbolique des arcs de la structure. Nous expérimentons ensuite cette approche sur des systèmes académiques et sur des systèmes issus d'applications industrielles. Ces expérimentations corroborent nos premiers résultats : les SDD couplés aux méthodes de saturation constituent une alternative sérieuse pour la vérification de systèmes à fort degré de concurrence. Nous proposons des perspectives de recherche pour améliorer encore la vérification de tels systèmes mais également pour introduire le concept de hiérarchie dans la description du système