Dissertations / Theses: 'Sécurité des systèmes – Méthodes formelles (informatique)'

1

Rauzy, Pablo. "Méthodes logicielles formelles pour la sécurité des implémentations de systèmes cryptographiques." Thesis, Paris, ENST, 2015. http://www.theses.fr/2015ENST0039/document.

Full text

Abstract:

Les implémentations cryptographiques sont vulnérables aux attaques physiques, et ont donc besoin d'en être protégées. Bien sûr, des protections défectueuses sont inutiles. L'utilisation des méthodes formelles permet de développer des systèmes tout en garantissant leur conformité à des spécifications données. Le premier objectif de ma thèse, et son aspect novateur, est de montrer que les méthodes formelles peuvent être utilisées pour prouver non seulement les principes des contre-mesures dans le cadre d'un modèle, mais aussi leurs implémentations, étant donné que c'est là que les vulnérabilités physiques sont exploitées. Mon second objectif est la preuve et l'automatisation des techniques de protection elles-même, car l'écriture manuelle de code est sujette à de nombreuses erreurs, particulièrement lorsqu'il s'agit de code de sécurité
Implementations of cryptosystems are vulnerable to physical attacks, and thus need to be protected against them. Of course, malfunctioning protections are useless. Formal methods help to develop systems while assessing their conformity to a rigorous specification. The first goal of my thesis, and its innovative aspect, is to show that formal methods can be used to prove not only the principle of the countermeasures according to a model, but also their implementations, as it is where the physical vulnerabilities are exploited. My second goal is the proof and the automation of the protection techniques themselves, because handwritten security code is error-prone

APA, Harvard, Vancouver, ISO, and other styles

2

Bursuc, Sergiu. "Contraintes de déductibilité dans une algèbre quotient : réduction de modèles et applications à la sécurité." Cachan, Ecole normale supérieure, 2009. http://www.theses.fr/2009DENS0055.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

3

Masson, Lola. "Safety monitoring for autonomous systems : interactive elicitation of safety rules." Thesis, Toulouse 3, 2019. http://www.theses.fr/2019TOU30220.

Full text

Abstract:

Un moniteur de sécurité actif est un mécanisme indépendant qui est responsable de maintenir le système dans un état sûr, en cas de situation dangereuse. Il dispose d'observations (capteurs) et d'interventions (actionneurs). Des règles de sécurité sont synthétisées, à partir des résultats d'une analyse de risques, grâce à l'outil SMOF (Safety MOnitoring Framework), afin d'identifier quelles interventions appliquer quand une observation atteint une valeur dangereuse. Les règles de sécurité respectent une propriété de sécurité (le système reste das un état sûr) ainsi que des propriétés de permissivité, qui assurent que le système peut toujours effectuer ses tâches. Ce travail se concentre sur la résolution de cas où la synthèse échoue à retourner un ensemble de règles sûres et permissives. Pour assister l'utilisateur dans ces cas, trois nouvelles fonctionnalités sont introduites et développées. La première adresse le diagnostique des raisons pour lesquelles une règle échoue à respecter les exigences de permissivité. La deuxième suggère des interventions de sécurité candidates à injecter dans le processus de synthèse. La troisième permet l'adaptation des exigences de permissivités à un ensemble de tâches essentielles à préserver. L'utilisation des ces trois fonctionnalités est discutée et illustrée sur deux cas d'étude industriels, un robot industriel de KUKA et un robot de maintenance de Sterela
An active safety monitor is an independent mechanism that is responsible for keeping the system in a safe state, should a hazardous situation occur. Is has observations (sensors) and interventions (actuators). Safety rules are synthesized from the results of the hazard analysis, using the tool SMOF (Safety MOnitoring Framework), in order to identify which interventions to apply for dangerous observations values. The safety rules enforce a safety property (the system remains in a safe state) and some permissiveness properties, ensuring that the system can still perform its tasks. This work focuses on solving cases where the synthesis fails to return a set of safe and permissive rules. To assist the user in these cases, three new features are introduced and developed. The first one addresses the diagnosis of why the rules fail to fulfill a permissiveness requirement. The second one suggests candidate safety interventions to inject into the synthesis process. The third one allows the tuning of the permissiveness requirements based on a set of essential functionalities to maintain. The use of these features is discussed and illustrated on two industrial case studies, a manufacturing robot from KUKA and a maintenance robot from Sterela

APA, Harvard, Vancouver, ISO, and other styles

4

Konopacki, Pierre. "Modélisation de politiques de sécurité à l'aide de méthode de spécifications formelles." Phd thesis, Université Paris-Est, 2012. http://tel.archives-ouvertes.fr/tel-00786926.

Full text

Abstract:

Le contrôle d'accès permet de spécifier une partie de la politique de sécurité d'un SI (système d'informations). Une politique de CA (Contrôle d'accès) permet de définir qui a accès à quoi et sous quelles conditions. Les concepts fondamentaux utilisés en CA sont : les permissions, les interdictions (ou prohibitions), les obligations et la SoD (séparation des devoirs). Les permissions permettent d'autoriser une personne à accéder à des ressources. Au contraire les prohibitions interdisent à une personne d'accéder à certaines ressources. Les obligations lient plusieurs actions. Elles permettent d'exprimer le fait qu'une action doit être réalisée en réponse à une première action. La SoD permet de sécuriser une procédure en confiant la réalisation des actions composant cette procédure à des agents différents. Différentes méthodes de modélisation de politiques de contrôle d'accès existent. L'originalité de la méthode EB3Sec issue de nos travaux repose sur deux points :- permettre d'exprimer tous les types de contraintes utilisées en CA dans un même modèle,- proposer une approche de modélisation basée sur les événements. En effet, aucune des méthodes actuelles ne présente ces deux caractéristiques, au contraire de la méthode EB3Sec. Nous avons défini un ensemble de patrons, chacun des patrons correspond à un type de contraintes de CA. Un modèle réalisé à l'aide de la méthode EB3Sec peut avoir différentes utilisations :- vérification et simulation,- implémentation. La vérification consiste à s'assurer que le modèle satisfait bien certaines propriétés, dont nous avons défini différents types. Principalement, les blocages doivent être détectés. Ils correspondent à des situations où une action n'est plus exécutable ou à des situations où plus aucune action n'est exécutable. Les méthodes actuelles des techniques de preuves par vérification de modèles ne permettent pas de vérifier les règles dynamiques de CA. Elles sont alors combinées à des méthodes de simulation. Une fois qu'un modèle a été vérifié, il peut être utilisé pour implémenter un filtre ou noyau de sécurité. Deux manières différentes ont été proposées pour réaliser cette implémentation : transformer le modèle EB3Sec vers un autre langage, tel XACML, possédant une implémentation ayant déjà atteint la maturité ou réaliser un noyau de sécurité utilisant le langage EB3Sec comme langage d'entrée

APA, Harvard, Vancouver, ISO, and other styles

5

Colange, Maximilien. "Symmetry reduction and symbolic data structures for model-checking of distributed systems." Paris 6, 2013. http://www.theses.fr/2013PA066724.

Full text

Abstract:

Les systèmes répartis deviennent omniprésents au quotidien, en particulier dans des domaines critiques, requérant une forte garantie de fiabilité. Les approches basées sur le test sont intrinsèquement non-exhaustives, rendant nécessaire l’usage de méthodes formelles. Parmi elles, nous nous concentrons sur le model-checking, qui explore tous les comportements d’un système pour s’assurer que sa spécification est respectée. Mais cette approche se heurte à l’explosion combinatoire : le nombre d’états d’un système réparticroît exponentiellement avec son nombre de composants. Nous retenons deux des nombreuses solutions à ce problème :- les symétries pour identifier des comportements similaires : ils partagent des propriétés communes, ce qui réduit le nombre d’états à explorer. - des structures de données compactes, comme les diagrammes de décision (DD), pour réduire l’empreinte mémoire de l’exploration. Nous proposons trois principales contributions :- La réduction par symétries et les DD sont théoriquement orthogonaux, mais se combinent mal en pratique, car l’efficacité des DD repose sur l’emploi d’algorithmes dédiés. Nous proposons un nouvel algorithme pour appliquer la réduction par symétries sur des DD, et démontrons son efficacité pratique. - Classiquement, les opérations sur les DD sont encodées après un pré-calcul de toutes les entrées possibles. Nous offrons un nouveau mécanisme de manipulation des DD, entièrement symbolique, qui évite un tel pré-calcul. Nous démontrons son efficacité pour encoder une relation de transition. - Nous montrons comment ces deux contributions peuvent être appliquées à un formalisme déjà existant, les Symmetric Nets with Bags
Distributed systems are becoming omnipresent in our daily life, especially in critical domains, thus requiring a strong guarantee of reliability. Approaches like testing are inherently not exhaustive, so that formal methods are needed. Among those, we focus on model-checking, that consists in exploring exhaustively all the behaviors of a system to ensure that the specification is enforced. However, this approach faces the “combinatorial explosion” problem: the number behaviors of a distributed system increases exponentially with its number of components. To tackle this explosion, several approaches have been proposed. We focus on two of them:- symmetries to identify similar behaviors: they share similar properties, thus allowing to reduce the number of behaviors to explore;- symbolic compact data structures, namely decision diagrams (DD), to reduce the memory footprint of the explored behaviors. We propose three main contributions:- Symmetry reduction and DD are theoretically orthogonal techniques, but are not known to combine well in practice, because efficiency of DD heavily relies on the use of dedicated algorithms. We propose a novel algorithm to use symmetry reduction on DD, and demonstrate experimentally its efficiency. - Classical operations on DD are encoded using a pre-computation of all possible inputs. We offer a new mechanism of manipulation of DD, fully symbolic, that avoids such a pre-computation. We demonstrate its efficiency to encode a transition relation, and to improve our symmetry reduction algorithm- We show how to use the two previous contributions to model-check an existing class of models, the Symmetric Nets with Bags

APA, Harvard, Vancouver, ISO, and other styles

6

El, Jamal Mohamad Hani. "Contribution à l'évolution des exigences et son impact sur la sécurité." Phd thesis, Université Paul Sabatier - Toulouse III, 2006. http://tel.archives-ouvertes.fr/tel-00139543.

Full text

Abstract:

Le travail de la thèse porte sur la problématique de l'évolution des exigences et son analyse d'impact sur la sécurité. Au cours du développement des systèmes, les parties prenantes demandent l'application des évolutions, afin d'améliorer leurs fonctionnalités. L'occurrence d'une évolution affecte plusieurs aspects comme: la sécurité, le coût du développement et les délais. Lorsque le développement concerne un système complexe où le nombre des exigences est de l'ordre de dizaines de milliers, alors les demandes des évolutions rendent l'analyse d'impact du changement de plus en plus difficile. Malheureusement, la problématique de l'évolution des exigences n'est pas encore complètement résolue en milieu industriel. Notre étude est située dans le contexte d'ingénierie système et ingénierie des exigences, en intégrant des modèles formels et outils supports associés pour la vérification des propriétés de sécurité. La méthodologie est basée sur la norme industrielle de l'EIA-632 et sur le format VOLERE d'ingénierie des exigences en intégrant un modèle de traçabilité. De cette démarche ingénierie système, on a développé une méthodologie associée et un système d'information du processus de changement/évolution des exigences. Enfin, ce travail présente la méthodologie de la recherche d'impact lors de la demande de changement, et les outils qui supportent la méthodologie de la recherche d'impact, en se basant sur la méthode formelle (RAISE), qui nous permet d'analyser l'impact de l'évolution sur la sécurité.

APA, Harvard, Vancouver, ISO, and other styles

7

Guesmi, Asma. "Spécification et analyse formelles des politiques de sécurité dans un processus de courtage de l'informatique en nuage." Thesis, Orléans, 2016. http://www.theses.fr/2016ORLE2010/document.

Full text

Abstract:

Les offres de l’informatique en nuage augmentent de plus en plus et les clients ne sont pas capables de lescomparer afin de choisir la plus adaptée à leurs besoins. De plus, les garanties de sécurité proposées parles fournisseurs restent incompréhensibles pour les clients. Cela représente un frein pour l'adoption dessolutions de l’informatique en nuage.Dans cette thèse, nous proposons un mécanisme de courtage des services de l’informatique en nuage quiprend en compte les besoins du client en termes de sécurité.Les besoins exprimés par le client sont de deux natures. Les besoins fonctionnels représentent lesressources et leurs performances. Les besoins non-fonctionnels représentent les propriétés de sécurité etles contraintes de placement des ressources dans le nuage informatique. Nous utilisons le langage Alloypour décrire les offres et les besoins. Nous utilisons l'analyseur Alloy pour l'analyse et la vérification desspécifications du client. Le courtier sélectionne les fournisseurs qui satisfont les besoins fonctionnels et nonfonctionnelsdu client. Il vérifie ensuite, que la configuration du placement des ressources chez lesfournisseurs respecte toutes les propriétés de sécurité exigées par le client.Toutes ces démarches sont effectuées avant le déploiement des ressources dans le nuage informatique.Cela permet de détecter les erreurs et conflits des besoins du client tôt. Ainsi, on réduit les vulnérabilités desressources du client une fois déployées
The number of cloud offerings increases rapidly. Therefore, it is difficult for clients to select the adequate cloud providers which fit their needs. In this thesis, we introduce a cloud service brokerage mechanism that considers the client security requirements. We consider two types of the client requirements. The amount of resources is represented by the functional requirements. The non-functional requirements consist on security properties and placement constraints. The requirements and the offers are specified using the Alloy language. To eliminate inner conflicts within customers requirements, and to match the cloud providers offers with these customers requirements, we use a formal analysis tool: Alloy. The broker uses a matching algorithm to place the required resources in the adequate cloud providers, in a way that fulfills all customer requirements, including security properties. The broker checks that the placement configuration ensures all the security requirements. All these steps are done before the resources deployment in the cloud computing. This allows to detect the conflicts and errors in the clients requirements, thus resources vulnerabilities can be avoided after the deployment

APA, Harvard, Vancouver, ISO, and other styles

8

Robin, Ludovic. "Vérification formelle de protocoles basés sur de courtes chaines authentifiées." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0019/document.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

9

Filipiak, Alicia. "Conception et analyse formelle de protocoles de sécurité, une application au vote électronique et au paiement mobile." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0039/document.

Full text

Abstract:

Les “smart-devices” tels les smartphones, tablettes et même les montres ont été largement démocratisés au cours de la dernière décennie. Dans nos sociétés occidentales, on ne garde plus seulement son ordinateur personnel chez soi, on le transporte dans la poche arrière de son pantalon ou bien autour de son poignet. Ces outils ne sont d’ailleurs plus limités, en termes d’utilisation, à de la simple communication par SMS ou bien téléphone, on se fie à eux pour stocker nos photos et données personnelles, ces dernières parfois aussi critiques que des données de paiement bancaires, on gère nos contacts et finances, se connecte à notre boite mail ou un site marchand depuis eux. . . Des exemples récents nous fournissent d’ailleurs un aperçu des tâches de plus en plus complexes que l’on confie à ces outils : l’Estonie autorise l’utilisation de smartphones pour participer aux scrutins nationaux et en 2017, la société Transport for London a lancé sa propre application autorisant l’émulation d’une Oyster card et son rechargement pour emprunter son réseau de transports publics. Plus les services se complexifient, plus la confiance qui leur est accordée par les groupes industriels et les utilisateurs grandit. Nous nous intéressons ici aux protocoles cryptographiques qui définissent les échanges entre les outils et entités qui interviennent dans l’utilisation de tels services et aux garanties qu’ils proposent en termes de sécurité (authentification mutuelle des agent, intégrité des messages circulant, secret d’une valeur critique…). Moult exemples de la littérature et de la vie courante ont démontré que leur élaboration était hautement vulnérable à des erreurs de design. Heureusement, des années de recherches nous ont fournis des outils pour rendre cette tâche plus fiable, les méthodes formelles font partie de ceux-là. Il est possible de modeler un protocole cryptographique comme un processus abstrait qui manipule des données et primitives cryptographiques elles aussi modélisées comme des termes et fonctions abstraites. On met le protocole à l’épreuve face à un attaquant actif et on peut spécifier mathématiquement les propriétés de sécurité qu’il est censé garantir. Ces preuves de sécurité peuvent être automatisées grâce à des outils tels que ProVerif ou bien Tamarin. L’une des grandes difficultés lorsque l’on cherche à concevoir et prouver formellement la sécurité d’un protocole de niveau industriel réside dans le fait que ce genre de protocole est généralement très long et doit satisfaire des propriétés de sécurité plus complexes que certains protocoles universitaires. Au cours de cette thèse, nous avons souhaité étudier deux cas d’usage : le vote électronique et le paiement mobile. Dans les deux cas, nous avons conçu et prouvé la sécurité d’un protocole répondant aux problématiques spécifiques à chacun des cas d’usage. Dans le cadre du vote électronique, nous proposons le protocole Belenios VS, une variante de Belenios RF. Nous définissons l’écosystème dans lequel le protocole est exécuté et prouvons sa sécurité grâce à ProVerif. Belenios VS garantit la confidentialité du vote et le fait qu’un utilisateur puisse vérifier que son vote a bien fait parti du résultat final de l’élection, tout cela même si l’outil utilisé par le votant est sous le contrôle d’un attaquant. Dans le cadre du paiement, nous avons proposé la première spécification ouverte de bout en bout d’une application de paiement mobile. Sa conception a pris en compte le fait qu’elle devait pouvoir s’adapter à l’écosystème de paiement déjà existant pour être largement déployable et que les coûts de gestion, de développement et de maintenance de la sécurité devait être optimisés
The last decade has seen the massive democratization of smart devices such as phones, tablets, even watches. In the wealthiest societies of the world, not only do people have their personal computer at home, they now carry one in their pocket or around their wrist on a day to day basis. And those devices are no more used simply for communication through messaging or phone calls, they are now used to store personal photos or critical payment data, manage contacts and finances, connect to an e-mail box or a merchant website... Recent examples call for more complex tasks we ask to such devices: Estonia voting policy allows the use of smart ID cards and smartphones to participate to national elections. In 2017, Transport for London launched the TfL Oyster app to allow tube users to top up and manage their Oyster card from their smartphone. As services grow with more complexity, so do the trust users and businesses put in them. We focus our interest into cryptographic protocols which define the exchanges between devices and entities so that such interaction ensure some security guarantees such as authentication, integrity of messages, secrecy… Their design is known to be an error prone task. Thankfully, years of research gave us some tools to improve the design of security protocols, among them are the formal methods: we can model a cryptographic protocol as an abstract process that manipulates data and cryptographic function, also modeled as abstract terms and functions. The protocol is tested against an active adversary and the guarantees we would like a protocol to satisfy are modeled as security properties. The security of the protocol can then be mathematically proven. Such proofs can be automated with tools like ProVerif or Tamarin. One of the big challenge when it comes to designing and formally proving the security an “industrial- level” protocol lies in the fact that such protocols are usually heavier than academic protocols and that they aim at more complex security properties than the classical ones. With this thesis, we wanted to focus on two use cases: electronic voting and mobile payment. We designed two protocols, one for each respective use case and proved their security using automated prover tools. The first one, Belenios VS, is a variant of an existing voting scheme, Belenios RF. It specifies a voting ecosystem allowing a user to cast a ballot from a voting sheet by flashing a code. The protocol’s security has been proven using the ProVerif tool. It guarantees that the vote confidentiality cannot be broken and that the user is capable of verifying their vote is part of the final result by performing a simple task that requires no technical skills all of this even if the user’s device is compromised – by a malware for instance. The second protocol is a payment one that has been conceived in order to be fully scalable with the existing payment ecosystem while improving the security management and cost on the smartphone. Its security has been proven using the Tamarin prover and holds even if the user’s device is under an attacker’s control

APA, Harvard, Vancouver, ISO, and other styles

10

Jacomme, Charlie. "Preuves de protocoles cryptographiques : méthodes symboliques et attaquants puissants." Electronic Thesis or Diss., université Paris-Saclay, 2020. http://www.theses.fr/2020UPASG005.

Full text

Abstract:

L'utilisation des protocoles de communication est omniprésente dans notre société, mais leur utilisation comporte des risques de sécurité ou d'atteinte à la vie privée. Pour réduire ces risques, il faut exiger de solides garanties, i.e. des preuves formelles, approfondies, modulaires et vérifiées par ordinateur. Toutefois, de telles preuves sont très difficiles à obtenir. Nous essayons dans cette thèse de faciliter ce processus dans le cas des protocoles cryptographiques et d'attaquants puissants. Nos contributions principales sont 1) une méthodologie d'analyse approfondies dans le cas de l'authentification multi-facteurs; 2) des résultats de composition permettant des preuves modulaires de protocoles complexes dans le modèle calculatoire; 3) l'automatisation d'étapes élémentaires de preuves calculatoires via des méthodes symboliques appliquées à des programmes probabilistes; 4) un prototype d'assistant de preuve dans le modèle de l'attaquant symbolique calculatoirement complet
The use of communication protocols has become pervasive at all levels of our society. Yet, their uses come with risks, either about the security of the system or the privacy of the user. To mitigate those risks, we must provide the protocols with strong security guarantees: we need formal, extensive, modular and machine-checked proofs. However, such proofs are very difficult to obtain in practice. In this Thesis, we strive to ease this process in the case of cryptographic protocols and powerful attackers. The four main contributions of this Thesis, all based on symbolic methods, are 1) a methodology for extensive analyses via a case study of multi-factor authentication; 2) composition results to allow modular proofs of complex protocols in the computational model; 3) symbolic methods for deciding basic proof steps in computational proofs, formulated as problems on probabilistic programs; 4) a prototype of a mechanized prover in the Computationally Complete Symbolic Attacker model

APA, Harvard, Vancouver, ISO, and other styles

11

De, Almeida Pereira Dalay Israel. "Analyse et spécification formelle des systèmes d’enclenchement ferroviaire basés sur les relais." Thesis, Centrale Lille Institut, 2020. http://www.theses.fr/2020CLIL0009.

Full text

Abstract:

Les Systèmes d'Enclenchement Ferroviaire (SEF) basés sur des relais sont des systèmes critiques, ils doivent être spécifiés et leur sécurité doit être prouvée afin de garantir l'absence de dangers lors de leurs exécutions. Toutefois, il s'agit d'une tâche difficile, car les SEF à relais ne sont généralement modélisés que de manière structurelle, de sorte que leur analyse comportementale est effectuée manuellement sur la base des connaissances des experts sur le système. Cependant, l'existence d'une description formelle du comportement des SEF est impérative pour pouvoir effectuer des preuves de sécurité. En outre, comme les SEF informatisés ont tendance à être moins chers, plus faciles à entretenir et à faire évoluer, le secteur ferroviaire a intérêt à ce qu'il existe une méthodologie pour transformer des SEF à relais existants en SEF informatisés.Les méthodologies formelles de spécification sont fondées sur des bases mathématiques solides qui permettent de prouver la sécurité des systèmes. En outre, de nombreux langages de spécification formelle prennent en charge non seulement la vérification, mais aussi la mise en œuvre de ces systèmes par un processus de développement formalisé. Ainsi, les méthodes formelles peuvent être la clé pour prouver la sécurité des SEF et les mettre en œuvre en utilisant des technologies informatiques.Cette thèse aborde deux propositions principales. Premièrement, elle présente une analyse des informations des diagrammes à relais et de la formalisation de la structure et du comportement des SEF basés sur des expressions mathématiques afin de créer un certain niveau de formalisation des systèmes. Le modèle résultant peut être étendu et adapté afin de se conformer à différents contextes ferroviaires et il peut aussi être utilisé afin de soutenir la spécification de ces systèmes dans différents langages de spécification formels. Ensuite, cette thèse présente comment le modèle formel des SEF peut être adapté afin de spécifier formellement ces systèmes selon la méthode B, un langage de spécification formel qui a déjà été utilisé avec succès dans le domaine ferroviaire et qui permet de prouver la sécurité du système et de le mettre en œuvre en tant que système informatique.En définitive, cette thèse présente une méthodologie complète pour la spécification et la vérification des Systèmes d'Enclenchement Ferroviaire basés sur des relais, en fournissant un support pour la preuve des systèmes dans différents contextes et pour leur spécification et leur mise en œuvre dans de nombreux langages formels différents
Relay-based Railway Interlocking Systems (RIS) are critical systems and must be specified and safety proved in order to guarantee the absence of hazards during their execution. However, this is a challenging task, since Relay-based RIS are generally only structurally modelled in a way that their behavioural analysis are made manually based on the experts knowledge about the system. Thus, the existence of a RIS behavioural formal description is imperative in order to be able to perform safety proofs. Furthermore, as Computer-based RIS tend to be less expensive, more maintainable and extendable, the industry has interest in the existence of a methodology for transforming the existing Relay-based RIS into Computer-based RIS.Formal specification methodologies are grounded in strong mathematical foundations that allow the systems safety proof. Besides, many formal specification languages support not only the verification, but also the implementation of these systems through a formal development process. Thus, Formal Methods may be the key in order to prove the RIS safety and implement them with computer-based technologies.This thesis addresses two main propositions. Firstly, it presents an analysis of the relay diagrams information and a formalisation of the Relay-based RIS structure and behaviour based on mathematical expressions as a way to create a certain level of formalisation of the systems. The resulting model can be extended and adapted in order to conform to different railway contexts and it can be used in order to support the specification of these systems in different formal specification languages. Then, this thesis presents how the RIS formal model can be adapted in order to formally specify these systems in B-method, a formal specification language with a successful history in the railway field and which allows the system safety proof and implementation as computer-based systems.As a result, this thesis presents a complete methodology for the specification and verification of Relay-based Railway Interlocking Systems, giving support for the systems safety proof in different contexts and for their specification and implementation in many different formal languages

APA, Harvard, Vancouver, ISO, and other styles

12

De, Almeida Pereira Dalay Israel. "Analyse et spécification formelle des systèmes d’enclenchement ferroviaire basés sur les relais." Thesis, Ecole centrale de Lille, 2020. http://www.theses.fr/2020ECLI0009.

Full text

Abstract:

Les Systèmes d'Enclenchement Ferroviaire (SEF) basés sur des relais sont des systèmes critiques, ils doivent être spécifiés et leur sécurité doit être prouvée afin de garantir l'absence de dangers lors de leurs exécutions. Toutefois, il s'agit d'une tâche difficile, car les SEF à relais ne sont généralement modélisés que de manière structurelle, de sorte que leur analyse comportementale est effectuée manuellement sur la base des connaissances des experts sur le système. Cependant, l'existence d'une description formelle du comportement des SEF est impérative pour pouvoir effectuer des preuves de sécurité. En outre, comme les SEF informatisés ont tendance à être moins chers, plus faciles à entretenir et à faire évoluer, le secteur ferroviaire a intérêt à ce qu'il existe une méthodologie pour transformer des SEF à relais existants en SEF informatisés.Les méthodologies formelles de spécification sont fondées sur des bases mathématiques solides qui permettent de prouver la sécurité des systèmes. En outre, de nombreux langages de spécification formelle prennent en charge non seulement la vérification, mais aussi la mise en œuvre de ces systèmes par un processus de développement formalisé. Ainsi, les méthodes formelles peuvent être la clé pour prouver la sécurité des SEF et les mettre en œuvre en utilisant des technologies informatiques.Cette thèse aborde deux propositions principales. Premièrement, elle présente une analyse des informations des diagrammes à relais et de la formalisation de la structure et du comportement des SEF basés sur des expressions mathématiques afin de créer un certain niveau de formalisation des systèmes. Le modèle résultant peut être étendu et adapté afin de se conformer à différents contextes ferroviaires et il peut aussi être utilisé afin de soutenir la spécification de ces systèmes dans différents langages de spécification formels. Ensuite, cette thèse présente comment le modèle formel des SEF peut être adapté afin de spécifier formellement ces systèmes selon la méthode B, un langage de spécification formel qui a déjà été utilisé avec succès dans le domaine ferroviaire et qui permet de prouver la sécurité du système et de le mettre en œuvre en tant que système informatique.En définitive, cette thèse présente une méthodologie complète pour la spécification et la vérification des Systèmes d'Enclenchement Ferroviaire basés sur des relais, en fournissant un support pour la preuve des systèmes dans différents contextes et pour leur spécification et leur mise en œuvre dans de nombreux langages formels différents
Relay-based Railway Interlocking Systems (RIS) are critical systems and must be specified and safety proved in order to guarantee the absence of hazards during their execution. However, this is a challenging task, since Relay-based RIS are generally only structurally modelled in a way that their behavioural analysis are made manually based on the experts knowledge about the system. Thus, the existence of a RIS behavioural formal description is imperative in order to be able to perform safety proofs. Furthermore, as Computer-based RIS tend to be less expensive, more maintainable and extendable, the industry has interest in the existence of a methodology for transforming the existing Relay-based RIS into Computer-based RIS.Formal specification methodologies are grounded in strong mathematical foundations that allow the systems safety proof. Besides, many formal specification languages support not only the verification, but also the implementation of these systems through a formal development process. Thus, Formal Methods may be the key in order to prove the RIS safety and implement them with computer-based technologies.This thesis addresses two main propositions. Firstly, it presents an analysis of the relay diagrams information and a formalisation of the Relay-based RIS structure and behaviour based on mathematical expressions as a way to create a certain level of formalisation of the systems. The resulting model can be extended and adapted in order to conform to different railway contexts and it can be used in order to support the specification of these systems in different formal specification languages. Then, this thesis presents how the RIS formal model can be adapted in order to formally specify these systems in B-method, a formal specification language with a successful history in the railway field and which allows the system safety proof and implementation as computer-based systems.As a result, this thesis presents a complete methodology for the specification and verification of Relay-based Railway Interlocking Systems, giving support for the systems safety proof in different contexts and for their specification and implementation in many different formal languages

APA, Harvard, Vancouver, ISO, and other styles

13

Bourdier, Tony. "Méthodes algébriques pour la formalisation et l'analyse de politiques de sécurité." Phd thesis, Université Henri Poincaré - Nancy I, 2011. http://tel.archives-ouvertes.fr/tel-00646401.

Full text

Abstract:

Concevoir et mettre en œuvre des méthodes pour la spécification, l'analyse et la vérification de logiciels et de systèmes sont les principaux moteurs des activités de recherche présentées dans ce manuscrit. Dans ce cadre, nos travaux se positionnent dans la catégorie dite des méthodes formelles appartenant à la communauté plus large du génie logiciel. A l'interface des travaux théoriques et applicatifs, notre objectif est de contribuer aux méthodes permettant d'assurer la correction et la sûreté des systèmes (fonctionnalité, sécurité, fiabilité, ...) en développant ou en améliorant des langages de spécification, des techniques et des outils permettant leur analyse formelle. Dans ce but, nous nous sommes attaché dans cette thèse à proposer et à étudier un cadre formel permettant la définition de politiques de sécurité et la vérification de leurs propriétés. A cet effet, nous avons proposé un cadre pour la spécification de politiques de sécurité basé sur une approche modulaire dans laquelle une politique est vue comme la composition d'un modèle de sécurité et d'une configuration. Nous avons investigué les possibilités offertes par de telles spécifications lorsque les modèles sont exprimés au moyen de contraintes du premier ordre et les configurations au moyen de programmes logiques. En particulier, nous avons proposé un algorithme permettant de transformer une politique exprimée dans un modèle donné vers une autre politique équivalente (au sens où elle engendre les mêmes autorisations) exprimée dans un autre modèle. Dans un second temps, nous nous sommes proposé de tenir compte des aspects dynamiques de la configuration d'une politique vue comme un état du système sur lequel la politique est mise en œuvre et où chaque action est associée à une procédure de modification des états. Nous avons proposé un langage formel simple pour spécifier séparément les systèmes et les politiques de sécurité puis avons donné une sémantique des spécifications exprimées dans ce cadre sous la forme de systèmes de réécriture. Nous nous sommes ensuite attachés à montrer que les systèmes de réécriture obtenus permettent l'étude de propriétés de sécurité. Dans une troisième partie, nous nous sommes focalisé sur les mécanismes permettant la mise en œuvre de politiques de sécurité dans les réseaux. Dans ce cadre, nous avons proposé une spécification des firewalls et de leurs compositions basée sur les automates d'arbres et les systèmes de réécriture puis avons montré en quoi ces spécifications nous permettent d'analyser de façon automatique les politiques de sécurité sous-jacentes.

APA, Harvard, Vancouver, ISO, and other styles

14

Morisset, Charles. "Sémantique des systèmes de contrôle d'accès : définition d'un cadre sémantique pour la spécification, l'implantation et la comparaison de modèles de contrôle d'accès." Paris 6, 2007. http://www.theses.fr/2007PA066244.

Full text

Abstract:

Un des aspects de la sécurité en informatique concerne le contrôle des accès aux données d'un systèm. Nous utilisons les méthodes formelles pour aborder le contrôle d'accès avec pour objectif à long terme le développement d'une bibliothèque certifiée de politiques de sécurité. Tout d'abord, il s'agit de formaliser les politiques considérées afin d'identifier les hypothèses implicites et d'expliciter le système à modéliser. Ensuite, il s'agit de mécaniser cette formalisation. Nous présentons un exemple d'implantation d'un modèle de contrôle d'accès au sein de l'atelier Focal, nous permettant de concevoir un moniteur de référence appliquant la politique de Bell et LaPadula au sein d'un SGBD. Enfin, pour permettre une réutilisation plus facile des développements formels obtenus, nous introduisons un cadre sémantique abstrait permettant de spécifier, d'implanter et de comparer des modèles de contrôle d'accès. Ce cadre caractérise des propriétés de simulation entre implantations permettant d'exprimer qu'un modèle est plus restrictif qu'un autre

APA, Harvard, Vancouver, ISO, and other styles

15

Chaudemar, Jean-Charles. "Étude des architectures de sécurité de systèmes autonomes : formalisation et évaluation en Event B." Thesis, Toulouse, ISAE, 2012. http://www.theses.fr/2012ESAE0003/document.

Full text

Abstract:

La recherche de la sûreté de fonctionnement des systèmes complexes impose une démarche de conception rigoureuse. Les travaux de cette thèse s’inscrivent dans le cadre la modélisation formelle des systèmes de contrôle autonomes tolérants aux fautes. Le premier objectif a été de proposer une formalisation d’une architecture générique en couches fonctionnelles qui couvre toutes les activités essentielles du système de contrôle et qui intègre des mécanismes de sécurité. Le second objectif a été de fournir une méthode et des outils pour évaluer qualitativement les exigences de sécurité. Le cadre formel de modélisation et d’évaluation repose sur le formalisme Event-B. La modélisation Event-B proposée tire son originalité d’une prise en compte par raffinements successifs des échanges et des relations entre les couches de l’architecture étudiée. Par ailleurs, les exigences de sécurité sont spécifiées à l’aide d’invariants et de théorèmes. Le respect de ces exigences dépend de propriétés intrinsèques au système décrites sous forme d’axiomes. Les preuves que le principe d’architecture proposé satisfait bien les exigences de sécurité attendue ont été réalisées avec les outils de preuve de la plateforme Rodin. L’ensemble des propriétés fonctionnelles et des propriétés relatives aux mécanismes de tolérance aux fautes, ainsi modélisées en Event-B, renforce la pertinence de la modélisation adoptée pour une analyse de sécurité. Cette approche est par la suite mise en œuvre sur un cas d’étude d’un drone ONERA
The study of complex system safety requires a rigorous design process. The context of this work is the formal modeling of fault tolerant autonomous control systems. The first objective has been to provide a formal specification of a generic layered architecture that covers all the main activities of control system and implement safety mechanisms. The second objective has been to provide tools and a method to qualitatively assess safety requirements. The formal framework of modeling and assessment relies on Event-B formalism. The proposed Event-B modeling is original because it takes into account exchanges and relations betweenarchitecture layers by means of refinement. Safety requirements are first specified with invariants and theorems. The meeting of these requirements depends on intrinsic properties described with axioms. The proofs that the concept of the proposed architecture meets the specified safety requirements were discharged with the proof tools of the Rodin platform. All the functional properties and the properties relating to fault tolerant mechanisms improve the relevance of the adopted Event-B modeling for safety analysis. Then, this approach isimplemented on a study case of ONERA UAV

APA, Harvard, Vancouver, ISO, and other styles

16

Xie, Yuchen. "Modélisation et Vérification Formelles de Systèmes de Contrôle de Trains." Thesis, Ecole centrale de Lille, 2019. http://www.theses.fr/2019ECLI0001.

Full text

Abstract:

Le degré d'automatisation des systèmes de contrôle ferroviaire est en constante augmentation. Les industriels ferroviaires ont besoin d'un niveau accru de sécurité et de fiabilité pour remplacer les conducteurs par des systèmes de contrôle automatique des trains (ATC). Cependant, la complexité du système est également fortement augmentée par l'intégration des fonctions automatiques, ce qui rend difficile l'analyse de ces systèmes.Différentes méthodes de modélisation peuvent être utilisées pour construire les modèles du système au niveau d'abstraction approprié. Les méthodes de modélisation formelles et les méthodes de vérification formelles fournissent un cadre crucial pour assurer les propriétés de sécurité et de fiabilité. Les Réseaux de Petri constituent un outil formel approprié à la modélisation et à la vérification de systèmes critiques comme les systèmes de contrôle automatique du ferroviaire. Dans cette thèse, nous utilisons plus particulièrement les réseaux de Pétri colorés (CPNs) de Jensen pour exploiter la modularité et la hiérarchisation pour la modélisation et la vérification d’un système de grande taille
The automation degree of railway control systems is constantly increasing. Railway industry needs the enhanced level of safety and reliability guarantee to replace the drivers by Automatic Train Control (ATC) systems. However, the system complexity is also heavily increased by the integration of automatic functions, which has caused the difficulty to analyze these systems.Different modeling methods can be used to build the system models at the appropriate level of abstraction. Formal modeling methods and formal verification methods can provide crucial support to ensure safety and reliability properties. Petri Nets are a suitable tool for modeling and verifying critical systems such as automatic train control systems. In this thesis, we use more specifically Colored Petri Nets (CPNs) to exploit modularity and hierarchization for the modeling and verification of a large-scale system

APA, Harvard, Vancouver, ISO, and other styles

17

Schnepf, Nicolas. "Orchestration et vérification de fonctions de sécurité pour des environnements intelligents." Thesis, Université de Lorraine, 2019. http://www.theses.fr/2019LORR0088/document.

Full text

Abstract:

Les équipements intelligents, notamment les smartphones, sont la cible de nombreuses attaques de sécurité. Par ailleurs, la mise en œuvre de mécanismes de protection usuels est souvent inadaptée du fait de leurs ressources fortement contraintes. Dans ce contexte, nous proposons d'utiliser des chaînes de fonctions de sécurité qui sont composées de plusieurs services de sécurité, tels que des pare-feux ou des antivirus, automatiquement configurés et déployés dans le réseau. Cependant, ces chaînes sont connues pour être difficiles à valider. Cette difficulté est causée par la complexité de ces compositions qui impliquent des centaines, voire des milliers de règles de configuration. Dans cette thèse, nous proposons l'architecture d'un orchestrateur exploitant la programmabilité des réseaux pour automatiser la configuration et le déploiement de chaînes de fonctions de sécurité. Il est important que ces chaînes de sécurité soient correctes afin d’éviter l'introduction de failles de sécurité dans le réseau. Aussi, notre orchestrateur repose sur des méthodes automatiques de vérification et de synthèse, encore appelées méthodes formelles, pour assurer la correction des chaînes. Notre travail appréhende également l'optimisation du déploiement des chaînes dans le réseau, afin de préserver ses ressources et sa qualité de service
Smart environments, in particular smartphones, are the target of multiple security attacks. Moreover, the deployment of traditional security mechanisms is often inadequate due to their highly constrained resources. In that context, we propose to use chains of security functions which are composed of several security services, such as firewalls or antivirus, automatically configured and deployed in the network. Chains of security functions are known as being error prone and hard to validate. This difficulty is caused by the complexity of these constructs that involve hundreds and even thousands of configuration rules. In this PhD thesis, we propose the architecture of an orchestrator, exploiting the programmability brought by software defined networking, for the automated configuration and deployment of chains of security functions. It is important to automatically insure that these security chains are correct, before their deployment in order to avoid the introduction of security breaches in the network. To do so, our orchestrator relies on methods of automated verification and synthesis, also known as formal methods, to ensure the correctness of the chains. Our work also consider the optimization of the deployment of chains of security functions in the network, in order to maintain its resources and quality of service

APA, Harvard, Vancouver, ISO, and other styles

18

Defossez, François. "Modélisation discrète et formelle des exigences temporelles pour la validation et l’évaluation de la sécurité ferroviaire." Thesis, Ecole centrale de Lille, 2010. http://www.theses.fr/2010ECLI0004/document.

Full text

Abstract:

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit
The introduction of new European standards for railway safety, coupled with an increasing use of software technology changes the method of development of critical railway systems. Indeed, new systems have to be at least as good as the previous ones. Therefore the appropriate safety level of critical systems has to be proved in order to obtain the necessary approval from the authorities. Accordingly a high level of reliability and correctness must be reached by the use of mathematical proofs and then formal methods. We focus on the treatment of the temporal requirements in the level crossing case study which is modelled with p-time Petri nets, and on the translation of this model in a more formal way by using the B method. This paper introduces a methodology to analyse the safety of timed discrete event systems. First, our goal is to take out the forbidden state highlighted by a p-time Petri net modelling. This model deals with the requirements of the considered system and has to contain all the constraints that have to be respected. Then we aim at describing a process identified as a solution of the system functioning. This method consists in exploring all the possible behaviours of the system by means of the construction of state classes. Finally, we check if the proposed process corresponds to the requirements model previously built.Our case-study is the level crossing, a critical component for the safety of railway systems

APA, Harvard, Vancouver, ISO, and other styles

19

Sun, Tithnara Nicolas. "Modélisation et analyse formelle de modèles système pour les menaces persistantes avancées." Electronic Thesis or Diss., Brest, École nationale supérieure de techniques avancées Bretagne, 2022. http://www.theses.fr/2022ENTA0004.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

20

Farinier, Benjamin. "Procédures de décision pour l'analyse de vulnérabilités." Thesis, Université Grenoble Alpes, 2020. http://www.theses.fr/2020GRALM013.

Full text

Abstract:

Les méthodes formelles ont à plusieurs reprises montré leur pertinence dans la recherche et l'analyse de bogues. Si les méthodes actuelles sont bien adaptées à l'analyse de code critique où les erreurs ne sont pas une option, leur intérêt est moindre sur des programmes non critique. En effet, sur de tels programmes où les bugs sont pléthores, seuls les plus graves sont corrigés, une distinction qui ne sied pas avec les outils d'aujourd'hui.Le but de cette thèse est donc de permettre une telle gradation dans le contexte fort des méthodes formelles, ce qui passe par le développement de nouvelles procédures de décisions adaptées à l'analyse de vulnérabilité
Formal methods have repeatedly demonstrated their relevance in search and analysis of bugs. If current methods are well suited to critical code analysis where mistakes are not a possible option, they are less interested on non-critical programs. Indeed, on such programs bugs are too numerous and only the most serious are corrected, a practice that does not fit well with today's tools.The aim of this thesis is therefore to allow such a gradation in the context of formal methods, which involves developing new decision procedures tailored to vulnerability analysis

APA, Harvard, Vancouver, ISO, and other styles

21

Charmet, Fabien. "Security characterization of SDN virtual network migration : formal approach and resource optimization." Electronic Thesis or Diss., Institut polytechnique de Paris, 2020. http://www.theses.fr/2020IPPAS008.

Full text

Abstract:

Cette thèse explore la sécurité de la migration de réseaux virtuels. Au cours des années, la virtualisation a été utilisée pour optimiser l'usage des ressources informatiques et pour supporter les infrastructures des entreprises. La virtualisation consiste à allouer une partie des ressources d'une machine physique à un utilisateur (sous la forme d'une machine virtuelle) pour qu'il puisse l'exploiter. Les machines virtuelles sont utilisées pour héberger des services opérationnels comme un serveur internet ou une base de données. La virtualisation des réseaux n'a pas profité du même intérêt de la part des chercheurs et des acteurs industriels. Le paradigme du Software Defined Networking a introduit de nouvelles possibilités pour implémenter la virtualisation réseau et fournir aux utilisateurs une solution flexible pour leurs besoins métiers. Les réseaux virtuels sont utilisés pour interconnecter des machines virtuelles, et ils peuvent être configurés avec des règles de routages ou des protocoles de sécurité spécifiques. Dans l'éventualité où un équipement réseau tomberait en panne ou sous le coup d'une attaque informatique, le système d'hypervision va migrer les ressources afin de préserver la disponibilité des services utilisateurs.La sécurité des machines virtuelles et de leur migration est un domaine de recherche qui a été grandement exploré par le passé, tandis que la virtualisation réseau et plus spécifiquement la migration de réseaux virtuels restent encore des domaines de recherche assez jeune et où beaucoup reste à faire. La surface d'attaque de la virtualisation réseau est similaire en nature à celle de la virtualisation traditionnelle, mais elle présente un aspect supplémentaire dû à l'usage du paradigme du Software Defined Networking. La motivation de notre travail est d'étudier la sécurité du processus de migration des réseaux virtuels, dans le contexte du Software Defined Networking. Nous proposons d'atteindre cet objectif en trois phases. Tout d'abord, nous définissons le périmètre de cette étude, et nous concentrons sur l'aspect réseau de la migration. Ensuite, nous décrivons le modèle d'attaquant afin de compromettre la migration des réseaux et nous concevons un mécanisme de détection contre les attaques envers l'infrastructure de virtualisation. Enfin, nous améliorons le mécanisme de défense en optimisant le déploiement des ressources de détection afin d'obtenir une couverture optimale de l'infrastructure.Dans la première partie de cette thèse, nous proposons une approche formelle pour décrire les différents composants de l'infrastructure de virtualisation.Nous utilisons un formalisme de logique du premier ordre pour décrire différentes propriétés de sécurité sous la forme de prédicats booléens.Cette modélisation inclut la représentation des données des utilisateurs finaux ainsi que l'infrastructure de virtualisation.Une trace d'exécution est générée pendant la migration d'un réseau virtuel, et est ensuite utilisée par un prouveur de théorème afin de vérifier formellement si la sécurité de la migration a été respectée. Le modèle formel est basé sur la supposition que la trace d'exécution est générée par un outil de supervision exempt de tout défaut. Ceci implique que la preuve formelle est complète. Nous levons cette hypothèse en modélisant un problème d'allocation de ressources afin de déterminer quels équipements réseau devraient être chargés de la détection d'attaques pour une couverture optimale. Nous résolvons ce problème en utilisant un processus de décision markovien. Nous concluons notre optimisation en proposant un déploiement statique des ressources, en amont de toute migration
This thesis investigates the security of virtual network migration. Over the years, virtualization has been used to optimize physical resources and to support businesses’ infrastructure. Virtualization consists in exposing a fraction of a resource for a user to operate. Virtual Machines are used to host business services like web servers or a backup service. Network virtualization has not benefited from the same interest from researchers and the industry. The Software Defined Networking paradigm has introduced new possibilities to implement network virtualization and provide users with a flexible network, decoupled from the physical equipment. Virtual Networks are used to interconnect Virtual Machines and can be configured with specific routing policies or security protocols. In case of a failure of the resource, either accidental or intentional, the virtualization infrastructure will migrate the resource to maintain the service provided.The security of Virtual Machines and their migration is a well-researched topic that has been widely in the past, while the study of network virtualization and especially the migration process only are at an early stage. The attack surface of network virtualization is similar in nature to the virtualization of legacy resources, and presents an additional aspect because of the use of Software Defined Networking.The motivation of this research is to investigate the security of the virtual network migration process in the context of Software Defined Networking. In order to do so, we first define the scope of the study and focus on the networking aspect of the migration. Then, we outline the threat model of the migration process and devise a detection mechanism against attacks in the virtualization infrastructure. Finally, we optimize the previous mechanism by optimizing the deployment of network monitoring resources for an optimal coverage.In the first part of this thesis we propose a formal approach to describe the different aspects of the virtualization infrastructure. We use a first order formalism to model several security properties as a set of logical predicates. These predicates account for both physical and virtual elements of the virtualization infrastructure, and the data use by both end users and the infrastructure owner.An execution trace is generated during the migration of a virtual network, and will be used by a theorem prover to compute a formal proof to verify if a security violation occurred. The first order model is based on the assumption that the execution trace is generated using perfect monitoring. This implies that the proof is complete and that the networking monitoring is always done under optimal conditions.We alleviate this assumption by modeling a resource allocation problem to determine how the monitoring resources should be deployed and which network nodes provide the best coverage. We solve this problem using a Markov Decision Process, and determine a dynamic deployment of monitoring resources during the migration. We conclude our optimization with a proposition of a static deployment of the resources prior to the migration

APA, Harvard, Vancouver, ISO, and other styles

22

Wiedling, Cyrille. "Formal verification of advanced families of security protocols : E-voting and APIs." Thesis, Université de Lorraine, 2014. http://www.theses.fr/2014LORR0199/document.

Full text

Abstract:

Les méthodes formelles ont fait leurs preuves dans l’étude des protocoles de sécurité et plusieurs outils existent, permettant d’automatiser ces vérifications. Hélas, ils se montrent parfois dans l’incapacité d’analyser certains protocoles, à cause des primitives cryptographiques employées ou des propriétés que l’on cherche à démontrer. On étudie deux systèmes existants: un protocole de vote par internet Norvégien et un protocole pour les votes en réunion du CNRS. Nous analysons les garanties de sécurité qu’ils proposent, dans différents scénarios de corruption. Malgré les résultats réutilisables obtenus, ces preuves démontrent également la difficulté de les effectuer à la main. Une nouvelle piste dans l’automatisation de telles preuves pourrait alors venir des systèmes de types. Basés sur le développement récent d’un système de types permettant de traiter des propriétés d’équivalence, nous l’avons utilisé afin de démontrer des propriétés comme l’anonymat du vote. Nous avons appliqué cette méthode Helios, un système de vote par internet bien connu. Il existe une autre famille de protocoles de sécurité : les APIs. Ces interfaces permettent l’utilisation d’informations stockées dans des dispositifs sécurisés sans qu’il soit normalement possible de les en ex- traire. Des travaux récents montrent que ces interfaces sont également vulnérables. Cette thèse présente un nouveau design d’API, incluant une fonctionnalité de révocation, rarement présente dans les solutions existantes. Nous démontrons, par une analyse formelle, qu’aucune combinaison de commandes ne permet de faire fuir des clefs sensées rester secrètes, même si l’adversaire parvient à en brute-forcer certaines
Formal methods have been used to analyze security protocols and several tools have even been developed to tackle automatically different proof techniques and ease the verification of such protocols. However, for electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives, or the security properties, involved in those protocols. We work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. We analyze them using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even including several reusable results, these proofs are complex and, therefore, expose a real need for automation. Thus, we focus on a possible lead in direction of this needed automation: type-systems. We build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in electronic voting like ballot-secrecy. We present an application of this method through Helios, a well-known e-voting system. Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Recet work seems to show that these interfaces are also vulnerable. In this thesis, we provide a new design for APIs, including revocation. In addition, we include a formal analysis of this API showing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them

APA, Harvard, Vancouver, ISO, and other styles

23

Debant, Alexandre. "Symbolic verification of distance-bounding protocols : application to payment protocols." Thesis, Rennes 1, 2020. http://www.theses.fr/2020REN1S057.

Full text

Abstract:

L’essor des nouvelles technologies, et en particulier la Communication en Champ Proche (NFC), a permis l’apparition de nouvelles applications. Á ce titre, nous pouvons mentionner le paiement sans contact, les clefs mains libres ou encore les carte d’abonnement dans les transports en commun. Afin de sécuriser l’ensemble de ces applications, des protocoles de sécurité, appelés protocoles délimiteurs de distance on été développés. Ces protocoles ont pour objectif d’assurer la proximité physique des appareils mis en jeu afin protocole cryptographique, protocole de paiement de limiter le risque d’attaque. Dans ce manuscrit, nous présentons diverses approches permettant une analyse formelle de ces protocoles. Dans ce but, nous proposons un modèle symbolique permettant une modélisation précise du temps ainsi que des positions dans l’espace de chaque participant. Nous proposons ensuite deux approches : la première développant une nouvelle procédure de vérification, la seconde permettant la ré-utilisation d’outils existants tels que Proverif. Tout au long de ce manuscrit, nous porterons une attention parti- culières aux protocoles de paiement sans contact
The rise of new technologies, and in particular Near Field Communication (NFC) tags, offers new applications such as contactless payments, key-less entry systems, transport ticketing... Due to their security concerns, new security protocols, called distance-bounding protocols, have been developed to ensure the physical proximity of the de- vices during a session. In order to prevent flaws and attacks, these protocols require formal verification. In this manuscript, we present several techniques that allow for an automatic verification of such protocols. To this aim, we first present a symbolic model which faithfully models time and locations. Then we develop two approaches : either ba- sed on a new verification procedure, or leveraging existing tools like Proverif. Along this manuscript, we pay a particular attention to apply our results to contactless payment protocols

APA, Harvard, Vancouver, ISO, and other styles

24

Krasnowski, Piotr. "Codage conjoint source-chiffrement-canal pour les canaux de communication vocaux sécurisés en temps réel." Thesis, Université Côte d'Azur, 2021. http://www.theses.fr/2021COAZ4029.

Full text

Abstract:

Les risques croissants de violation de la vie privée et d’espionnage associés à la forte croissance des communications mobiles ont ravivé l’intérêt du concept originel de chiffrement de la parole sous forme de signaux audio transmis sur des canaux vocaux non spécifiques. Les méthodes habituelles utilisées pour la transmission de données cryptées par téléphonie analogique se sont révélées inadaptées pour les communications vocales modernes (réseaux cellulaires, VoIP) avec leurs algorithmes de compression de la voix, de détection d’activité vocale et de suppression adaptative du bruit. La faible bande passante disponible, les distorsions non linéaires des canaux et les phénomènes d’évanouissements du signal motivent l’introduction d’une approche conjointe du codage et du chiffrement de la parole adaptée aux canaux vocauxbruités modernes.Dans cette thèse sont développés, analysés et validés divers schémas sûrs et efficaces pour le chiffrement et la transmission de la parole en temps réel pour les canaux vocaux modernes. En plus du chiffrement de la parole, cette étude couvre les aspects sécurité et algorithmique de l’ensemble du système de communication vocale - aspects critiques d’un point de vue industriel. La thèse détaille un système de chiffrement de la parole associé à un codage avec perte, par brouillage aléatoire des paramètres vocaux (volume, hauteur, timbre) de certaines représentations de la parole. En résulte un pseudo-signal vocal chiffré robuste aux erreurs ajoutées par les canaux de transmission modernes. La technique de chiffrement repose sur l’introduction de translations et rotations aléatoires sur des maillages de tores plats associés à des codes sphériques. Face aux erreurs de transmission, le schéma déchiffre approximativement les paramètres vocaux et reconstruit, grâce à un synthétiseur vocal utilisant un réseau de neurones par apprentissage, un signal de parole perceptuellement très proche du signal d’origine. Le dispositif expérimental a été validé par la transmission de signaux de type pseudo-voix chiffrés sur un canal vocal réel. Les signaux de parole déchiffrés ont été favorablement notés lors d’une évaluation subjective de qualité incluant environ 40 participants.La thèse décrit également une nouvelle technique de transmission de données sur canaux vocaux en utilisant un dictionnaire d’ondes harmoniques courtes représentant les mots d’un code quaternaire. La technique fournit un débit binaire variable allant jusqu’à 6.4 kbps et a été testée avec succès sur différents canaux vocaux réels. Enfin, est présenté aussi un protocole d’échange de clés cryptographiques dédié pour les canaux vocaux authentifiés par signatures et vérification vocale. La sécurité du protocole a été vérifiée sous forme d’un modèle symbolique par l’assistant de preuve formelle Tamarin.L’étude conclut qu’une communication vocale sécurisée sur des canaux vocaux numériques réels est techniquement et de fait viable lorsque les canaux vocaux utilisés pour la communication sont stables et ne présentent que des distorsions prévisibles
The growing risk of privacy violation and espionage associated with the rapid spread of mobile communications renewed interest in the original concept of sending encrypted voice as audio signal over arbitrary voice channels. The usual methods used for encrypted data transmission over analog telephony turned out to be inadequate for modern vocal links (cellular networks, VoIP) equipped with voice compression, voice activity detection, and adaptive noise suppression algorithms. The limited available bandwidth, nonlinear channel distortion, and signal fadings motivate the investigation of a dedicated, joint approach for speech encodingand encryption adapted to modern noisy voice channels.This thesis aims to develop, analyze, and validate secure and efficient schemes for real-time speech encryption and transmission via modern voice channels. In addition to speech encryption, this study covers the security and operational aspects of the whole voice communication system, as this is relevant from an industrial perspective.The thesis introduces a joint speech encryption scheme with lossy encoding, which randomly scrambles the vocal parameters of some speech representation (loudness, pitch, timbre) and outputs an encrypted pseudo-voice signal robust against channel noise. The enciphering technique is based on random translations and random rotations using lattices and spherical codes on flat tori. Against transmission errors, the scheme decrypts the vocal parameters approximately and reconstructs a perceptually analogous speech signal with the help of a trained neural-based voice synthesizer. The experimental setup was validated by sending encrypted pseudo-voice over a real voice channel, and the decrypted speech was tested using subjective quality assessment by a group of about 40 participants.Furthermore, the thesis describes a new technique for sending data over voice channels that relies on short harmonic waveforms representing quaternary codewords. This technique achieves a variable bitrate up to 6.4 kbps and has been successfully tested over various real voice channels. Finally, the work considers a dedicated cryptographic key exchange protocol over voice channels authenticated by signatures and a vocal verification. The protocol security has been verified in a symbolic model using Tamarin Prover.The study concludes that secure voice communication over real digital voice channels is technically viable when the voice channels used for communication are stable and introduce distortion in a predictable manner.stabintroduce distortion in a predictable manner

APA, Harvard, Vancouver, ISO, and other styles

25

Geeraerts, Gilles. "Coverability and expressiveness properties of well-structured transition systems." Doctoral thesis, Universite Libre de Bruxelles, 2007. http://hdl.handle.net/2013/ULB-DIPOT:oai:dipot.ulb.ac.be:2013/210724.

Full text

Abstract:

Ces cinquante dernières annéees, les ordinateurs ont occupé une place toujours plus importante dans notre vie quotidienne. On les retrouve aujourd’hui présents dans de nombreuses applications, sous forme de systèmes enfouis. Ces applications sont parfois critiques, dans la mesure où toute défaillance du système informatique peut avoir des conséquences catastrophiques, tant sur le plan humain que sur le plan économique.

Nous pensons par exemple aux systèmes informatiques qui contrôlent les appareils médicaux ou certains systèmes vitaux (comme les freins) des véhicules automobiles.

Afin d’assurer la correction de ces systèmes informatiques, différentes techniques de vérification Assistée par Ordinateur ont été proposées, durant les trois dernières

décennies principalement. Ces techniques reposent sur un principe commun: donner une description formelle tant du système que de la propriété qu’il doit respecter, et appliquer une méthode automatique pour prouver que le système respecte la propriété.

Parmi les principaux modèles aptes à décrire formellement des systèmes informatiques, la classe des systèmes de transition bien structurés [ACJT96, FS01] occupe une place importante, et ce, pour deux raisons essentielles. Tout d’abord, cette classe généralise plusieurs autres classes bien étudiées et utiles de modèles à espace

d’états infini, comme les réseaux de Petri [Pet62](et leurs extensions monotones [Cia94, FGRVB06]) ou les systèmes communiquant par canaux FIFO avec pertes [AJ93]. Ensuite, des problèmes intéressants peuvent être résolus algorithmiquement sur cette classe. Parmi ces problèmes, on trouve le probléme de couverture, auquel certaines propriétés intéressantes de sûreté peuvent être réduites.

Dans la première partie de cette thèse, nous nous intéressons au problème de couverture. Jusqu’à présent, le seul algorithme général (c’est-à-dire applicable à n’importe quel système bien structuré) pour résoudre ce problème était un algorithme dit en arrière [ACJT96] car il calcule itérativement tous les états potentiellement non-sûrs et vérifie si l’état initial du système en fait partie. Nous proposons Expand, Enlarge and Check, le premier algorithme en avant pour résoudre le problème de couverture, qui calcule les états potentiellement accessibles du système et vérifie si certains d’entre eux sont non-sûrs. Cette approche est plus efficace en pratique, comme le montrent nos expériences. Nous présentons également des techniques permettant d’accroître l’efficacité de notre méthode dans le cas où nous analysons des réseaux de Petri (ou

une de leurs extensions monotones), ou bien des systèmes communiquant par canaux FIFO avec pertes. Enfin, nous nous intéressons au calcul de l’ensemble de couverture pour les réseaux de Petri, un objet mathématique permettant notamment de résoudre le problème de couverture. Nous étudions l’algorithme de Karp & Miller [KM69], une solution classique pour calculer cet ensemble. Nous montrons qu’une optimisation de cet algorithme présenté dans [Fin91] est fausse, et nous proposons une autre solution totalement neuve, et plus efficace que la solution de Karp & Miller.

Dans la seconde partie de la thèse, nous nous intéressons aux pouvoirs d’expression des systèmes bien structurés, tant en terme de mots infinis que de mots finis. Le pouvoir d’expression d’une classe de systèmes est, en quelque sorte, une mesure de la diversité des comportements que les modèles de cette classe peuvent représenter. En ce qui concerne les mots infinis, nous étudions les pouvoirs d’expression des réseaux de Petri et de deux de leurs extensions (les réseaux de Petri avec arcs non-bloquants et les réseaux de Petri avec arcs de transfert). Nous montrons qu’il existe une hiérarchie stricte entre ces différents pouvoirs d’expression. Nous obtenons également des résultats partiels concernant le pouvoir d’expression des réseaux de Petri avec arcs de réinitialisation. En ce qui concerne les mots finis, nous introduisons la classe des langages bien structurés, qui sont des langages acceptés par des systèmes de transition bien structurés étiquettés, où l’ensemble des états accepteurs est clos par le haut. Nous prouvons trois lemmes de pompage concernant ces langages. Ceux-ci nous permettent de réobtenir facilement des résultats classiques de la littérature, ainsi que plusieurs nouveaux résultats. En particulier, nous prouvons, comme dans le cas des mots infinis, qu’il existe une hiérarchie stricte entre les pouvoirs d’expression des extensions des réseaux de Petri considérées.
Doctorat en sciences, Spécialisation Informatique
info:eu-repo/semantics/nonPublished

APA, Harvard, Vancouver, ISO, and other styles

26

Ribeiro, Marcelo Alves. "Méthodes formelles pour la vérification probabiliste de propriétés de sécurité de protocoles cryptographiques." Thesis, Université Laval, 2011. http://www.theses.ulaval.ca/2011/28121/28121.pdf.

Full text

Abstract:

Certains protocoles cryptographiques ont été développés spécifiquement pour assurer quelques propriétés de sécurité dans nos réseaux de communication. Dans le but de s'assurer qu'un protocole remplit ses propriétés de sécurité, des vérifications probabilistes y sont donc entreprises afin de confirmer s'il présente des failles lorsqu'on prend en compte leur comportement probabiliste. Nous avons voulu entreprendre une méthode probabiliste, mais aussi non-déterministe, de modélisation de protocoles afin de confirmer si cette méthode peut remplacer d'autres qui ont déjà été utilisées pour vérifier des failles sur des protocoles cryptographiques. Cela nous a motivé à envisager comme objectif de nos recherches scientifiques, des analyses quantitatives des possibilités de faille sur des protocoles cryptographiques.
Certain cryptographic protocols were specifically developed to provide some security properties in our networks of communication. For the purpose of assuring that a protocol fulfils its security properties, probabilistic model checkings are undertaken to confirm if it introduces a fault when its probabilistic behavior is considered. We wanted to use a probabilistic method (and also non-deterministic) of protocols modeling to confirm if this method may substitute others that were already used for checking faults in cryptographic protocols. It leads us to consider the objective of our scientific researches as: quantitative analysis of faults in cryptographic protocols.

APA, Harvard, Vancouver, ISO, and other styles

27

Embe, Jiague Michel. "Approches formelles de mise en oeuvre de politiques de contrôle d'accès pour des applications basées sur une architecture orientée services." Thèse, Université de Sherbrooke, 2012. http://hdl.handle.net/11143/6683.

Full text

Abstract:

La sécurité des systèmes d'information devient un enjeu préoccupant pour les organisations tant publiques que privées, car de tels systèmes sont pour la plupart universellement accessibles à partir de navigateurs Web. Parmi tous les aspects liés à la sécurité des systèmes d'information, c'est celui de la sécurité fonctionnelle qui est étudié dans cette Thèse sous l'angle de la mise en oeuvre de politiques de contrôle d'accès dans une architecture orientée services. L'élément de base de la solution proposée est un modèle générique qui introduit les concepts essentiels pour la conception de gestionnaires d'exécution de politiques de contrôle d'accès et qui établit une séparation nette entre le système d'information et les mécanismes de contrôle d'accès. L'instanciation de ce modèle conduit à un cadre d'applications qui comporte, entre autres, un filtre de contrôle d'accès dynamique. Cette Thèse présente également deux méthodes systématiques d'implémentation de ce filtre à partir de politiques écrites en ASTD, une notation graphique formelle basée sur les statecharts augmentés d'opérateurs d'une algèbre de processus. La notation ASTD est plus expressive que la norme RBAC et ses extensions. La première méthode repose sur une transformation de politiques de contrôle d'accès, instanciées à partir de patrons de base exprimés en ASTD, en des processus BPEL. La deuxième méthode est basée sur une interprétation de spécifications ASTD par des processus BPEL. Dans les deux cas, les processus BPEL s'exécutent dans un moteur d'exécution BPEL et interagissent avec le système d'information. Ces deux méthodes permettent une implémentation automatique d'un cadre d'applications à partir de la spécification de départ. Finalement, un prototype a été réalisé pour chacune des deux méthodes afin de montrer leur faisabilité au niveau fonctionnel et de comparer leurs performances au niveau système.

APA, Harvard, Vancouver, ISO, and other styles

28

Berner, David. "Utilisation de méthodes formelles dans la conception conjointe de systèmes embarqués." Rennes 1, 2006. http://www.theses.fr/2006REN1S015.

Full text

Abstract:

La modélisation du contenu des puces pour systèmes embarqués s'avère de plus en plus difficile puisque le développement des outils et des méthodologies de modélisation n'a pas su accompagner l'explosion de la complexité des systèmes. Les méthodes formelles ont su démontrer dans les dernières années leurs capacités de prévention et de détection d'erreurs, ainsi que leurs avantages dans l'expression univoque de demandes et dans la spécification de systèmes. Malgré cela, leur utilisation reste toujours restreinte en raison d'un manque de liens avec les méthodes existantes et la difficulté de leur utilisation. Dans ce document, on essaye de montrer dans quelle mesure la conception de systèmes embarqués peut profiter de l'utilisation de méthodes formelles. Pour cela, plusieurs exemples sont présentés qui démontrent comment l'utilisation des méthodes formelles peut être intégrée dans la conception conjointe tout en cachant - du moins en partie - leur complexité inhérente.

APA, Harvard, Vancouver, ISO, and other styles

29

Pagani, Florence. "Ordres partiels pour la vérification de systèmes temps réel." Toulouse, ENSAE, 1997. http://www.theses.fr/1997ESAE0005.

Full text

Abstract:

Si l'utilité des méthodes de vérification formelle des systèmes temps réel est désormais reconnue, leur application à des systèmes complexes est encore freinée par les performances des outils disponibles. En particulier, la vérification de modèles fondée sur l'exploration exhaustive de l'espace des états d'un système est souvent limitée par ce que l'on appelle l'explosion combinatoire des états. Ce phénomène est encore accentué lorque des aspects quantitatifs (durée des actions par exemple) sont introduits dans le modèle. Une partie de l'xplosion combinatoire est due à la modélisation du parallélisme par l'entrelacement non déterministe des actions. Les techniques dites d'ordre partiel tirent parti de l'indépendance des actions s'exécutant en parallèle pour réduire l'espace des états à explorer. Ces techniques ont initialement été développées pour la vérification des systèmes temps réels afin de prendre en compte des aspects temporels quantitatifs. Nous nous intéressons en particulier à l'intégration de ces techniques dans les méthodes de vérification symboliques développées pour des automates temporisés.

APA, Harvard, Vancouver, ISO, and other styles

30

Prigent, Armelle. "Le test des systèmes temps-réel paramétrés : application à la conception d'architectures avioniques." Nantes, 2003. http://www.theses.fr/2003NANT2097.

Full text

Abstract:

Les systèmes embarqués critiques doivent être soumis à une validation rigoureuse afin d'assurer leurs performances et leur sûreté de fonctionnement. Le test de conformité est l'activité permettant de s'assurer que le produit final correspond aux attentes de la spécification. Dans le cas des systèmes temps-réel, il est important de tester la conformité en prenant en considération les contraintes temporelles du modèle. Cette thèse propose une approche de génération de tests pour des systèmes d'automates temporisés paramétrés. L'algorithme de construction des tests utilise un objectif de test pour sélectionner les comportements à tester. Les tests sont construits grâce à une analyse d'accessibilité symbolique des états du modèle, et une représentation des contraintes d'horloges par une extension paramétrée des diagrammes différentiels d'horloges Clock difference diagrams. Au cours de ce travail, nous avons développé un outil de génération de tests : RTT (Real Time Test Generator).

APA, Harvard, Vancouver, ISO, and other styles

31

Radhouani, Amira. "Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information." Thesis, Université Grenoble Alpes (ComUE), 2017. http://www.theses.fr/2017GREAM025/document.

Full text

Abstract:

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description Secure UML des règles de contrôle d’accès basées sur les rôles. Ces vulnérabilités étant dues à l’évolution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système. Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes. Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles
The early detection of potential threats during the modelling phase of a Secure Information System (IS) is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This involves studying the validation of access control rules and performing vulnerabilities automated checks before the IS operationalization. We are particularly interested in detecting vulnerabilities that can be exploited by internal trusted users to commit attacks, called insider attacks, by taking advantage of their legitimate access to the system. To do so, we use formal B specifications which are generated by the B4MSecure platform from UML functional models and a SecureUML modelling of role-based access control rules. Since these vulnerabilities are due to the dynamic evolution of the functional state, we propose to study the reachability of someundesirable states starting from a normal state of the system. The proposed techniques are an alternative to model-checking techniques. Indeed, they implement symbolic backward search algorithm based on complementary approaches: proof and constraint solving. This rich technical background allowed the development of the GenISIS tool which automates our approach and which was successfully experimented on several case studies available in the literature. These experiments showed its capability to extract already published attacks but also new attacks

APA, Harvard, Vancouver, ISO, and other styles

32

Fayolle, Thomas. "Combinaison de méthodes formelles pour la spécification de systèmes industriels." Thesis, Paris Est, 2017. http://www.theses.fr/2017PESC1078/document.

Full text

Abstract:

La spécification d’un système industriel nécessite la collaboration d’un ingénieur connaissant le système à modéliser et d’un ingénieur connaissant le langage de modélisation. L'utilisation d'un langage de spécification graphique, tel que les ASTD (Algebraic State Transition Diagram), permet de faciliter cette collaboration. Dans cette thèse, nous définissons une méthode de spécification graphique et formelle qui combine les ASTD avec les langages Event-B et B. L’ordonnancement des actions de la spécification est décrit par les ASTD et le modèle de données est décrit dans la spécification Event-B. La spécification B permet de vérifier la cohérence du modèle : les événements Event-B doivent pouvoir être exécutés lorsque les transitions associées doivent l’être. Un raffinement combiné des ASTD et d’Event-B permet la spécification incrémental du système. Afin de valider son apport, la méthode de spécification a été utilisée pour la spécification de cas d’études
Specifying industrial systems requires collaboration between an engineer that knows how the system works and an engineer that know the specification language. Graphical specification languages can help this collaboration. In this PhD Thesis a method is defined that combines ASTD (Algebraic State Transition Diagram), a formal graphical notation, with B and Event-B langagues. The ordering of actions is specified using ASTD and the data model is specified using Event-B. B specification is used to verify the consistency of the model : Event-B events have to be executed when the corresponding transitions have to be executed. A combined refinement allows to incrementaly design the system

APA, Harvard, Vancouver, ISO, and other styles

33

Proch, Cyril. "Assistance au développement incrémental et prouvé de systèmes enfouis." Nancy 1, 2006. http://docnum.univ-lorraine.fr/public/SCD_T_2006_0012_PROCH.pdf.

Full text

Abstract:

Les méthodes de développement rigoureuses ne se sont pas encore imposées en électronique. La validation des systèmes se fait par des séries de tests ou par l'utilisation de model checker ne couvrant pas toutes les possibilités. Nous avons élaboré une méthode de développement par la preuve en nous appuyant sur une étude de cas (TV numérique). Le raffinement est central à nos travaux car il permet de conserver la traçabilité et distribue la complexité du système et des preuves. Les modèles construits aident aux choix architecturaux en structurant les tâches du système. Nous avons proposé un mécanisme de traduction de modèles produisant du code SystemC. Le code obtenu sert de support aux expérimentations électroniques. La traduction est prouvée par des modèles B décrivant la sémantique de simulation SystemC. Un programme est représenté par un modèle B, instanciation des modèles de simulation. Nous montrons que l'exécution des programmes traduits conservent les propriétés des modèles
Design process in electronic engineering is not formally defined and developments are based on empirical knowledge. Systems validation is made by tests but these are incomplete and all scenarios or use cases are not tested. We propose a design method built on proof and based on a case study, the RNRT project EQUAST, in the domain of digital television (DVB-T). Our works are based on refinement and its use helps tracability by distributing complexity in steps of refinement. The models help designer in his choices by structuring tasks of the system thanks to invariant properties and refinement. We propose a translation from models to SystemC code; produced code conserves properties of source models and helps to verify electronic constraints. Translation correction is proved by use of B event-based models which explain simulation semantics of SystemC. A specific SystemC program can be represented with a B model. This model is an instanciation of generic models describing SystemC simulation. With the help of refinement, we have shown that simulation of programs conserves properties of abstract models

APA, Harvard, Vancouver, ISO, and other styles

34

Sagaspe, Laurent. "Allocation sûre dans les systèmes aéronautiques : modélisation, vérification et génération." Thesis, Bordeaux 1, 2008. http://www.theses.fr/2008BOR13707/document.

Full text

Abstract:

Les architectures des systèmes embarqués des nouvelles générations d'avions civils et militaires tendent à s'organiser autour d'une plateforme avionique constituée de calculateurs interconnectés par un réseau central. Ce type d'architecture a fait apparaitre le besoin de développer de nouvelles méthodes de conception afin d'assister le dialogue entre les concepteurs des fonctions à embarquer (commandes de vol, gestion de l'énergie, ...) et les architectes de la plateforme avionique. Il est, en particulier, primordial de s'assurer que l'allocation des ressources de la plateforme aux fonctions embarquées respecte les exigences de sûreté de fonctionnement propres aux systèmes avioniques. Dans un premier temps, un cadre général a été proposé pour modéliser et vérifier l'effet de l'allocation des ressources d'une plateforme avionique du point de la sûreté de fonctionnement. Ce cadre est fondé sur l'utilisation du langage AltaRica pour décrire formellement la propagation des défaillances au sein de systèmes embarqués et des outils associés à ce langage (model-checking, génération de séquences et d'arbres de défaillances) pour vérifier la tenue des exigences de sûreté de fonctionnement. Ce cadre a été utilisé pour étudier, d'une part, l'allocation d'équipements informatiques aux fonctions de systèmes embarqués, et d'autre part, les placements des équipements au sein de l'avion en tenant compte de risques tels que l'éclatement d'un pneu ou l'explosion d'un moteur. Dans un second temps, la génération d'allocations respectant les exigences de sûreté de fonctionnement a été étudiée. L'approche retenue est fondée sur l'expression de contraintes d'allocation sous forme d'inégalités linéaires entières et sur l'utilisation de techniques de résolution de ces contraintes. Plusieurs types de contraintes (ségrégation, co-location, exclusion, ...) sont pris en compte. De plus, des critères d'optimisation permettent de guider la résolution des contraintes de façon à proposer des allocations les plus pertinentes du point de vue des besoins des systèmes aéronautiques. Finalement, une approche intégrant les techniques de vérification et de génération a été proposée. La première étape consiste à vérifier un modèle des fonctions embarquées qui est indépendant de la plateforme avionique. Il est possible d'extraire automatiquement des contraintes d'allocation à partir des résultats de cette vérification. L'étape de résolution de contraintes génère alors une allocation sûre. Les travaux sont illustrés par deux études de cas industrielles : une fonction de suivi de terrain d'un avion de chasse et un système de génération et de distribution hydraulique d'un avion de type A320
Abstract

APA, Harvard, Vancouver, ISO, and other styles

35

Doche, Marielle. "Techniques formelles pour l'évaluation de systèmes critiques complexes : test et modularité." École nationale supérieure de l'aéronautique et de l'espace (Toulouse ; 1972-2007), 1999. http://www.theses.fr/1999ESAE0024.

Full text

Abstract:

L'intérêt des méthodes formelles est de permettre le développement rigoureux de systèmes informatiques critiques. Pour des systèmes complexes, elles peuvent être complétées par des formalismes de structuration et de modularité. Nous proposons ici une démarche pour la génération et l'évaluation de jeux de test fonctionnel à partir de spécifications formelles structurées ou modulaires. Nous nous appuyons sur un formalisme de spécification modulaire Moka-TRIO basé d'une part sur la théorie des catégories et le calcul des modèles défini par Ehrig et Mahr (qui permettent de structurer une modélisation et éventuellement d'encapsuler des données) et d'autre part sur la logique temporelle métrique TRIO (pour décrire des comportements réactifs). Des outils associés à ce formalisme permettent de définir et valider une spécification complexe. Nous montrons comment la structure d'une spécification Moka-TRIO permet de mettre en avant différents niveaux d'abstraction pour le test : unitaire, intégration, agrégat et système. Pour chacun de ces niveaux, nous décrivons un mécanisme de génération de jeux de test à partir d'une spécification complexe en s'appuyant sur la sémantique de celle-ci. Enfin, nous reprenons le cadre théorique d'évaluation défini par Bernot, Gaudel et Marre qui détermine la pertinence d'un jeu de test. En étendant la définition d'institution pour prendre en compte des catégories de cas de test, nous montrons comment nos mécanismes de génération permettent de définir des jeux pertinents. L'outil Moka-TRIO implémente les différents mécanismes de génération. L'approche a été appliquée à un système de contrôle de commandes électriques de vol.

APA, Harvard, Vancouver, ISO, and other styles

36

Sassolas, Mathieu. "Méthodes qualitatives et quantitatives pour la détection d'information cachée." Paris 6, 2011. http://www.theses.fr/2011PA066581.

Full text

Abstract:

Les systèmes informatiques sont devenus omniprésents et sont utilisés au quotidien pour gérer toujours plus d'information. Ces informations sont de plus en plus souvent confidentielles: informations stratégiques militaires ou financières, données personnelles. La fuite de ces informations peut ainsi avoir des conséquences graves telles que des pertes humaines, financières, des violations de la vie privée ou de l'usurpation d'identité. Les contributions de cette thèse se découpent en trois parties. Tout d'abord, nous étudions le problème de synthèse d'un canal de communication dans un système décrit par un transducteur. Malgré les limites imposées par ce modèle, nous montrons que le problème de synthèse est indécidable en général. Cependant, lorsque le système est fonctionnel, c'est-à-dire que son fonctionnement externe est toujours le même, le problème devient décidable. Nous généralisons ensuite le concept d'opacité aux systèmes probabilistes, en donnant des mesures groupées en deux familles. Lorsque le système est opaque, nous évaluons la robustesse de cette opacité vis-à-vis des informations données par les lois de probabilités du système. Lorsque le système n'est pas opaque, nous évaluons la taille de la faille de sécurité induite par cette non opacité. Enfin, nous étudions le modèle des automates temporisés à interruptions (ITA) où les informations sur l'écoulement du temps sont organisées en niveaux comparables à des niveaux d'accréditation. Nous étudions les propriétés de régularité et de clôture des langages temporisés générés par ces automates et proposons des algorithmes de model-checking pour des fragments de logiques temporelles temporisées.

APA, Harvard, Vancouver, ISO, and other styles

37

Demangeon, Romain. "Terminaison des systèmes concurrents." Lyon, Ecole normale supérieure, 2010. http://www.theses.fr/2010ENSL0595.

Full text

Abstract:

Cette thèse propose une étude de la terminaison dans les systèmes concurrents. La terminaison est une propriété désirable pour les programmes en elle même et comme prérequis pour d'autres propriétés. La cadre du pi calccul est présente dans la section 2. Dans la section 3, des systèmes de types de bases sur le poids sont présentés. Dans la section 4, on montre comment utiliser des approches pour aborder la question de la terminaison des langages concurrents d'ordre supérieur. Dans la section 5, on propose une étude de la complexité du problème de l'inférence pour les analyses basées sur le poids. La section 6 présente brièvement des analyses sémantiques de la terminaison. La section 7 s'intéresse à l'étude de la terminaison d'un pi-calcul impur composé d'un noyau fonctionnel et de constructions impératives. Une nouvelle technique de preuve par élagage est développée. Enfin, on illustre l'efficacité de cette technique en montrant comment elle peut-être appliquée à un lambda calcul avec références
This thesis proposes a study of termination for concurrent languages. Termination is a key-property for concurrent programs. It is useful in itself and as a prerequisite for other properties. The framework of the pi-calculus is presented in section 2. Some existing weight-based type systems as well as new refinments are presented in Section 3. Section 4 is dedicated to results about termination in higher-order concurrent calculi where the [m]essages exchanges are pieces of code. Section 5, we propose a study of the complexity of the inference problem for the weight-based type systems. In section 6, termination techniques based on logical relations are presented. Section 7 contained results about the termination of an impure pi-calculus where a functional core is distinguished from the imperative constructs. A new pruning technique is used for the soundness proof. A last chapter illustrates the efficiency of this new method by ensuring terrmination in a impure lambda-calculi

APA, Harvard, Vancouver, ISO, and other styles

38

Chorfi, Redha. "Abstraction et vérification de programmes informatiques." Thesis, Université Laval, 2008. http://www.theses.ulaval.ca/2008/25710/25710.pdf.

Full text

Abstract:

Les systèmes informatiques offrent une grande flexibilité aux usagers en leur permettant l’accès, notamment par le biais de réseaux de télécommunication ou de l’Internet, à un vaste éventail de services. Toutefois, certains de ces services sont soumis à de fortes contraintes de sécurité, comme le télépaiement qui est au coeur du commerce électronique. Ainsi, les fournisseurs et les utilisateurs expriment des besoins croissants, et antagonistes, en sécurité. Répondre à ces deux besoins simultanément est un enjeu technologique transversal à de nombreux domaines de l’informatique. L’objectif de ce travail est de développer un mécanisme permettant de garantir la sécurité des systèmes, en s’appuyant sur l’expérience établie dans le domaine de la sécurité et des méthodes formelles. Pour se faire, nous définissons un nouveau cadre de vérification des propriétés de sécurité d’un programme informatique par l’analyse des flots de données et de contrôle construits à partir du code de ce dernier. L’idée principale consiste à définir un modèle pouvant abstraire la trace d’événements et les dépendances de ressources engendrés au moment de l’exécution du programme, et pouvant être soumis à des algorithmes de vérification de modèle (model-checking) pour l’analyse de la sûreté du programme vis-à-vis d’une propriété.

APA, Harvard, Vancouver, ISO, and other styles

39

Turuani, Mathieu. "Sécurité des protocoles cryptographiques : décidabilité et complexité." Nancy 1, 2003. http://www.theses.fr/2003NAN10223.

Full text

APA, Harvard, Vancouver, ISO, and other styles

40

Souissi, Youssef. "Méthodes optimisant l'analyse des cryptoprocesseurs sur les canaux cachés." Phd thesis, Télécom ParisTech, 2011. http://pastel.archives-ouvertes.fr/pastel-00681665.

Full text

Abstract:

Ces dernières années, la sécurité des systèmes embarqués a fait l'objet de recherches intensives. Comme l'énergie, le coût et la performance; la sécurité est un aspect important qui doit être considérée tout au long du processus de conception d'un système embarqué. Des menaces récentes appelées "attaques par canaux cachés'' (Side-Channel Analysis (SCA)) ont attiré beaucoup d'attention dans le milieu de la sécurité embarquée. Ces attaques exploitent des propriétés physiques, telles que la consommation d'énergie ou le champ magnétique rayonné, afin de retrouver le secret. De plus, elles sont passives dans le sens où l'analyse se contente d'une observation extérieure du système sans l'endommager. Dans ce contexte, il est évident que la sécurisation des systèmes embarqués contre les attaques SCA constitue un aspect vital dans le flot de conception. Par conséquent, la nécessité d'assurer et d'évaluer la robustesse des systèmes embarqués contre ces attaques devient clair. Cette thèse propose principalement des techniques et méthodes génériques dans l'analyse par canaux cachés. Ces techniques qui touchent à différents aspects de l'analyse SCA (acquisition, pré-traitement, attaque et évaluation) peuvent être utilisées dans un cadre d'évaluation plus officiel tel que les Critères Communs (CC) ou le FIPS-140 afin d'améliorer la visibilité de l'évaluateur. Par ailleurs, le propriétaire d'un produit pourrait aussi se baser sur ces techniques dans le but d'évaluer la sécurité de son produit face aux attaques par canaux cachés avant de solliciter un certificat.

APA, Harvard, Vancouver, ISO, and other styles

41

Bonnefoi, Fabien. "Vérification formelle des spécifications de systèmes complexes par réseaux de Petri : application aux systèmes de transport intelligents." Paris 6, 2010. http://www.theses.fr/2010PA066616.

Full text

APA, Harvard, Vancouver, ISO, and other styles

42

Syed, Alwi Syed Hussein. "Vérification compositionnelle pour la conception sûre de systèmes embarqués." Paris 6, 2013. http://www.theses.fr/2013PA066230.

Full text

Abstract:

Afin d’améliorer la vérification de systèmes synchrones synthétisables, une méthode de vérification par model-checking basée sur une procédure de raffinement d’abstraction s’appuyant sur la structure en composants du système est proposée. Ayant opté pour la génération d'abstraction à partir des propriétés vérifiées des composants, différentes méthodes de sélection de propriétés pour l'abstraction initiale et les stratégies de raffinement pour améliorer le modèle abstrait sont présentées et analysées. La stratégie la plus directe est la technique de la Négation du Contre-exemple qui raffine le modèle abstrait en éliminant uniquement le contre-exemple fourni par le model-checker. La technique de la sélection de propriété est une autre stratégie où les propriétés disponibles sont organisées en fonction de leur pertinence par rapport à la propriété globale en exploitant les graphes de dépendances de ses variables. De plus, la phase de raffinement est assistée par un mécanisme de filtrage qui assure l’élimination du contre-exemple. Une technique complète basée sur le FSM a également été proposée pour résoudre les principaux problèmes dans l'abstraction dérivée des propriétés, notamment le manque de propriétés exploitables et la génération d’une bonne abstraction. Les techniques proposées ont été testées sur une plate-forme expérimentale d'un protocole industriel, le bus CAN. Les résultats expérimentaux montrent l'applicabilité des techniques proposées, les gains par rapport aux techniques traditionnelles et l’efficacité relative des trois stratégies proposées varient selon le contexte d’utilisation
In the aim of improving the verification of synthesizable synchronous systems, a model-checking method based on the abstraction-refinement procedure which relies on the compositional structure of the system is proposed. Having opted for the abstraction generation from verified component properties, different methods of property selection for the initial abstraction and the refinement strategies to improve the abstract model are presented and analyzed. The most straight-forward strategy is the Negation of the Counterexample Technique which refines the abstract model by eliminating exclusively the spurious counterexample provided by the model checker. The Property Selection Technique is another abstraction-refinement strategy where the available properties are ordered according to their relevance towards the global property by exploiting the dependency graphs of its variables. Furthermore, the refinement phase is assisted by a filtering mechanism that ensures the current counterexample will be eliminated. A comprehensive FSM-based technique has also been proposed to address the main problems in property based abstraction in compositional verification notably the lack of exploitable properties and the generation of a good abstraction. The techniques proposed have been tested on an experimental platform of an industrial protocol, the Controller Area Network (CAN). The experimental results demonstrate the applicability of the techniques proposed, the gains in comparison to conventional techniques and the relative effectiveness of the three strategies proposed varies according to the application context

APA, Harvard, Vancouver, ISO, and other styles

43

Tchuenkam, Tchoneng Honoré. "Techniques formelles pour le développement de systèmes de conduite de procédés manufacturiers : abstraction, spécification, synthèse et optimisation." Nancy 1, 1991. http://www.theses.fr/1991NAN10413.

Full text

Abstract:

Nous utilisons des techniques classiques d'abstraction, de spécification et de synthèse de programmes pour proposer une démarche de développement formel de systèmes temps réels dans le cadre (restreint) de la conduite des processus de productions discrètes. Dans le type de problème que nous avons à traiter, on dispose d'une installation industrielle dont les composants assurent des fonctions élémentaires de transformation, d'assemblage et de manutention de produits. Ces composants peuvent être mis en marche par des actionneurs et des capteurs fournissent des renseignements sur l'état du système et des produits. On souhaite construire un logiciel qui pilote l'installation existante pour obtenir un système global ayant certaines fonctionnalités. Nous préconisons une démarche qui consiste à:―faire une description abstraite et formelle de l'installation existante sans préjuger de son utilisation future, en combinant le formalisme des types abstraits et une extension temps réelle de la logique temporelle;―spécifier formellement le résultat attendu de son fonctionnement en indiquant essentiellement la relation qui existe entre les produits fabriqués et ceux de base. A partir des éléments précédents, nous synthétisons des programmes séquentiels de commande de l'installation donnée. Nous optimisons ensuite ces programmes en essayant de les paralléliser au maximum.

APA, Harvard, Vancouver, ISO, and other styles

44

Darlot, Christophe. "Reformulation et vérification de propriétés temporelles dans le cadre du raffinement de systèmes d'évènements." Besançon, 2002. http://www.theses.fr/2002BESA2054.

Full text

Abstract:

Les travaux présentés se placent dans le contexte de la vérification de propriétés temporelles sur des systèmes d'événements spécifiés par raffinement. Notre démarche se décompose en quatre étapes : 1-Nous vérifions une propriété abstraite par model-checking; 2- Nous raffinons le système et vérifions ce raffinement ; 3- Nous raffinons la propriété abstraite en une propriété dite reformulée; 4- Nous vérifions la propriété reformulée. L'apport de ces travaux est d'une part de permettre à l'utilisateur de raffiner les propriétés pour tenir compte des détails introduits lors du raffinement, d'autre part de diminuer l'effort de vérification en combinant preuve et model-checking. Ce travail, basé sur une définition de raffinement entre structures de Kripke étiquetées, nous a conduit a prouver la préservation des propriétés PLTL par raffinement et la correction de la démarche de vérification pour un ensemble de schémas de reformulation. Notre technique est implantée dans un prototype utilisant le prouveur PVS
We are interested in verifying temporal properties in event systems specified by refinement. We adopt a four-step method : 1- We verify an abstract property by model-checking; 2- We refine the system and verify the refinement; 3- We refine the abstract property into a reformulated property; 4- We verify the reformulated property; The main interest is in one hand to have the abstract properties refined by the specifier to take into account the details introduced during refinement, on the other hand to decrease the verification effort by combining proof and model-checking. This work, based on a refinement definition between labelled Kripke structures lead us to prove the preservation of PLTL properties through refinement and the correctness of the verification method for a set of reformulation patterns. This work is implemented in a prototype using the PVS prover

APA, Harvard, Vancouver, ISO, and other styles

45

Letan, Thomas. "Specifying and Verifying Hardware-based Security Enforcement Mechanisms." Thesis, CentraleSupélec, 2018. http://www.theses.fr/2018CSUP0002.

Full text

Abstract:

Dans ces travaux de thèse, nous nous intéressons à une classe de stratégies d'application de politiques de sécurité que nous appelons HSE, pour Hardware-based Security Enforcement. Dans ce contexte, un ou plusieurs composants logiciels de confiance contraignent l'exécution du reste de la pile logicielle avec le concours de la plate-forme matérielle sous-jacente afin d'assurer le respect d'une politique de sécurité donnée. Pour qu'un mécanisme HSE contraigne effectivement l'exécution de logiciels arbitraires, il est nécessaire que la plate-forme matérielle et les composants logiciels de confiance l'implémentent correctement.Ces dernières années, plusieurs vulnérabilités ont mis à défaut des implémentations de mécanismes HSE. Nous concentrons ici nos efforts sur celles qui sont le résultat d'erreurs dans les spécifications matérielles et non dans une implémentation donnée.Plus précisément, nous nous intéressons aux cas particulier de l'usage légitime, par un attaquant, d'une fonctionnalité d'un composant matériel pour contourner les protections offertes par un second. Notre but est d'explorer des approches basées sur l'usage de méthodes formelles pour spécifier et vérifier des mécanismes HSE. La spécification de mécanismes HSE peut servir de point de départ pour la vérification des spécifications matérielles concernées, dans l'espoir de prévenir des attaques profitant de la composition d'un grand nombre de composants matériels. Elles peuvent ensuite être fournies aux développeurs logiciels, sous la forme d'une liste de prérequis que leurs produits doivent respecter s'ils désirent l'application d'une politique de sécurité clairement identifiée
In this thesis, we consider a class of security enforcement mechanisms we called Hardware-based Security Enforcement (HSE). In such mechanisms, some trusted software components rely on the underlying hardware architecture to constrain the execution of untrusted software components with respect to targeted security policies. For instance, an operating system which configures page tables to isolate userland applications implements a HSE mechanism. For a HSE mechanism to correctly enforce a targeted security policy, it requires both hardware and trusted software components to play their parts. During the past decades, several vulnerability disclosures have defeated HSE mechanisms. We focus on the vulnerabilities that are the result of errors at the specification level, rather than implementation errors. In some critical vulnerabilities, the attacker makes a legitimate use of one hardware component to circumvent the HSE mechanism provided by another one. For instance, cache poisoning attacks leverage inconsistencies between cache and DRAM’s access control mechanisms. We call this class of attacks, where an attacker leverages inconsistencies in hardware specifications, compositional attacks. Our goal is to explore approaches to specify and verify HSE mechanisms using formal methods that would benefit both hardware designers and software developers. Firstly, a formal specification of HSE mechanisms can be leveraged as a foundation for a systematic approach to verify hardware specifications, in the hope of uncovering potential compositional attacks ahead of time. Secondly, it provides unambiguous specifications to software developers, in the form of a list of requirements

APA, Harvard, Vancouver, ISO, and other styles

46

Gervais, Frédéric. "Combinaison de spécifications formelles pour la modélisation des systèmes d'information." Phd thesis, Conservatoire national des arts et metiers - CNAM, 2006. http://tel.archives-ouvertes.fr/tel-00121006.

Full text

Abstract:

L'objectif de cette thèse est de profiter des avantages de deux formes de modélisation complémentaires pour représenter de manière formelle les systèmes d'information (SI). Un SI est un système informatisé qui permet de rassembler les informations d'une organisation et qui fournit des opérations pour les manipuler. Les SI considérés sont développés autour de systèmes de gestion de bases de données (SGBD). Notre motivation est d'utiliser des notations et des techniques formelles pour les concevoir, contrairement aux méthodes actuelles qui sont au mieux semi-formelles. D'une part, EB3 est un langage formel basé sur les traces d'événements qui a été défini pour la spécification des SI. En particulier, EB3 met en avant le comportement dynamique du système. D'autre part, B est un langage formel basé sur les états qui se prête bien à la spécification des propriétés statiques des SI. Nous avons défini une nouvelle approche, appelée EB4, qui bénéficie à la fois des avantages d'EB3 et B. Dans un premier temps, les processus décrits en EB3 sont utilisés pour représenter et pour valider le comportement du système. Ensuite, la spécification est traduite en B pour spécifier et vérifier les principales propriétés statiques du SI. Enfin, nous avons défini des techniques de synthèse automatique de transactions BD relationnelles à partir du modèle de données d'EB3 pour compléter le cycle de développement du SI.

APA, Harvard, Vancouver, ISO, and other styles

47

Hachicha, Rim. "Modélisation et analyse de la flexibilité dans les systèmes workflow." Paris, CNAM, 2007. http://www.theses.fr/2007CNAM0565.

Full text

Abstract:

Cette thèse est consacrée à la modélisation formelle et la gestion des systèmes workflows. Nous nous intéressons à apporter une solution à l'un des principaux problèmes des systèmes workflows est celui de la flexibilité : les modèles aussi bien que les systèmes actuels ne sont pas suffisamment flexibles et adaptables. Dans ce but, nous proposons un modèle de tâches et d'acteurs précisant les relations formelles entre les tâches workflow et les acteurs et permettant une assignation flexible des acteurs ux activités workflow. L'allocation des tâches workflows est fondée sur le concept de distance acteur/tâche et sur le processus de formation de coalitions d'agents. Le modèle permet de vérifier l'interchangeabilité des acteurs et la cohérence des tâches workflows suite à l'évolution de l'environnement. Nous proposons une architecture orientée agent distribuée intégrant le modèle formel et permettant de réaliser les fonctionnalités requises par les systèmes workflows. Cette architecture est capable de s'adapter de façon réactive aux changements tout en assurant la réutilisabilité du système Workflow. Nous avons implémenté le modèle sur la plate forme JADE en utilisant le système expert JESS et nous l'avons validé sur une réelle application
This thesis is devoted to formal modeling and management of workflow system. We are interested to bring a solution to the one of the principal problems of workflow systems is that of flexibility : the models as well as the current systems are not sufficiently flexible and adaptable. For these requirements, we propose a task model and actor model specifying the formal relations between workflow tasks and actors and allowing a flexible assignment of actors to workflow activities. The workflow task allocation is based on the concept of actor/task distance and agent coalition formation process. The model allows checking the interchangeability of the actors and the coherence of the workflows tasks following the evolution of the environment. We propose a distributed agent architecture integrating the formal model and permitting to carry out the functionalities required by the workflow system. This architecture is adaptable, reactive and ensures the reusability of the workflow system. We implemented the proposed model on JADE agent platform using expert system JESS and we validated our model on a real application

APA, Harvard, Vancouver, ISO, and other styles

48

Jaeger, Éric. "Study of the benefits of using deductive formal methods for secure developments." Paris 6, 2010. http://www.theses.fr/2010PA066048.

Full text

Abstract:

La mise en oeuvre des méthodes formelles déductives lors du développement de systèmes permet d'obtenir des garanties mathématiques quant à leur validité. Pour cette raison, leur utilisation est recommandée ou exigée par certains standards relatifs à la sûreté de fonctionnement ou la sécurité. Il reste cependant légitime de s'interroger sur la portée exacte des bénéfices. Certains aspects d'un système peuvent échapper à la formalisation, et il n'est pas toujours facile d'identifier ces limitations ou leurs conséquences. De même, si la validité d'une preuve est difficilement contestable, son utilisation pour justifier d'une confiance réelle dans le système physique n'est pas toujours admise. De telles questions sont particulièrement pertinentes dans le domaine de la sécurité, lorsque les systèmes font l'objet d'attaques de la part d'agents intelligents ; par rapport à la sûreté, il y a un changement radical de point de vue, qui justifie de s'interroger quant à l'application de principes ou de pratiques bien connus. Nous identifions les bénéfices et évaluons la confiance résultant de l'application des méthodes formelles déductives lors de développements de systèmes de sécurité. Cette analyse aborde les éventuelles difficultés, déviations ou problèmes qui peuvent être rencontrés, et les illustre par des exemples. Elle comporte également une étude détaillée du concept de raffinement, et présente un plongement profond visant à valider la logique de la méthode B; ce plongement conduit par ailleurs à l'étude des représentations à la de Bruijn.

APA, Harvard, Vancouver, ISO, and other styles

49

Foughali, Mohammed. "Vérification Formelle des Modules Fonctionnels de Systèmes Robotiques et Autonomes." Thesis, Toulouse, INSA, 2018. http://www.theses.fr/2018ISAT0033.

Full text

Abstract:

Les systèmes robotiques et autonomes ne cessent d’évoluer et deviennent de plus en plus impliqués dans les missions à coût considérable et/ou dans les milieux humains. Par conséquent, les simulations et campagnes de tests ne sont plus adaptées à la problématique de sûreté et fiabilité des systèmes robotiques et autonomes compte tenu (i) du caractère sérieux des défaillances éventuelles dans les contextes susmentionnés (un dommage à un robot très coûteux ou plus dramatiquement une atteinte aux vies humaines) et (ii) de la nature non exhaustive de ces techniques (les tests et simulations peuvent toujours passer à côté d’un scénario d’exécution catastrophique.Les méthodes formelles, quant à elles, peinent à s’imposer dans le domaine de la robotique autonome, notamment au niveau fonctionnel des robots, i.e. les composants logiciels interagissant directement avec les capteurs et les actionneurs. Elle est due à plusieurs facteurs. D’abord, les composants fonctionnels reflètent un degré de complexité conséquent, ce qui mène souvent à une explosion combinatoire de l’espace d’états atteignables (comme l’exploration se veut exhaustive). En outre, les composants fonctionnels sont décrits à travers des languages et frameworks informels (ROS, GenoM, etc.). Leurs spécifications doivent alors être traduites en des modèles formels avant de pouvoir y appliquer les méthodes formelles associées. Ceci est souvent pénible, lent, exposé à des erreurs, et non automatique, ce qui implique un investissement dans le temps aux limites de la rentabilité. Nous proposons, dans cette thèse, de connecter GenoM3, un framework de développement et déploiement de composants fonctionnels robotiques, à des langages formels et leurs outils de vérification respectifs. Cette connexion se veut automatique: nous développons des templates en mesure de traduire n’importe quelle spécification de GenoM3 en langages formels. Ceci passe par une formalisation de GenoM3: une sémantique formelle opérationnelle est donnée au langage. Une traduction à partir de cette sémantique est réalisée vers des langages formels et prouvée correcte par bisimulation. Nous comparons de différents langages cibles, formalismes et techniques et tirerons les conclusions de cette comparaison. La modélisation se veut aussi, et surtout, efficace. Un modèle correct n’est pas forcément utile. En effet, le passage à l’échelle est particulièrement important.Cette thèse porte donc sur l'applicabilité des méthodes formelles aux compo-sants fonctionnels des systèmes robotiques et autonomes. Le but est d'aller vers des robots autonomes plus sûrs avec un comportement plus connu et prévisible. Cela passe par la mise en place d'un mécanisme de génération automatique de modèles formels à partir de modules fonctionnels de sys-tèmes robotiques et autonomes. Les langages et outils cibles sont Fiacre/TINA et UPPAAL (model checking), UPPAAL-SMC (statistical model checking), BIP/RTD-Finder (SAT solving), et BIP/Engine (enforcement de propriétés en ligne). Les modèles générés sont exploités pour vérifier des propriétés quali-tatives ou temps-réel, souvent critiques pour les systèmes robotiques et auto-nomes considérés. Parmi ces propriétés, on peut citer, à titre d'exemple, l'ordonnançabilité des tâches périodiques, la réactivité des tâches spora-diques, l'absence d’interblocages, la vivacité conditionnée (un évènement tou-jours finit par suivre un autre), la vivacité conditionnée bornée (un évène-ment toujours suit un autre dans un intervalle de temps borné), l'accessibilité (des états “indésirables” ne sont jamais atteints), etc.La thèse propose éga-lement une analyse du feedback expérimental afin de guider les ingénieurs à exploiter ces méthodes et techniques de vérification efficacement sur les mo-dèles automatiquement générés
The goal of this thesis is to add to the efforts toward the long-sought objective of secure and safe robots with predictable and a priori known behavior. For the reasons given above, formal methods are used to model and verify crucial properties, with a focus on the functional level of robotic systems. The approach relies on automatic generation of formal models targeting several frameworks. For this, we give operational semantics to a robotic framework, then several mathematically proven translations are derived from such semantics. These translations are then automatized so any robotic functional layer specification can be translated automatically and promptly to various frameworks/languages. Thus, we provide a mathematically correct mapping from functional components to verifiable models. The obtained models are used to formulate and verify crucial properties (see examples above) on real-world complex robotic and autonomous systems. This thesis provides also a valuable feedback on the applicability of formal frameworks on real-world, complex systems and experience-based guidelines on the efficient use of formal-model automatic generators. In this context, efficiency relates to, for instance, how to use the different model checking tools optimally depending on the properties to verify, what to do when the models do not scale with model checking (e.g. the advantages and drawbacks of statistical model checking and runtime verification and when to use the former or the latter depending on the type of properties and the order of magnitude of timing constraints)

APA, Harvard, Vancouver, ISO, and other styles

50

Ponsini, Olivier. "Des programmes impératifs vers la logique équationnelle pour la vérification." Phd thesis, Université de Nice Sophia-Antipolis, 2005. http://tel.archives-ouvertes.fr/tel-00090688.

Full text

Abstract:

Nous nous sommes intéressé à la logique équationnelle en tant que support de la vérification des programmes impératifs. Notre approche vise le double objectif d'automatiser la vérification des propriétés de programmes et de proposer un formalisme pour raisonner sur les programmes adapté aux acteurs du développement des logiciels. Précisément, les travaux de cette thèse portent sur la traduction automatique des programmes impératifs vers la logique équationnelle. Nous avons considéré deux classes de programmes. Dans la première, la seule instruction avec effet de bord du langage est l'affectation. Nous présentons l'algorithme de traduction d'un programme en un ensemble d'équations sous la forme d'un système de réécriture définissant la sémantique du langage. Nous montrons la convergence du système de réécriture à l'aide d'un démonstrateur de théorèmes. Pour la seconde classe, nous ajoutons au langage appel par référence et listes mutables. Ces deux mécanismes introduisent la possibilité de manipuler des alias dans les programmes. Nous énonçons des restrictions sur l'utilisation des alias moyennant lesquelles nous proposons un algorithme pour la traduction en équations des programmes de cette seconde classe. La définition équationnelle obtenue ne s'appuie pas sur un modèle de la mémoire. Les équations produites par la traduction d'un programme peuvent alors être utilisées dans des systèmes de preuve afin de vérifier des propriétés du programme, elles-mêmes exprimées par des équations. Nous validons notre approche par une implantation des algorithmes et par la preuve de propriétés de programmes non triviales à l'aide des équations produites par notre méthode.

APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic 'Sécurité des systèmes – Méthodes formelles (informatique)'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles