Dissertations / Theses: 'Logiciel – Mesures de sûreté'

1

Duc, Guillaume. "Support matériel, logiciel et cryptographique pour une éxécution sécurisée de processus." Télécom Bretagne, 2007. http://www.theses.fr/2007TELB0041.

Full text

Abstract:

La majorité des solutions apportées aux problèmes de sécurité informatique (algorithmes, protocoles, systèmes d'exploitation sécurisés, applications) s'exécute sur des architectures matérielles non sécurisées et pouvant donc être vulnérables à des attaques physiques (espionnage du bus, modification de la mémoire, etc. ) ou logicielles (système d'exploitation corrompu). Des architectures sécurisées, permettant de garantir la confidentialité et la bonne exécution de programmes contre de telles attaques, sont proposées depuis quelques années. Après avoir présenté quelques bases cryptographiques ainsi qu'un comparatif des principales architectures sécurisées proposées dans la littérature, nous présenterons l'architecture sécurisée CryptoPage. Cette architecture garantit la confidentialité du code et des données des applications ainsi que leur bonne exécution contre des attaques matérielles et logicielles. Elle inclut également un mécanisme permettant de réduire les fuites d'informations via le bus d'adresse, tout en conservant des performances raisonnables. Nous étudierons également comment déléguer certaines opérations de sécurité de l'architecture CryptoPage à un système d'exploitation qui n'est pas digne de confiance, afin de permettre plus de flexibilité, sans pour autant compromettre la sécurité de l'ensemble. Enfin, d'autres mécanismes importants pour le bon fonctionnement de l'architecture CryptoPage sont traités : identification des processus chiffrés, attestation des résultats, gestion des signaux logiciels, gestion des processus légers, gestion des communications inter-processus
The majority of the solutions to the issue of computer security (algorithms, protocols, secure operating systems, applications) are running on insecure hardware architectures that may be vulnerable to physical (bus spying, modification of the memory content, etc. ) or logical (malicious operating system) attacks. Several secure architectures, which are able to protect the confidentiality and the correct execution of programs against such attacks, have been proposed for several years. After the presentation of some cryptographic bases and a review of the main secure architectures proposed in the litterature, we will present the secure architecture CryptoPage. This architecture guarantees the confidentiality of the code and the data of applications and the correct execution against hardware or software attacks. In addition, it also includes a mechanism to reduce the information leakage on the address bus, while keeping reasonable performances. We will also study how to delegate some security operations of the architecture to an untrusted operating system in order to get more flexibility but without compromising the security of thearchitecture. Finally, some other important mechanism are studied: encrypted processid entification, attestations of the results, management of software signals, management of the threads, inter-process communication

APA, Harvard, Vancouver, ISO, and other styles

2

Aussibal, Julien. "Rsids : un IDS distribué basé sur le framework CVSS." Pau, 2009. http://www.theses.fr/2009PAUU3044.

Full text

Abstract:

La détection d'intrusion est une méthode qui permet de garantir la notion de disponibilité dans les systèmes et réseaux informatiques. Cette disponibilité est généralement mise à mal par différentes anomalies. Ces anomalies peuvent être provoqués soit de manière légitime suite a des opérations involontaires intervenant sur ces systèmes (rupture de lien, embouteillages,. . . ), soit de manière illégitimes avec des opérations malveillantes ayant pour but de nuire à la disponibilité de ces systèmes. La mise en oeuvre d'outils recherchant ces différentes anomalies, que sont les IDS (Intrusion Dectetion System), contribuent à détecter au plus tôt ces anomalies et à les bloquer. Cette thèse nous a permis de mettre en place une nouvelle plateforme de génération d'anomalies légitimes et illégitimes. Ce travail a été réalisé dans le cadre du projet METROSEC. Cette plateforme nous a permis d'obtenir différentes captures de trafics contenant ces anomalies. Les différentes anomalies illégitimes ont été réalisées avec des outils classiques de Dénis de Service qui sont TFN2k ou encore Trinoo. Des anomalies légitimes ont aussi été réalisées sous la forme de phénomène de foules subites. L'ensemble de ces captures réelles de trafic ont été utilisées dans le cadre d'autres recherches sur la détection d'intrusion pour l'évaluation de nouvelles méthodes de détection. Dans un second temps, la mise en oeuvre d'un nouvel outil de détection nous a semblé nécessaire afin d'améliorer la qualité de détection de ces anomalies. Ce nouvel IDS distribué, appelé RSIDS (Risk Scored Intrusion Detection System), permettra de récupérer les résultats d'une multitude de sondes hétérogènes. L'utilisation de ses sondes va permettre de supprimer les risques de fausses alertes. En effet une sonde n'est pas capable de détecter l'ensemble des anomalies pouvant arriver sur un système ou un réseau. Chacune des remontées d'alertes fournies par ses sondes sera évaluée en fonction de son degré de dangerosité. Cette évaluation de la dangerosité s'appuie sur le framework CVSS (Common Vulnerability Scoring System)
Intrusion detection is a method that ensures the availability concept in systems and computer networks. This availability is generally undermined by various anomalies. These anomalies can be caused either legitimately unintended result has operations working on these systems (broken link, traffic, or. . . ), so illegitimate with malicious operations designed to undermine the availability of these systems. The implementation of these various anomalies detection tools, such as IDS (Intrusion Detection System), contribute to early identification of these anomalies and to block them. This thesis has enabled us to develop a new generation platform to generate legitimate and illegitimate anomalies. This work was carried out under the project METROSEC. This platform has enabled us to obtain various traffic captures containing these anomalies. The various illegimitate anomalies were performed with classic tools to make Denial of Service like TFN2k or Trinoo. Legitimate Anormalies were also conducted with flash crowd phenomenon. All these catch real traffic were used in further research on intrusion detection for the evaluation of new methods of detection. In a second part, the implementation of a new detection tool seems necessary to improve the quality of detection of these anomalies. This new distributed IDS, called RSIDS (Risk Scored Intrusion Detection System), will retrieve the results of a multitude of heterogeneous probes. The use of probes will remove the risk of false alarms. Indeed, a probe is not able to detect all anomalies that occur on a system or network. Each alert provided by its probes will be evaluated according to their degree of dangerousness. The assessment of dangerousness based on the framework CVSS (Common Vulnerability Scoring System)

APA, Harvard, Vancouver, ISO, and other styles

3

Limane, Tahar. "Conception et réalisation d'un outil de surveillance, temps réel, d'espaces de débattements de robots." Lyon, INSA, 1991. http://www.theses.fr/1991ISAL0093.

Full text

Abstract:

Les travaux présentés dans ce mémoire concernent la conception et La réalisation d'un outil de surveillance en temps réel, de débattements de robots industriels dans le but d'améliorer La sécurité des opérateurs et des machines. Ce mémoire présente d'abord une analyse globale des conditions de risques en Robotique et la mise en évidence des différents facteurs de dépendance Liés à la spécification d'un système de protection. Les différents moyens et dispositifs de protection ainsi que les paramètres caractérisant l'arrêt d'un robot sont ensuite présentés. Les contraintes liées à la réalisation d'un nouveau système de sécurité, élaborant des contrôles d'appartenance à des espaces de surveillance en intégrant la dynamique du robot surveillé sont étudiées. Sont exposées ensuite, les spécifications fonctionnelles et structurelles ainsi que les modèles conceptuels du système de protection à réaliser. Des approches méthodologiques issues du domaine du Génie Logiciel sont utilisées, permettant ainsi de valider l'ensemble du cycle de vie du produit développe et d'en garantir le niveau de qualité et de fiabilité recherché. Ces travaux sont concrétisés par la réalisation de l'outil SAFE (Surveillance d'Ateliers Flexibles et de leur Environnement). Enfin, des perspectives d'intégration de fonctionnalités complémentaires sont proposées, concernant notamment La gestion de la commande et des espaces de surveillance autour des sites robotisés sécurisés
The study presented in this report addresses the problems of designing and implementing a real-time control system of robots movements. The top-Level objective of the study is to enhance the safety of both the human operators and the machines. We begin with a global analysis of risk conditions in Robotics and general relationship statements between the different factors which have to be taken into account when specifying protection systems. We survey the different methods as well as the different equipments used in protection systems against robots possibly undue clearances. Constraints specification of a mean safety system able to control dynamically the robot's containment within the limits allowed or forbidden spaces are studied. Afterwards, we present the functional and structural specifications a well as the conceptual models of the protection systems to be implemented. Methodological approaches of software engineering type are proposed in view of validating the overall system life-cycle, its quality and its reliability. This study results the elaboration of the software tool SAFE (Surveillance d'Ateliers Flexibles et de Leur environnement) which is described in the report. Further developments of SAFE are suggested concerning, particularly, two inter-related functionalities of safety control : - first, the robot command program itself, - second, the dynamic re-specification of safety space when any change arises in the robot's task

APA, Harvard, Vancouver, ISO, and other styles

4

Abdelnur, Humberto Jorge. "Gestion de vulnérabilités voix sur IP." Thesis, Nancy 1, 2009. http://www.theses.fr/2009NAN10005/document.

Full text

Abstract:

Les solutions voix sur IP (VoIP) sont actuellement en plein essor et gagnent tous le jours de nouveaux marché en raison de leur faible coût et d'une palette de services riche. Comme la voix sur IP transite par l'Internet ou utilise ses protocoles, elle devient la cible de multiples attaques qui peuvent mettre son usage en péril. Parmis les menaces les plus dangereuses on trouve les bugs et les failles dans les implantations logicielles des équipements qui participent à la livraison de ces services. Cette thése comprend trois contributions à l'amélioration de la sécurité des logiciels. La première est une architecture d'audit de sécurité pour les services VoIP intégrant découverte, gestion des données et attaques à des fins de test. La seconde contribution consiste en la livraison d'une approche autonome de discrimination de signatures de messages permettant l'automatisation de la fonction de fingerprinting passif utilisée pour identifier de façon unique et non ambigüe la source d'un message. La troisième contribution porte sur la détection dynamique de vulnérabilités dans des états avancés d'une interaction protocolaire avec un équipement cible. L'expérience acquise dans la recherche de vulnérabilités dans le monde de la VoIP avec nos algorithmes est également partagée dans cette thèse
VoIP networks are in a major deployment phase and are becoming widely accepted due to their extended functionality and cost efficiency. Meanwhile, as VoIP traffic is transported over the Internet, it is the target of a range of attacks that can jeopardize its proper functionality. Assuring its security becomes crucial. Among the most dangerous threats to VoIP, failures and bugs in the software implementation will continue rank high on the list of vulnerabilities. This thesis provides three contributions towards improving software security. The first is a VoIP specific security assessment framework integrated with discovery actions, data management and security attacks allowing to perform VoIP specific assessment tests. The second contribution consists in an automated approach able to discriminate message signatures and build flexible and efficient passive fingerprinting systems able to identify the source entity of messages in the network. The third contribution addresses the issue of detecting vulnerabilities using a stateful fuzzer. It provides an automated attack approach capable to track the state context of a target device and we share essential practical experience gathered over a two years period in searching for vulnerabilities in the VoIP space

APA, Harvard, Vancouver, ISO, and other styles

5

Galissant, Pierre. "Contributions to white-box cryptography : models and algebraic constructions." Electronic Thesis or Diss., université Paris-Saclay, 2023. http://www.theses.fr/2023UPASG099.

Full text

Abstract:

Du fait de la démocratisation detechnologies telles que le paiement par mobile oul'essor des technologies basées sur la blockchain, lesbesoins d'implémentations sécurisées dans le modèleboîte blanche d'algorithmes standardisés sont de plusen plus conséquents dans l'industrie. Malgré cesbesoins, très peu de nouveaux designs sont proposésdans la littérature. Pour ne pas avoir à utiliser desimplémentations aux designs non publics, denouvelles techniques d'implémentations doivent êtreproposées et étudiées.Ce manuscrit commence par un guide pour lacryptographie boîte blanche. Son but est de réviser,préciser ou corriger les modèles boîte blanche, lesnotions de sécurité et les constructions qui ontémergé dans l'état-de-l'art depuis l'introduction duconcept. Notamment, nous clarifions les modèles'Remote-Access' et 'Hardware-Module' et lescontextualisons dans la littérature cryptographique ausens large.Nous explorons ensuite les implémentations boîteblanche de l'AES en synthétisant tout d'abord lesimplémentations connues et leurs failles. Nousproposons ensuite une nouvelle implémentation del'AES pour laquelle nous proposons une analyse desécurité et un challenge. La dernière partie de cettethèse est consacrée à l'étude de l'implémentationdes primitives à base de cryptographie multivariée.Après une introduction succincte à la cryptographiemultivariée, nous motivons l'utilisation de lacryptographie multivariée dans le modèle boîteblanche. Nous proposons ensuite la premièreimplémentation boîte blanche de la famille designature HFE, pour laquelle nous proposons uneanalyse de sécurité et un challenge. Enfin, pourproposer d'autres idées basées sur la cryptographiemultivariée, nous proposons un chiffrement à flotincompressible basé sur QUAD
Due to the democratization of technologiessuch as mobile payment or the soaring of blockchaintechnologies, there is a growing need for secureimplementations of standardized algorithms in thewhite-box model. In spite of this, there are too fewsecure designs published in the literature. To avoidrelying on hidden design implementations to provideany security in the white-box model, moreimplementations designs and techniques have to beexplored.This thesis begins with a guide to white-boxcryptography. Its goal is to revise, precise or correctwhite-box models, security notions andconstructions that have emerged in the state of theart since the introduction of the concept. We notablyclarify the Remote-Access White-Box model and theHardware Module White-Box and contextualize themin the general cryptographic literature.We then explore white-box implementations of theAES by first synthesizing the knownimplementations techniques and their flaws, andthen proposing a new solution based on polynomialrepresentations, for which we propose a securityanalysis and a challenge implementation. The lastpart of this thesis focuses on the implementation ofmultivariate cryptographic primitives in thewhite-box model. After introducing succinctlymultivariate cryptography, we motivate the studyof this branch of public key cryptography in thewhite-box context. We propose the firstimplementation technique of the HFE family ofsignature algorithms, for which we propose anextensive security analysis and a challengeimplementation. Finally, to propose otherperspectives on multivariate white-boxcryptography, we also propose an incompressiblestream cipher adapted from QUAD

APA, Harvard, Vancouver, ISO, and other styles

6

Le, Blond Stevens. "Est-ce que la vie privée existe toujours (dans les réseaux pair-à-pair) ?" Nice, 2011. http://www.theses.fr/2011NICE4018.

Full text

Abstract:

Avec le paradigme pair-à-pair (P2P), chaque utilisateur partage ses ressources (e. G. Stockage et bande passante) afin de fournir un service. Parce que le paradigme P2P passe à l'échelle, il est à ce jour utilisé par certains des systèmes les plus populaires de l'Internet. Cependant, les systèmes P2P tournant sur l'Internet peuvent permettre à un utilisateur malicieux d'associer l'adresse IP des participants avec d'autres informations personnelles, possiblement introduisant une faille majeure pour la protection de la vie privée. Afin d'évaluer la sévérité de cette menace, nous lançons des attaques contre la vie privée pour trois applications P2P: Une application pour le partage de fichiers (BitTorrent), une application temps réel (Skype), et une application anonymisante à faible latence (Tor). (a) En exploitant Skype, nous montrons qu'il est possible d'associer l'identité (e. G. Nom et ville) d'une personne avec son adresse IP. Nous redimensionnons cette attaque afin de traquer la mobilité et le comportement de téléchargement d'un grand nombre de personnes. (b) En exploitant BitTorrent, nous démontrons qu'un adversaire peut continuellement espionner l'ensemble des téléchargements effectués par la plupart des utilisateurs de l'Internet, à partir d'une seule machine. Nous montrons également qu'il est possible de déterminer l'adresse IP des utilisateurs injectant de nouveaux contenus et que les 100 utilisateurs les plus actifs injectent 1/3 de tous les contenus. (c) En utilisant Tor, nous montrons qu'il est possible de révéler l'adresse IP, ou de tracer, des utilisateurs supposés être anonymes et nous montrons que le design de Tor peut aussi être exploit pour tracer une quantité significative de trafic ``anonyme'' additionnel (non P2P). Nous concluons que les applications P2P constituent une faille majeure pour la protection de la vie privée et décrivons brièvement une architecture pouvant atténuer cette menace
With the Peer-to-peer (P2P) paradigm, each user shares some of his resources (e. G. , storage and bandwidth) to provide a service. Because a P2P system scales with its number of users, the P2P paradigm is today used by some of the most popular Internet systems. However, P2P systems on the Internet may allow a malicious user to correlate the IP address of other participants with some personal information, possibly introducing a major privacy invasion. To evaluate the severity of this threat, we run privacy attacks against three popular P2P applications: a filesharing application (BitTorrent), a real-time application (Skype), and a low-latency anonymity application (Tor). (a) Exploiting Skype, we show that one can associate the identity (e. G. , birth name and city of residence) of a person with his IP address. We then scale this attack to track the mobility and filesharing behavior of a large number of identified-targeted users. (b) Exploiting BitTorrent, we demonstrate that an adversary can continuously spy on the download of most of the BitTorrent users of the Internet, from a single machine. We also show that it is possible to determine the IP address of the users who inject new content and that the top100 of these users inject 1/3 of all content. (c) Exploiting Tor, we show that it is possible to reveal the IP address of, or trace, supposedly anonymous users and show that Tor's design can also be exploited to trace a significant amount of non-P2P ``anonymous'' traffic. We conclude that P2P applications enable a major invasion in users' privacy and sketch an architecture that could alleviate this threat

APA, Harvard, Vancouver, ISO, and other styles

7

Hodique, Yann. "Sûreté et optimisation par les systèmes de types en contexte ouvert et contraint." Lille 1, 2007. https://pepite-depot.univ-lille.fr/LIBRE/Th_Num/2007/50376-2007-15.pdf.

Full text

Abstract:

La généralisation des équipements électroniques embarqués provoque des besoins croissants d'adaptabilité en ce qui concerne les systèmes logiciels qui doivent y être déployés. Par ailleurs, les faibles ressources dont les équipements disposent, ainsi que leur propension à se trouver en milieu non sécurisé, imposent des contraintes de performance et de fiabilité à ces mêmes systèmes. Le cadre de cette thèse est l'étude de la conception et de l'exploitation de systèmes de types afin d'adapter au mieux les systèmes logiciels à ces différentes contraintes. À travers la définition de systèmes de types adaptés, nous intervenons dans la chaîne de production logicielle de façon à faciliter le respect des contraintes spécifiques du domaine embarqué. Les contributions scientifiques de ce travail trouvent leur place dans deux périodes particulières du cycle de vie du logiciel. La première période est celle de la conception, durant laquelle nous proposons l'emploi d'un système de types présentant la propriété d'être suffisamment souple pour permettre l'expression de concepts de haut niveau sans crainte d'une dégradation de performance. La seconde période est celle du déploiement qui, par sa nature « définitive », nous permet d'avoir recours au calcul de types plus spécifiquement orientés vers l'interprétation spécialisée des programmes, à des fins d'optimisation notamment.

APA, Harvard, Vancouver, ISO, and other styles

8

Trouessin, Gilles. "Traitements fiables de données confidentielles par fragmentation-redondance-dissémination." Toulouse 3, 1991. http://www.theses.fr/1991TOU30260.

Full text

Abstract:

Ce memoire presente des travaux et resultats, theoriques mais aussi appliques, concernant trois approches permettant de resoudre le probleme des traitements fiables de donnees confidentielles: protection-replication, chiffrement-replication et fragmentation-redondance-dissemination. Ces approches visent a tolerer a la fois des fautes accidentelles et des fautes intentionnelles. L'amelioration de la fiabilite et la preservation de la confidentialite reposent en general sur des techniques antagonistes et sont d'ordinaire abordees separement. Differentes solutions sont presentees et comparees selon un ensemble de criteres relatifs a la surete de fonctionnement, a l'ouverture et aux performances; l'une d'elles, la fragmentation-dissemination et replication, qui semble la plus prometteuse, est approfondie. Les caracteristiques de cette solution sont presentees, en insistant sur les analogies qui peuvent etre constatees avec la parallelisation d'algorithmes. Trois classes de techniques de fragmentation sont definies (tranches de bits, orientee-structure, orientee-parallelisme) et deux modeles d'execution fragmentee (client/serveurs, oriente-objets) sont proposes. Une technique d'evaluation quantitative de la preservation de la confidentialite, issue de la theorie de l'information et reposant sur des mesures d'entropie, est appliquee a la fragmentation par tranches de bits. Des mesures generales d'evaluation comparative sont ainsi obtenues. L'analogie entre fragmentation et parallelisation est etudiees en detail sur des algorithmes paralleles de resolution de systemes lineaires. Une demarche d'evaluation qualitative, qui offre des analogies avec la technique precedente pour ce qui est des types d'information a observer et des niveaux d'appreciation de la preservation de la confidentialite, est appliquee a la fragmentation orientee-parallelisme. Ces deux etudes confirment l'interet de la fragmentation-redondance-dissemination pour tolerer de facon unifiee les fautes accidentelles et les intrusions

APA, Harvard, Vancouver, ISO, and other styles

9

Jacob, Grégoire. "Malware behavioral models : bridging abstract and operational virology." Rennes 1, 2009. http://www.theses.fr/2009REN1S204.

Full text

Abstract:

This thesis is devoted to the modeling of malicious behaviors inside malevolent codes, commonly called malware. The thesis work follows two directions, one operational, one theoretical. The objective is to eventually combine these two approaches in order to elaborate detection methods covering most of existing malware, while offering formal security guarantees against appearing ones. The operational approach introduces an abstract behavioral language, independent from implementation. The language itself relies on the attribute-grammar formalism, capable of expressing the behavior semantics. Within the language, several behavior descriptions are specified in order to build a multi-layered detection method based on parsing. Its deployment has shown satisfying results in terms of coverage. On the basis of the same language, some techniques of behavioral mutation have been formalized using compilation techniques. These mutations have proved themselves interesting tools for the evaluation of antiviral products. The theoretical approach introduces a formal viral model, no longer based on functional paradigms, but on process algebras. This new model enables the description of self-replication as well as other more complex behaviors based on interactions. It supports the redemonstration of fundamental results such as the detection undecidability or the prevention by isolation. Moreover, the model supports the formalization of several existing techniques of behavioral detection, thus allowing the formal evaluation of their resilience
Cette thèse s'intéresse à la modélisation des comportements malicieux au sein des codes malveillants, communément appelés malwares. Les travaux de thèse s'articulent selon deux directions, l'une opérationnelle, l'autre théorique. L'objectif à terme est de combiner ces deux approches afin d'élaborer des méthodes de détection comportementales couvrant la majorité des malwares existants, tout en offrant des garanties formelles de sécurité contre ceux susceptibles d'apparaître. L'approche opérationnelle introduit un langage comportemental abstrait, décorrélé de l'implémentation. Le langage en lui-même repose sur le formalisme des grammaires attribuées permettant d'exprimer la sémantique des comportements. A l'intérieur du langage, plusieurs descriptions de comportements malicieux sont spécifiées afin de construire une méthode de détection multicouche basée sur le parsing. Sur la base de ce même langage, des techniques de mutation comportementale sont également formalisées à l'aide de techniques de compilation. Ces mutations se révèlent un outil intéressant pour l'évaluation de produits antivirus. L'approche théorique introduit un nouveau modèle viral formel, non plus basé sur les paradigmes fonctionnels, mais sur les algèbres de processus. Ce nouveau modèle permet la description de l'auto-réplication ainsi que d'autres comportements plus complexes, basés sur les interactions. Il supporte la redémonstration de résultats fondamentaux tels que l'indécidabilité de la détection et la prévention par isolation. En outre, le modèle supporte la formalisation de plusieurs techniques existantes de détection comportementale, permettant ainsi d'évaluer formellement leur résistance

APA, Harvard, Vancouver, ISO, and other styles

10

Boisseau, Alexandre. "Abstractions pour la vérification de propriétés de sécurité de protocoles cryptographiques." Cachan, Ecole normale supérieure, 2003. https://theses.hal.science/tel-01199555.

Full text

Abstract:

Depuis le développement de l'utilisation des réseaux informatiques et de l'informatisation des communications, il est apparu pour le public un besoin de sécuriser les communications électroniques. Les considérations cryptographiques constituent un élément de réponse au problème de la sécurité des communications et les protocoles cryptographiques décrivent comment intégrer la cryptographie à l'intérieur de communications réelles. Cependant, même dans le cas où les algorithmes de chiffrement sont supposés robustes, les protocoles peuvent présenter des failles de conception exploitables (failles logiques), entrainant un besoin de vérification formelle. Dans cette thèse, nous utilisons des techniques d'abstraction afin de prouver formellement divers types de propriétés. Les propriétés de secret et d'authentification, les propriétés de type équité et des propriétés de type anonymat
Since the development of computer networks and electronic communications, it becomes important for the public to use secure electronic communications. Cryptographic considerations are part of the answer to the problem and cryptographic protocols describe how to integrate cryptography in actual communications. However, even if the encryption algorithms are robust, there can still remain some attacks due to logical flaw in protocols and formal verification can be used to avoid such flaws. In this thesis, we use abstraction techniques to formally prove various types of properties : secrecy and authentication properties, fairness properties and anonymity

APA, Harvard, Vancouver, ISO, and other styles

11

Carré, Jean-Loup. "Static analysis of embedded multithreaded programs." Cachan, Ecole normale supérieure, 2010. https://theses.hal.science/tel-01199739.

Full text

Abstract:

Cette thèse présente un algorithme d'analyse statique pour des programmes parallèles. Il généralise des techniques d'interprétation abstraite utilisée dans le cas de programmes sans parallélisme et permet de détecter des erreurs d'exécution, exempli gratia, les déréférencements de pointeur invalide, les débordements de tableaux, les débordements d'entiers. Nous avons implémenté cet algorithme. Il analyse un code industriel de taille conséquente (100 000 lignes de code) en quelques heures. Notre technique est modulaire, elle peut utiliser n'importe quel domaine abstrait créé pour le cas de programmes non-parallèles. En outre, sans change le calcul du point fixe, certains de nos domaines abstraits. Permettent la détection de data-races ou de deadlocks. Cette technique ne présuppose pas la consistance séquentielle (i. E. Ne présuppose pas que l'exécution d'un programme parallèle est l'entrelacement de l'exécution de sous-programmes) puisque, en pratique (les processeurs INTEL et SPARC, JAVA,. . . ) l'exécution des programmes n'est pas séquentiellement consistante. Exempli gratia notre technique fonctionne avec les modèles TSO (Total Store Ordering) et PSO (Partial Store Ordering)
This Phd thesis presents a static analysis algorithm for programs with threads. It generalizes abstract interpretation techniques used in the single-threaded case and allows to detect runtimes errors, e. G, invalid pointer dereferences, array overflows, integer overflows. We have implemented this algorithm. It analyzes a large industrial multithreaded code (100K LOC) in few hours. Our technique is modular, it uses any abtract domain designed for the single-threaded-case. Furthermore, without any change in the fixpoint computation, sorne abstract domains allow to detect data-races or deadlocks. This technique does not assume sequential consistency, since, in practice (INTEL and SPARC processors, JAVA,. . . ), program execution is not sequentially consistent. E. G, it works in TSO (Total Store ordering) or PSO (Partial Store Ordering) memory models

APA, Harvard, Vancouver, ISO, and other styles

12

Ismail, Leila. "Infrastructure système pour applications réparties à base d'agents mobiles." Grenoble INPG, 2000. http://www.theses.fr/2000INPG0072.

Full text

APA, Harvard, Vancouver, ISO, and other styles

13

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

14

Fioraldi, Andrea. "Fuzzing in the 2020s : novel approaches and solutions." Electronic Thesis or Diss., Sorbonne université, 2023. http://www.theses.fr/2023SORUS546.

Full text

Abstract:

Malgré les efforts considérables mis en œuvres en matière de fuzzing, la sécurité des logiciels informatiques reste menacée par des vulnérabilités insaisissables. Les coverage-guided fuzzers, qui se concentrent uniquement sur la couverture de code, ne parviennent généralement pas à découvrir des vulnérabilités spécifiques. La multiplication de divers outils de fuzzing a grandement divisé la communauté et a rendu difficile la combinaison de différentes techniques de fuzzing, l'évaluation précise des contributions et la comparaison efficace des différents outils. Pour remédier à cette situation, il est nécessaire de disposer d'un socle commun afin de garantir des évaluations précises et équitables. AFL, en raison de sa popularité, est souvent utilisé comme base lors de la création de nouveaux prototypes malgré le fait qu'il ne s'agisse pas d'une référence naïve et sa conception monolithique. D'autre part, les fuzzers personnalisés réécrits à partir de zéro ont tendance à réinventer la roue et utilisent souvent inneficacement la puissance des les systèmes multicœurs. Cette thèse relève ces défis en apportant plusieurs contributions: Un nouveau mécanisme de feedback appelé InvsCov est introduit, qui prend en compte les relations entre les variables du programme et la couverture du code. Il affine l'approximation de l'état du programme pour optimiser la détection de divers bugs. Une autre approche que nous introduisons explore les graphes de dépendance des données pour améliorer le fuzzing en récompensant la traversée de nouvelles arêtes du graphe de flux de données, ce qui a permis la découverte de nouvelles vulnérabilités manquées par la couverture standard efficacement. Nous présentons également une analyse approfondie des mécanismes internes d'AFL afin de mettre en lumière ses choix de conception et leur impact sur les performances du fuzzing. Enfin, pour remédier au problème de fragmentation cité précédemment, nous proposons un outil dédié au fuzzing modulaire et réutilisable: LibAFL. Les chercheurs peuvent étendre la pipeline de base du fuzzer, l'évaluation de nouvelles techniques techniques et la combinaison d'approches orthogonales. Une tentative de réécriture de AFLpp comme frontend de LibAFL a remporté le concours de fuzzing SBFT'23 dans le domaine de la recherche de bugs. Ces contributions font progresser le domaine du fuzzing, en abordant les défis de la sensibilité des mécanismes de feedback, de la diversité des bugs découverts, de la fragmentation des outils et de l'évaluation des fuzzers. Elles fournissent une base solide pour l'amélioration des techniques de fuzzing, permettant la détection d'une plus large gamme de bugs, et favorisant la collaboration et la standardisation au sein de la communauté
Security remains at risk due to elusive software vulnerabilities, even with extensive fuzzing efforts. Coverage-guided fuzzers, focusing solely on code coverage, often fall short in discovering specific vulnerabilities. The proliferation of diverse fuzzing tools has fragmented the field, making it challenging to combine different fuzzing techniques, assess contributions accurately, and compare tools effectively. To address this, standardized baselines are needed to ensure equitable evaluations. AFL, due to its popularity, is often extended to implement new prototypes despite not being a naive baseline and its monolithic design. On the other hand, custom fuzzers written from scratch tend to reinvent solutions and often lack scalability on multicore systems. This thesis addresses these challenges with several contributions: A new feedback mechanism called InvsCov is introduced, which considers program variable relationships and code coverage. It refines program state approximation for diverse bug detection. Another additional feedback we introduce explores data dependency graphs to enhance fuzzing by rewarding new dataflow edge traversal, effectively finding vulnerabilities missed by standard coverage. We also present a thorough analysis of AFL's internal mechanisms to shed light on its design choices and their impact on fuzzing performance. Finally, to address fragmentation, LibAFL is introduced as a modular and reusable fuzzing framework. Researchers can extend the core fuzzer pipeline, evaluation of compelling techniques, and combination of orthogonal approaches. An attempt to rewrite AFL++ as a frontend to LibAFL won the SBFT'23 fuzzing competition in the bug-finding track. These contributions advance the field of fuzz testing, addressing the challenges of sensitivity in feedback mechanisms, bug diversity, tool fragmentation, and fuzzers evaluation. They provide a foundation for improving fuzzing techniques, enabling the detection of a broader range of bugs, and fostering collaboration and standardization within the community

APA, Harvard, Vancouver, ISO, and other styles

15

Sadde, Gérald. "Sécurité logicielle des systèmes informatiques : aspects pénaux et civils." Montpellier 1, 2003. http://www.theses.fr/2003MON10019.

Full text

Abstract:

De l'instant de l'attaque logicielle contre le système, jusqu'aux conséquences macro-économiques induites, nous suivrons la propagation du dommage et ses implications juridiques en matière d'obligations et de responsabilité. Cela nous donnera tout d'abord l'occasion d'aborder l'aspect répressif de la sécurité au travers de la sanction pénale de l'acte. Mais tout autant nous nous intéresserons aux relations contractuelles qui vont naître de la prévention du dommage, au travers des mesures prises par la victime, le maître du système, pour protéger ses intérêts. Nous envisagerons les recours qui s'offrent non seulement à ce dernier mais aussi aux utilisateurs du système attaqué, qui subiront parfois un préjudice du fait d'une atteinte, à leurs biens, à la qualité d'un service, ou à leur vie privée. Enfin la sécurité informatique est à nos yeux un impératif d'ordre public et ce sont les dommages potentiels à l'économie dans son ensemble qui concluront donc cette étude.

APA, Harvard, Vancouver, ISO, and other styles

16

Pellegrino, Giancarlo. "Détection d'anomalies logiques dans les logiciels d'entreprise multi-partis à travers des tests de sécurité." Electronic Thesis or Diss., Paris, ENST, 2013. http://www.theses.fr/2013ENST0064.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

17

Paradinas, Pierre. "La Biocarte : intégration d'une carte à microprocesseur dans un réseau professionnel santé." Lille 1, 1988. http://www.theses.fr/1988LIL10100.

Full text

APA, Harvard, Vancouver, ISO, and other styles

18

Jolly, Germain. "Evaluation d’applications de paiement sur carte à puce." Caen, 2016. https://hal.archives-ouvertes.fr/tel-01419220.

Full text

Abstract:

Cette thèse traite des méthodes d'évaluation de haut niveau, proche des applications. Une méthode d'évaluation d'application sur cartes à puces, complémentaire aux méthodes existantes, a été définie durant de la thèse. Le but est de détecter les anomalies présentes sur cartes à puce (et plus précisément sur l'application de la carte à puce) et de fournir une documentation accrue sur cette erreur ainsi que les raisons déclencheurs de cette erreur. L'utilisateur de l'outil configure un ensemble de propriétés correspondant aux comportements attendus de l'application qu'il va vérifier. Afin de connaître la conformité du comportement de l'application carte vis à vis de la théorie (spécifications), la première étape est la génération de l'oracle, élément de référence lors d'une activité de vérification et validation. Nous nous sommes orientés vers une technique plus intelligente basée sur un algorithme génétique prenant en entrée un ensemble de logs de transaction qui permet de générer automatiquement un ensemble de propriétés (c'est à dire un ensemble de comportements locaux et attendus de l'application carte). La méthode de vérification est développée grâce au framework WSCT. Nous avons utilisé une applet JavaCard développée au laboratoire afin de tester la faisabilité de la méthode pour deux cas d'usages : lors de la phase de test, la méthodologie peut être utilisée en parallèle de la méthode utilisée par l'entreprise de certification et lors du développement de l'application, l'utilisation de cette méthodologie permet un guidage du développement, ce qui permet de l'utiliser dans le cadre de l'enseignement du développement JavaCard et de l'évaluation d'applications
This thesis deals with high-level evaluation of applications in smartcards. The proposed method combines observation of the communication and detection of violated properties. The goal is to detect anomalies on smart cards (and more precisely on its implementation) and provide a better documentation on this error and on the reasons that triggered this error. We can know on the fly if an application has an error of implementation. The user of the tool configures a set of properties corresponding to the expected behavior of the application. To ascertain compliance of the behavior of the card application with the theory (specifications), the first step is the generation of the oracle, reference used during verification and validation activity. We quickly directed to a smarter technique to target the most interesting behaviors to check for our study. We worked on a generation method based on a genetic algorithm taking as input a set of transaction logs to automatically generate a set of properties (i. E. A set of local and expected behaviors of the applications). The evaluation methodology is developed through the WSCT framework. Two plugins were created and used to communicate with the smart card application, but also to observe and detect an abnormality in the behavior of the application. We used a JavaCard applet developed in the laboratory to test the feasibility of the method for two use cases: during the test phase, the methodology can be used in parallel by the certification firm and during the development of an application, for example, allowing improving the teaching of the JavaCard development and the evaluation of application

APA, Harvard, Vancouver, ISO, and other styles

19

Lucas, Audrey. "Support logiciel robuste aux attaques passives et actives pour l'arithmétique de la cryptographie asymétrique sur des (très) petits coeurs de calcul." Thesis, Rennes 1, 2019. http://www.theses.fr/2019REN1S070.

Full text

Abstract:

Cette thèse porte sur le développement et l'évaluation de protections contrant simultanément des attaques par perturbation (FA) et des attaques par observation (SCA) dans le contexte de la cryptographie basée sur les courbes elliptiques (ECC). Deux protections ont été proposées pour la multiplication scalaire (SM), l'opération principale d'ECC. La première, nommée vérification de point (PV), permet une uniformisation de la SM grâce à une vérification de l'appartenance du point courant à la courbe. La SM ainsi obtenue est uniforme et donc résistante aux SPA mais aussi résistante à certaines FA. La seconde, nommée compteur d'itérations (IC), protège le scalaire contre certaines FA, tout en ayant un comportement uniforme et avec un très faible surcoût. Ces deux protections ont été implantées sur un microcontrôleur Cortex M0 pour les courbes de Weierstrass et de Montgomery, et ce pour différents types de coordonnées. Le surcoût de ces méthodes varie entre 48 % et 62 % dans le pire des cas (lorsque la PV est réalisée à chaque itération de la SM). Cela est moindre que celui des protections de bases habituelles contre les SCA. Un simulateur d'activité théorique au niveau arithmétique est également proposé. Il reproduit l'architecture d'un microcontrôleur 32 bits très simple. L'activité théorique est modélisée grâce à la variation du poids de Hamming des données manipulées lors de l'exécution. Grâce à ce simulateur, l'impact des opérandes sur l'activité des unités arithmétiques a pu être illustré. De plus, des attaques SPA et DPA furent réalisées pour évaluer les protections précédentes. Nos protections montrent une amélioration de la sécurité
This thesis deals with protection development and evaluation against fault attacks (FA) and side channel attacks (SCA) simultaneously. These protections have been developed for elliptic curves cryptography (ECC) and its main operation, the scalar multiplication (MS). Two protections have been proposed. The first is point verification (PV) checking that the current point is effectively on the curve, with a uniformization behavior. Thus, this new SM with PV is robust against some FAs and also SPA, since it is uniform. The second one is called counter iteration (IC). ICC protects the scalar against major FAs with a uniform behavior. Its overhead is very small. Our protections have been implemented on Cortex M0 microcontroller for Weiertrass and Montgomery curves and for different types of coordinates. The overhead is between 48 % and 62 %, in the worst case (when the PV is made at each SM iteration). This overhead is smaller than overhead of usual basic protections against SPA. A theorical activity simulator has also been developed. It reproduces the architecture of a simple 32-bit microcontroller. Theoric activity is modeled by the Hamming weigh variations of manipulated data during execution. Thanks to the simulator, the impact of operands is illustrated for arithmetic units. Moreover, SPA and DPA attacks were made for evaluating our protections. Our protections show some security improvements

APA, Harvard, Vancouver, ISO, and other styles

20

Cozzi, Emanuele. "Binary Analysis for Linux and IoT Malware." Electronic Thesis or Diss., Sorbonne université, 2020. http://www.theses.fr/2020SORUS197.

Full text

Abstract:

Au cours des deux dernières décennies, la communauté de la sécurité a lutté contre les programmes malveillants pour les systèmes d’exploitation basés sur Windows. Cependant, le nombre croissant de dispositifs embarqués interconnectés et la révolution de l’IoT modifient rapidement le paysage des logiciels malveillants. Les acteurs malveillants ne sont pas restés les bras croisés, mais ont rapidement réagi pour créer des “logiciels malveillants Linux”. Par cette thèse, nous naviguons dans le monde des logiciels malveillants basés sur Linux et mettons en évidence les problèmes que nous devons surmonter pour leur analyse correcte. Après une exploration systématique des défis liés à l’analyse des logiciels malveillants sous Linux, nous présentons la conception et la mise en œuvre du premier pipeline d’analyse des logiciels malveillants, spécialement conçu pour étudier ce phénomène émergent. Nous appliquons ensuite des techniques de similarité de code binaire pour reconstruire systématiquement la lignée des familles de logiciels malveillants de l’IoT, et suivre leurs relations, leur évolution et leurs variantes. Nous montrons comment la libre disponibilité du code source a entraîné une grand nombre de variantes, ce qui a souvent un impact sur la classification des systèmes antivirus. Enfin et surtout, nous abordons un problème majeur que nous avons rencontré dans l’analyse des exécutables liés statiquement. En particulier, nous présentons une nouvelle approche pour identifier la frontière entre le code utilisateur et les bibliothèques tierces
For the past two decades, the security community has been fighting malicious programs for Windows-based operating systems. However, the increasing number of interconnected embedded devices and the IoT revolution are rapidly changing the malware landscape. Malicious actors did not stand by and watch, but quickly reacted to create "Linux malware", showing an increasing interest in Linux-based operating systems and platforms running architectures different from the typical Intel CPU. As a result, researchers must react accordingly. Through this thesis, we navigate the world of Linux-based malicious software and highlight the problems we need to overcome for their correct analysis.After a systematic exploration of the challenges involved in the analysis of Linux malware, we present the design and implementation of the first malware analysis pipeline, specifically tailored to study this emerging phenomenon. We use our platform to analyze over 100K samples and collect detailed statistics and insights that can help to direct future works.We then apply binary code similarity techniques to systematically reconstruct the lineage of IoT malware families, and track their relationships, evolution, and variants. We show how the free availability of source code resulted in a very large number of variants, often impacting the classification of antivirus systems.Last but not least, we address a major problem we encountered in the analysis of statically linked executables. In particular, we present a new approach to identify the boundary between user code and third-party libraries, such that the burden of libraries can be safely removed from binary analysis tasks

APA, Harvard, Vancouver, ISO, and other styles

21

Hubert, Laurent. "Foundations and implementation of a tool bench for static analysis of Java bytecode programs." Rennes 1, 2010. http://www.theses.fr/2010REN1S122.

Full text

Abstract:

In this thesis we study the static analysis of Java bytecode and its semantics foundations. The initialization of an information system is a delicate operation where security properties are enforced and invariants installed. Initialization of fields, objects and classes in Java are difficult operations. These difficulties may lead to security breaches and to bugs, and make the static verification of software more difficult. This thesis proposes static analyses to better master initialization in Java. Hence, we propose a null pointer analysis that finely tracks initialization of fields. It allows proving the absence of dereferencing of null pointers (NullPointerException) and refining the intra-procedural control flow graph. We present another analysis to refine the inter-procedural control flow due to class initialization. This analysis directly allows inferring more precise information about static fields. Finally, we propose a type system that allows enforcer secure object initialization, hence offering a sound and automatic solution to a known security issue. We formalize these analyses, their semantic foundations, and prove their soundness. Furthermore, we also provide implementations. We developed several tools from our analyses, with a strong focus at having sound but also efficient tools. To ease the adaptation of such analyses, which have been formalized on idealized languages, to the full-featured Java bytecode, we have developed a library that have been made available to the community and is now used in other research labs across Europe
Dans cette thèse, nous nous intéressons à l’analyse statique du bytecode Java. L’initialisation d’un système d’information est une phase délicate où des propriétés de sécurité sont vérifiées et des invariants installés. L’initialisation en Java pose des difficultés, que ce soit pour les champs, les objets ou les classes. De ces difficultés peuvent résulter des failles de sécurité, des erreurs d’exécution (bugs), ou une plus grande difficulté à valider statiquement ces logiciels. Cette thèse propose des analyses statiques répondant aux problèmes d’initialisation de champs, d’objets et de classes. Ainsi, nous décrivons une analyse de pointeurs nuls qui suit finement l’initialisation des champs et permet de prouver l’absence d’exception de pointeur nuls (NullPointerException) et de raffiner le graphe de flot de contrôle intra-procédural. Nous proposons aussi une analyse pour raffiner le graphe de flot de contrôle inter-procédural liée à l’initialisation de classe et permettant de modéliser plus finement le contenu des champs statiques. Enfin, nous proposons un système de type permettant de garantir que les objets manipulés sont complètement initialisés, et offrant ainsi une solution formelle et automatique à un problème de sécurité connu. Les fondations sémantiques de ces analyses sont données. Les analyses sont décrites formellement et prouvées correctes. Pour pouvoir adapter ces analyses, formalisées sur de petits langages, au bytecode, nous avons développé une bibliothèque logicielle. Elle nous a permis de produire des prototypes efficaces gérant l’intégralité du bytecode Java

APA, Harvard, Vancouver, ISO, and other styles

22

Bulusu, Sravani Teja. "Méthodologie d'ingénierie des exigences de sécurité réseau." Thesis, Toulouse 3, 2019. http://www.theses.fr/2019TOU30084.

Full text

Abstract:

La construction de réseaux sécurisés est à la fois une étape cruciale et complexe pour toute organisation. Traditionnellement, cette tâche couvre les aspects architecturaux en proposant une segmentation du réseau où des règles de sécurité différentes sont appliquées à chaque zone ; elle couvre également la sécurisation des équipements d'extrémité exploités par des utilisateurs et apporte ainsi des garanties sécuritaires pour les informations transférées sur les liaisons de communication. Le plus souvent, les aspects sécurité réseau sont pris en compte après la conception du réseau et donc tardivement. Ceci se traduit inéluctablement par une augmentation de la complexité et des coûts pour prendre en compte les modifications nécessaires qui doivent alors être apportées. À cet égard, les exigences de sécurité revêtent une importance primordiale, car elles guident les décisions relatives à la mise en œuvre des contrôles de sécurité réseau (ex. Firewalls et proxies sécurité, VPN) répondant aux besoins de l'entreprise. En effet, de mauvaises exigences en matière de sécurité réseau peuvent conduire à une sécurité inefficace voire à des failles de sécurité dans la conception de la sécurité du réseau. Cependant, les méthodologies d'ingénierie des exigences de sécurité actuelles ne permettent pas de déduire les exigences de sécurité réseau. Ce travail de thèse fait partie du projet de recherche DGA IREDHO2 (Intégration REseau Haut Débit Embarqué Optique 2ème phase) qui concerne en particulier les réseaux avioniques du futur. Ce travail est le résultat d'une collaboration menée avec la société AIRBUS GROUP. Il a pour objectif de proposer une méthodologie d'ingénierie des exigences de sécurité pour capturer, exprimer et analyser les exigences de sécurité réseau, afin de pouvoir les dériver et gérer l'application de configurations réseau dans une approche "Top Down". La complexité adressée vient à la fois des différences de point de vue : i) en regard de la compréhension de la problématique de la sécurité par les différentes parties prenantes, ii) de la nature des systèmes impactés et iii) de la variabilité des niveaux d'abstraction retenus dans le cycle de développement réseau. Dans ce travail, nous avons défini une méthode qui s'appuie sur les niveaux d'abstraction proposés par la méthode SABSA (Sherwood Applied Business Security Architecture) afin de décomposer les exigences de sécurité métier en exigences de sécurité techniques. En effet, SABSA préconise l'étude de vues Métier (décisionnaire), Architecte (objectifs, risques, processus, applications, interactions), Concepteur (services de sécurité), Constructeur de réseau (mécanismes de sécurité) et Composants (produits, outils, technologies, etc.). Les vues Métier et Architecte sont exprimées dans le formalisme STS (Social Technical Systems)
Building secure networks is crucial as well as challenging for any organization. Network security majorly concerns the security architectural needs that describe network segmentation (i.e., security zoning); security of network devices connecting the communicating end user systems; and security of the information being transferred across the communication links. Most often, a late consideration of security aspects (i.e., post-deployment of network design) inevitably results in an increase in costs as well as in the complexity to take into account the necessary changes that have be made to the existing infrastructures. In this regard, network security requirements hold a paramount importance since they drive the decisions related to the implementation of security controls about business needs. Indeed, bad network security requirements can lead to ineffective and costly security or worth security holes in the network security design. Nevertheless, current security requirement engineering methodologies render no support to derive network security requirements. This thesis work is a part of the research project DGA IREHDO2 (Intégration REseau Haut Débit embarqué Optique 2ème phase) that concerns aircrafts future generation networks. Our work is done mainly in collaboration with AIRBUS and is related to the security requirements engineering process for aircraft networks. Our objective in this project is to propose an SRE methodology for capturing and analysing network security requirements, and that facilitates the refinement into network security and monitoring configurations (TOP/DOWN approach). The complexity addressed comes at a time from the differences in point of view: i) with regard to the understanding of the issue of security by different stakeholders, ii) the nature of the systems impacted and the variability of the levels of abstraction in the network development cycle. In this work, we defined SRE methodology based on the abstraction levels proposed by SABSA (Sherwood Applied Business Security Architecture) method in order to structure the refinement activity of business needs into network security requirements. Indeed, SABSA recommends the expression of the needs considering the Business view (decision makers), Architect's view (objectives, risks, processes, applications and interactions), Designer's view (security services), Builder's view (security mechanisms) and Tradesman's view (products, tools, technologies). We considered the first three views. We express the business and architect's views using STS (Social-Technical Systems) formalism. We also propose to represent attacks as multi-agent systems to facilitate the analysis of security risks at these first two views. For expressing the network security requirements captured at Designer's view, we propose a methodology that automates parts of the process of security zoning and network security requirements elicitation using a definite set of formalized rules derived from security design principles and formal integrity models. We developed a tool that implements these rules in ASP (Answer set programming), which facilitates calculating cost-optimal security zone models. In the end, to ensure traceability between the three views, we defined a new modelling notation based on the concepts proposed in KAOS (Keep All Objectives Satisfied) and STS. We illustrate our methodology using a scenario specific to the IRHEDO2 project. Finally, we evaluate our methodology using: 1) an e-commerce enterprise case study; 2) a new scenario specific to the IRHEDO2 project

APA, Harvard, Vancouver, ISO, and other styles

23

Karray, Achraf. "Conception, mise en œuvre et validation d’un environnement logiciel pour le calcul sécurisé sur une grille de cartes à puce de type Java." Thesis, Bordeaux 1, 2008. http://www.theses.fr/2008BOR13724/document.

Full text

Abstract:

Le calcul sur grille permet à un individu, une société, de disposer d’un ensemble d’unités de calcul fournies par des tiers. Dans ce type d’architecture, des problèmes de sécurité se posent : comment garantir à la fois la sécurité du matériel et de l’application. Pour ce qui concerne la sécurité de l’application, il s’agit principalement d’assurer la confidentialité du code et l’intégrité de son exécution. La sécurité du matériel consiste à protéger la machine contre tout code malveillant pouvant être contenu dans l’application. Aucun système ne permet aujourd’hui, de satisfaire ces contraintes fortes de sécurité. Notre objectif dans cette thèse est de proposer et de valider des solutions pour les problèmes de sécurité des grilles informatiques.Pour résoudre ces problèmes, nous proposons l’utilisation de la carte à puce comme support d’exécution hautement sécurisé à travers le déploiement de grilles de cartes à puce. Grâce aux mécanismes de sécurité qu’elles intègrent, les cartes à puce permettent en effet de protéger l’application et son code aussi bien que le support d’exécution. Le travail effectué dans cette thèse consiste à définir un environnement pour le calcul sécurisé sur grille de cartes à puce
Abstract

APA, Harvard, Vancouver, ISO, and other styles

24

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

25

Ali, Loubna. "Gestionnaire d'infrastructure distribuée." Lyon, INSA, 2008. http://theses.insa-lyon.fr/publication/2008ISAL0088/these.pdf.

Full text

Abstract:

Les contraintes de flexibilité et réactivité sur les entreprises conduisent celles-ci à de nouvelles formes organisationnelles : alliances, réseaux et autres organisations collaboratives. Cette tendance est favorisée par la diffusion des technologies de l'information et de la communication puisque ces organisations collaboratives imposent des processus interentreprises et de partager les systèmes d'information. Ainsi, ces nouvelles architectures organisationnelles utilisent largement des infrastructures distribuées ce qui impose de prendre en compte des contraintes de sécurisation, de contrôle d'accès et de gestion de la qualité de service. En outre, du fait de l'évolutivité de ces organisations, le système de management de l'infrastructure distribué doit permettre de réaliser un management pro-actif (pour s'adapter au mieux aux changements de contexte) et autonome (de manière à garantir l'agilité du système). Pour répondre à ces besoins, nous proposons de coupler la modélisation des processus d'entreprise à la modélisation de l'infrastructure distribuée pour établir des prévisions d'usage de l'infrastructure (ce qui permet de réaliser une gestion proactive) et d'utiliser les données collectées via le système d'administration pour surveiller et gérer la qualité de service de bout en bout. Pour garantir l'agilité du système de management, nous avons choisi de l'implémenter dynamiquement grâce à une plate-forme d'agents mobiles (les aglets). Notre architecture de management est basée sur un système d'administration multi-niveaux (suivant l'organisation hiérarchique de l'infrastructure distribuée de l'organisation collaborative) décentralisé (respectant ainsi les zones de responsabilité). Cette plate-forme constitue un point d'interconnexion non seulement entre les différentes zones géographiques de l'organisation mais aussi entre les différents niveaux de décision dans le système de management. L'intégration d'un mécanisme de composition d'agents offre une grande flexibilité et permet de définir "à la demande" les outils nécessaires à l'administration. Enfin, notre plate-forme ne se limite pas à la gestion pro-active de l'infrastructure, elle permet également de supporter des mécanismes de sécurité en pouvant générer les agents capables de mettre en oeuvre des fonctionnalités d'authentification ou d'autorisation
The diffusion of the TIC and the constraints of flexibility and reactivity on the companies lead those to new organizational forms: alliances, networks and another definition of BP inter enterprise in addition of an increased division of the information systems. These new organizational architectures largely use distributed infrastructures what forces to take into account: the security constraints, the access control and the quality of service management. Since of evolutionarily of these organizations, the distributed infrastructure management system must allow the realization of proactive management (to adapt as well as possible to the context changing) and autonomous (so as to guarantee the system agility). To realize these needs, we propose to couple the processes modelling of company with the distributed infrastructure modelling to establish forecasts of the infrastructure utilization (which make the realization of a proactive management possible) and to use the collected data via the administration system to monitor and manage the quality of service from beginning to end. To guarantee the agility of the management system, we chose to implement it dynamically thanks to a mobile agents (aglets) platform. Our management architecture is based on a multilevel administration system (according to the hierarchical organization of the distributed infrastructure of the virtual enterprise) and it is decentralized (thus respecting the responsibility zones). This platform constitutes a point of interconnection not only between the various geographical organization areas but also between the various levels of decision in the management system. The integration of agent’s composition mechanism offers a great flexibility and makes it possible to define "in the request" the necessary administration tools. Lastly, our platform is not limited to the proactive infrastructure management; it makes the possibility also to support security mechanisms while generating the agents able to execute the functionalities of authentication or authorization

APA, Harvard, Vancouver, ISO, and other styles

26

Occello, Audrey. "Capitalisation de la sûreté de fonctionnement des applications soumises à des adaptations dynamiques : le modèle exécutable Satin." Phd thesis, Université de Nice Sophia-Antipolis, 2006. http://tel.archives-ouvertes.fr/tel-00090755.

Full text

Abstract:

Les technologies pour l'adaptation dynamique (composants, aspects, ...)
arrivent à maturité et permettent de modifier les applications durant leur
exécution. Si l'on considère que la sûreté de fonctionnement d'une
application est la propriété permettant aux utilisateurs d'un système de
placer une confiance justifiée dans le service qu'il leur délivre alors il
faut garantir lors d'une adaptation dynamique que cette propriété est
préservée. Autrement dit, une adaptation n'est pas "sûre" à partir du moment
où le service que fournit l'application après adaptation diverge du service
attendu par l'utilisateur.

Actuellement, il n'existe pas de solution appropriée au problème de la
sûreté des adaptations dynamiques. En effet, un certain nombre de techniques
(typage, model-checking, ...) destinées à concevoir et implémenter les
systèmes informatiques de façon sûre peuvent être utilisées dans le cadre
des adaptations statiques mais pas directement pour valider des adaptations
dynamiques. De plus, la prise en charge de ces dernières doit tenir compte
du risque qu'une adaptation se produise à un moment inadéquat dans
l'exécution de l'application et implique de traiter les problèmes de sûreté
parallèlement à l'exécution de l'application sans perturbation. Bien que les
plates-formes permettant les adaptations dynamiques proposent des solutions,
il n'existe pas de consensus autour des vérifications à effectuer dans un
contexte dynamique. D'autre part, la mise en oeuvre de ces vérifications
reste souvent informelle ou à la charge du développeur d'applications.

Nous proposons d'identifier la sûreté d'une adaptation indépendamment des
plates-formes, et de déterminer le moment où les modifications liées à une
adaptation peuvent être prises en compte de façon sûre dans l'exécution de
l'application. Cette approche est basée sur un modèle nommé Satin sur lequel
des propriétés de sûreté sont exprimées et validées. Le modèle Satin est mis
en oeuvre sous la forme d'un service de sûreté que les plates-formes peuvent
interroger pour déterminer si une adaptation donnée risque de briser la
sûreté de fonctionnement de l'application.

APA, Harvard, Vancouver, ISO, and other styles

27

Varet, Antoine. "Conception, mise en oeuvre et évaluation d'un routeur embarqué pour l'avionique de nouvelle génération." Phd thesis, INSA de Toulouse, 2013. http://tel.archives-ouvertes.fr/tel-00932283.

Full text

Abstract:

Le contexte aéronautique a depuis plusieurs années mis en évidence le besoin croissant de technologies de sécurité permettant d'éviter des utilisations malveillantes des matériels ou services installés à bord des avions. La plupart des approches de sécurisation 'avion' se concentre sur des méthodes et techniques permettant de sécuriser les échanges au sein de l'avion. Elles sont cependant inadaptées à la sécurisation dans les cas d'interconnexion des réseaux avioniques avec le reste des réseaux de communication (réseau Internet par exemple). Le problème abordé dans ce travail de thèse vise donc à proposer une architecture de sécurité et de sûreté pour l'ensemble des communications aéronautiques et permettant une interconnexion sécurisée entre le monde 'avion' et le monde extérieur, en tenant compte de l'ensemble des critères de sécurité qui caractérisent les divers environnements traversés et considère dès le départ les divers principes de standardisation associés afin de garantir la pérennité scientifique et industrielle. La solution architecturale proposée dans ce travail de thèse repose principalement sur un composant central de routage, de filtrage et de sécurisation des flux de données aéronautiques. Le travail de conception et de développement de ce composant appelé Routeur Sécurisé de Nouvelle Génération (routeur SNG) a permis une validation expérimentale sur un système reproduisant un système embarqué.

APA, Harvard, Vancouver, ISO, and other styles

28

Scholte, Theodoor. "Amélioration de la sécurité par la conception des logiciels web." Electronic Thesis or Diss., Paris, ENST, 2012. http://www.theses.fr/2012ENST0024.

Full text

Abstract:

L'internet est devenu un environnement omniprésent dans le monde du travail et du loisir. La popularité sans cesse croissante des applications web ainsi que des services associés entraînent l'exécution de nombreuses transactions critiques, qui soulèvent des questions de sécurité. Du fait de cette croissance, des efforts ont été entrepris durant cette dernière décennie pour rendre les applications web plus sûres. Malgré ces efforts, de récents rapports provenant de l'institut SANS estiment que plus de 60 % des attaques commises sur l'Internet ciblent les applications web en se concentrant sur les vulnérabilités inhérentes aux problèmes de validation, comme le Cross-Site Scripting ou les injections SQL. Dans cette thèse, nous avons conduit deux études de recherche empirique, analysant un grand nombre d'application web vulnérables. Nous avons assemblé une base de données contenant plus de 10.000 rapports de vulnérabilités depuis l'an 2000. Ensuite, nous avons analysé ces données pour déterminer si les développeurs ont pris conscience des problématiques de sécurité web de nos jours, comparé à la période où ces applications émergeaient. Puis nous avons analysé l'étroit lien entre le langage de programmation utilisé pour développer l'application web et le nombre de vulnérabilité reporté. Avec ces résultats empiriques comme base, nous présentons notre solution IPAAS qui aide les développeurs novice en termes de sécurité à écrire des applications sécurisées par défaut. Nous montrons par ailleurs que cette technique améliore de manière probante la sécurité des applications web
The web has become a backbone of our industry and daily life. The growing popularity of web applications and services and the increasing number of critical transactions being performed, has raised security concerns. For this reason, much effort has been spent over the past decade to make web applications more secure. Despite these efforts, recent data from SANS institute estimates that up to 60% of Internet attacks target web applications and critical vulnerabilities such as cross-site scripting and SQL injection are still very common. In this thesis, we conduct two empirical studies on a large number of web applications vulnerabilities with the aim of gaining deeper insights in how input validation flaws have evolved in the past decade and how these common vulnerabilities can be prevented. Our results suggest that the complexity of the attacks have not changed significantly and that many web problems are still simple in nature. Our studies also show that most SQL injection and a significant number of cross-site scripting vulnerabilities can be prevented using straight-forward validation mechanisms based on common data types. With these empirical results as foundation, we present IPAAS which helps developers that are unaware of security issues to write more secure web applications than they otherwise would do. It includes a novel technique for preventing the exploitation of cross-site scripting and SQL injection vulnerabilities based on automated data type detection of input parameters. We show that this technique results in significant and tangible security improvements for real web applications

APA, Harvard, Vancouver, ISO, and other styles

29

Mantovani, Alessandro. "An Analysis of Human-in-the-loop Approaches for Reverse Engineering Automation." Electronic Thesis or Diss., Sorbonne université, 2022. https://accesdistant.sorbonne-universite.fr/login?url=https://theses-intra.sorbonne-universite.fr/2022SORUS052.pdf.

Full text

Abstract:

En matière de sécurité des systèmes et des logiciels, l'un des premiers critères avant d'appliquer une méthodologie d'analyse est de distinguer selon la disponibilité ou non du code source. Lorsque le logiciel que nous voulons investiguer est présent sous forme binaire, la seule possibilité que nous avons est d'en extraire des informations en observant son code machine, en effectuant ce qui est communément appelé Binary Analysis (BA). Les artisans de ce secteur sont chargés de mêler leur expérience personnelle à un arsenal d'outils et de méthodologies pour comprendre certains aspects intrinsèques et cachés du binaire cible, par exemple pour découvrir de nouvelles vulnérabilités ou détecter des comportements malveillants. Bien que cette configuration humaine dans la boucle soit bien consolidée au fil des ans, l'explosion actuelle des menaces et des vecteurs d'attaque tels que les logiciels malveillants, les exploits armés, etc. met implicitement à l'épreuve ce modèle de BA, exigeant en même temps une grande précision de l'analyse ainsi qu'une évolutivité appropriée des binaires pour contrer les acteurs adverses. C'est pourquoi, malgré les nombreux progrès réalisés dans le domaine de la BA au cours des dernières années, nous sommes toujours obligés de chercher de nouvelles solutions. Dans cette thèse, nous faisons un pas de plus sur ce problème et nous essayons de montrer ce qui manque aux paradigmes actuels pour augmenter le niveau d'automatisation. Pour ce faire, nous avons isolé trois cas d'utilisation classiques de l'analyse binaire et nous avons démontré comment l'analyse en pipeline bénéficie de l'intervention humaine. En d'autres termes, nous avons considéré trois systèmes "human-in-the-loop" et nous avons décrit le rôle de l'homme dans le pipeline en nous concentrant sur les types de feedback que l'analyste "échange" avec sa chaîne d'outils. Ces trois exemples nous ont fourni une vue complète de l'écart entre les solutions actuelles d'analyse binaire et les solutions idéalement plus automatisées, suggérant que la principale caractéristique à la base du retour d'information humain correspond à la compétence humaine à comprendre des portions de code binaire. Cette tentative de systématisation du rôle de l'homme dans les approches modernes de l'analyse binaire tente d'élever la barre vers des systèmes plus automatisés en tirant parti de la composante humaine qui, jusqu'à présent, est toujours inévitable dans la majorité des scénarios d'analyse binaire. Bien que notre analyse montre que les machines ne peuvent pas remplacer les humains au stade actuel, nous ne pouvons pas exclure que les approches futures seront en mesure de combler cette lacune et de faire évoluer les outils et les méthodologies vers un niveau supérieur. Par conséquent, nous espérons avec ce travail, inspirer les recherches futures dans le domaine pour atteindre des techniques d'analyse binaire toujours plus sophistiquées et automatisées
In system and software security, one of the first criteria before applying an analysis methodology is to distinguish according to the availability or not of the source code. When the software we want to investigate is present in binary form, the only possibility that we have is to extract some information from it by observing its machine code, performing what is commonly referred to as Binary Analysis (BA). The artisans in this sector are in charge of mixing their personal experience with an arsenal of tools and methodologies to comprehend some intrinsic and hidden aspects of the target binary, for instance, to discover new vulnerabilities or to detect malicious behaviors. Although this human-in-the-loop configuration is well consolidated over the years, the current explosion of threats and attack vectors such as malware, weaponized exploits, etc. implicitly stresses this binary analysis model, demanding at the same time for high accuracy of the analysis as well as proper scalability over the binaries to counteract the adversarial actors. Therefore, despite the many advances in the BA field over the past years, we are still obliged to seek novel solutions. In this thesis, we take a step more on this problem, and we try to show what current paradigms lack to increase the automation level. To accomplish this, we isolated three classical binary analysis use cases, and we demonstrated how the pipeline analysis benefits from the human intervention. In other words, we considered three human-in-the-loop systems, and we described the human role inside the pipeline with a focus on the types of feedback that the analyst ``exchanges'' with her toolchain. These three examples provided a full view of the gap between current binary analysis solutions and ideally more automated ones, suggesting that the main feature at the base of the human feedback corresponds to the human skill at comprehending portions of binary code. This attempt to systematize the human role in modern binary analysis approaches tries to raise the bar towards more automated systems by leveraging the human component that, so far, is still unavoidable in the majority of the scenarios. Although our analysis shows that machines cannot replace humans at the current stage, we cannot exclude that future approaches will be able to fill this gap as well as evolve tools and methodologies to the next level. Therefore, we hope with this work to inspire future research in the field to reach always more sophisticated and automated binary analysis techniques

APA, Harvard, Vancouver, ISO, and other styles

30

Sannier, Nicolas. "INCREMENT : une approche hybride pour modéliser et analyser dans le large les exigences réglementaires de sûreté." Phd thesis, Université Rennes 1, 2013. http://tel.archives-ouvertes.fr/tel-00941881.

Full text

Abstract:

Les systèmes de contrôle-commande importants pour la sûreté de fonctionnement doivent répondre à un certain nombre d'exigences, au premier rang desquelles se trouvent les exigences réglementaires, édictées par les autorités nationales et complétées par un ensemble de recommandations pratiques et de textes normatifs. Les exigences de ce domaine sont peu formalisées, les relations de traçabilité, et par conséquent l'organisation des exigences de ce vaste domaine est souvent implicite. Enfin, les passerelles entre contextes nationaux différents sont très peu développées. Les travaux de cette thèse se situent dans ce contexte industriel en partenariat avec EDF R&D et au sein du projet CONNEXION regroupant les acteurs majeurs du contrôle-commande nucléaire français. Les contributions de la thèse s'articulent autour de l'approche INCREMENT (Intrumentation aNd Control regulatory REquirement Modeling Environment) qui adresse les deux premiers challenges présentés, et en particulier : (1) la formalisation du domaine où nous proposons à la fois une description du domaine et un métamodèle permettant une capitalisation et une vue globale d'un référentiel d'exigences, (2) une base outillée pour l'acquisition automatique de documents, un environnement graphique pour la manipulation de modèles et l'apport de techniques de recherche d'information pour la traçabilité des exigences, (3) une approche originale avec une hybridation entre modélisation et recherche d'information pour une amélioration de la traçabilité des exigences. Le métamodèle proposé et ses outils sont utilisés dans l'industrie dans le projet CONNEXION. Notre approche hybride a permis dans nos expérimentations de réduire, en moyenne, la taille de ces espaces de 65% comparé aux approches standard de recherche d'information, sans en dégrader le contenu.

APA, Harvard, Vancouver, ISO, and other styles

31

Kang, Eun-Young. "Abstractions booléennes pour la vérification des systèmes temps-réel." Thesis, Nancy 1, 2007. http://www.theses.fr/2007NAN10089/document.

Full text

Abstract:

Cette thèse présente un schéma formel et efficace pour la vérification de systèmes temps-réel. Ce schéma repose sur la combinaison par abstraction de techniques déductives et de model checking, et cette combinaison permet de contourner les limites de chacune de ces techniques. La méthode utilise le raffinement itératif abstrait (IAR) pour le calcul d'abstractions finies. Etant donné un système de transitions et un ensemble fini de prédicats, la méthode détermine une abstraction booléenne dont les états correspondent à des ensembles de prédicats. La correction de l'abstraction par rapport au système d'origine est garantie en établissant un ensemble de conditions de vérification, issues de la procédure IAR. Ces conditions sont à démontrer à l'aide d'un prouveur de théorèmes. Les propriétés de sûreté et de vivacité sont ensuite vérifiées par rapport au modèle abstrait. La procédure IAR termine lorsque toutes les conditions sont vérifiées. Dans le cas contraire, une analyse plus fine détermine si le modèle abstrait doit être affiné en considérant davantage de prédicats. Nous identifions une classe de diagrammes de prédicats appelés PDT (predicate diagram for timed system) qui décrivent l'abstraction et qui peuvent être utilisés pour la vérification de systèmes temporisés et paramétrés
This thesis provides an efficient formal scheme for the tool-supported real-time system verification by combination of abstraction-based deductive and model checking techniques in order to handle the limitations of the applied verification techniques. This method is based on IAR (Iterative Abstract Refinement) to compute finite state abstractions. Given a transition system and a finite set of predicates, this method determines a finite abstraction, where each state of the abstract state space is a true assignment to the abstraction predicates. A theorem prover can be used to verify that the finite abstract model is a correct abstraction of a given system by checking conformance between an abstract and a concrete model by establishing/proving that a set of verification conditions are obtained during the IAR procedure. Then the safety/liveness properties are checked over the abstract model. If the verification condition holds successfully, IAR terminates its procedure. Otherwise more analysis is applied to identify if the abstract model needs to be more precise by adding extra predicates. As abstraction form, we adopt a class of predicate diagrams and define a variant of predicate diagram PDT (Predicate Diagram for Timed systems) that can be used to verify real-time and parameterized systems

APA, Harvard, Vancouver, ISO, and other styles

32

Poeplau, Sebastian. "Increasing the performance of symbolic execution by compiling symbolic handling into binaries." Electronic Thesis or Diss., Sorbonne université, 2020. http://www.theses.fr/2020SORUS451.

Full text

Abstract:

L'exécution symbolique a le potentiel de rendre les logiciels plus sûrs en améliorant considérablement la recherche automatisée des vulnérabilités. Nous proposons une technique générale qui permet des implémentations plus efficaces de la composante d'exécution dans les exécuteurs symboliques. Nous examinons d'abord l'état de l'art. A partir des résultats de cette comparaison, nous dérivons l'idée d'accélérer l'exécution en intégrant la manipulation symbolique dans les programmes compilés au lieu d'interpréter symboliquement une représentation de plus haut niveau du programme testé. En utilisant cette approche, nous développons un exécuteur symbolique basé sur le compilateur et nous montrons qu'il atteint effectivement une vitesse d'exécution élevée par rapport aux systèmes actuellement les plus performants. Comme le compilateur est limité aux scénarios où le code source du programme testé est disponible, nous concevons et mettons en œuvre une solution complémentaire pour l'exécution symbolique des binaires ; elle utilise la même idée de base d'intégration de l'exécution symbolique dans un code machine rapide, mais combine l'approche avec la traduction binaire pour relever les défis de l'analyse binaire seule. Nous concluons en discutant des directions de recherche qui pourraient conduire à des systèmes encore plus pratiques
Symbolic execution has the potential to make software more secure by significantly improving automated vulnerability search. In this thesis, we propose a general technique that allows for more efficient implementations of the execution component in symbolic executors. We first examine the state of the art. From the results of this comparison, we derive the idea of accelerating execution by embedding symbolic handling into compiled programs instead of symbolically interpreting a higher-level representation of the program under test. Using this approach, we develop a compiler-based symbolic executor and show that it indeed achieves high execution speed in comparison with state-of-the-art systems. Since the compiler is limited to scenarios where source code of the program under test is available, we then design and implement a complementary solution for symbolic execution of binaries; it uses the same basic idea of embedding symbolic execution into fast machine code but combines the approach with binary translation to handle the challenges of binary-only analysis. We conclude by discussing research directions that could lead to even more practical systems and ultimately enable the use of symbolic execution in mainstream software testing

APA, Harvard, Vancouver, ISO, and other styles

33

Pellegrino, Giancarlo. "Détection d'anomalies logiques dans les logiciels d'entreprise multi-partis à travers des tests de sécurité." Thesis, Paris, ENST, 2013. http://www.theses.fr/2013ENST0064/document.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

34

Cauchie, Stéphane. "Tactim : from pattern recognition to the security for Biometry." Thesis, Tours, 2009. http://www.theses.fr/2009TOUR4033.

Full text

Abstract:

Dans ce travail de thèse, nous proposons d'étudier un nouveau procédé biométrique selon deux axes de recherches; le premier sous le regard de la reconnaissance de formes, et le deuxième sous le regard de la sécurité. La première partie est consacrée à l'étude de ce nouveau procédé : Tactim. A l'aide du traitement du signal, nous proposons un ensemble d'extracteurs de caractéristiques puis nous présentons notre système de reconnaissance. Il est à préciser que les chaînes de reconnaissance de formes retenues ont été déterminées par notre plateforme de résolution de problèmes de reconnaissance de formes : Coyote. La deuxième partie est consacrée à son étude; Coyote est basé sur les concepts du raisonnement à base de cas afin d'assembler des algorithmes connus avec comme objectif la minimisation des taux d'erreurs des chaînes produites. Enfin, une fois la partie reconnaissance de formes finalisée (taux d'erreur acceptable), nous nous sommes penchés sur le problème de son intégration dans une architecture répartie (internet). Au sein de la troisième partie, nous étudions les protocoles cryptographiques permettant d'assurer l'anonymat de l'utilisateur lors d'une authentification biométrique. Nous proposons ainsi une hybridation de notre modèle de reconnaissance avec notre protocole cryptographique (une extension du protocole de Bringer et al.)
In this thesis, we propose a study on a new biometric signal following two axes; on the one hand, the pattern recognition objective and on the other hand security aspects. The first part is dedicated to the study of this new process: Tactim. With the help of signal processing methods, we propose a set of characteristic extractors. Then we present their uses through our biometric system. We take advantage of our pattern recognition solver, Coyote, in order to produce our biometric system. The second part is dedicated to the study of Coyote. Coyote is a Case Based Reasoning system, which assembles algorithms in order to produce pattern recognition systems which objective is to minimize error rates. Finally, when we consider the pattern recognition task accomplished (acceptable error rate), we study cryptographic protocols that ensure anonymity of the user during a biometric authentication. We propose a hybridization of our pattern recognition model with our cryptographic protocol (extension of the Bringer et al. protocol)

APA, Harvard, Vancouver, ISO, and other styles

35

Olivier, Paul L. R. "Improving Hardware-in-the-loop Dynamic Security Testing For Linux-based Embedded Devices." Electronic Thesis or Diss., Sorbonne université, 2023. http://www.theses.fr/2023SORUS049.

Full text

Abstract:

Les techniques d'analyse dynamique ont prouvé leur efficacité dans l'évaluation de la sécurité. Il est en revanche nécessaire de pouvoir exécuter le code à analyser et c'est souvent un défi pour les firmware dont la plupart sont profondément intégrés à l’architecture matérielle du système embarqué. L'émulation permet d’exécuter une grande partie du code mais se retrouve rapidement limitée lorsqu’il est nécessaire d'interagir avec des composants spécialisés. Pour cela, l’approche d'émulation partielle, ou hardware-in-the-loop, offre plusieurs avantages: transférer les accès aux matériels qui sont difficiles à émuler correctement et exécuter le firmware à tour de rôle sur les deux entités. Jusqu'à présent, cette approche a été principalement considérée pour les firmware monolithiques, mais moins pour les dispositifs utilisant des systèmes d'exploitation avancés. Dans cette thèse, nous explorons les défis des tests de sécurité pour les processus exécutés dans un environnement émulé où une partie de leur exécution doit être transmise à leur dispositif physique d'origine. Au travers de cette thèse, nous passons d'abord en revue les différentes techniques d'interception des appels système ainsi que leurs objectifs. Nous discutons des défis des différentes manières d'exécuter un processus dans deux noyaux Linux différents. Nous implémentons au travers d’un framework ces transferts pour un processus Linux avec ses appels système et accès mémoire entre son environnement émulé et son environnement d’origine sur le dispositif physique. Afin de surmonter les défis liés à l'utilisation de dispositifs physiques pour ces tests de sécurité, nous présentons également une nouvelle plateforme pour les tests de sécurité hardware-in-the-loop
Dynamic analysis techniques have proven their effectiveness in security assessment. Nevertheless, it is necessary to be able to execute the code to be analyzed and this is often a challenge for firmware, most of which are deeply integrated into the hardware architecture of embedded systems. Emulation allows to execute a large part of the code but is quickly limited when it is necessary to interact with specialized components. For this, the partial emulation, or hardware-in-the-loop, approach offers several advantages: transferring access to hardware that is difficult to emulate properly and executing the firmware in turn on both entities. To date, this approach has been considered primarily for monolithic firmware, but less so for devices running advanced operating systems. In this thesis, we explore the challenges of security testing for processes running in an emulated environment where part of their execution must be transmitted to their original physical device. Throughout this thesis, we first review the various techniques for intercepting system calls and their objectives. We highlight the fact that forwarding is not a very well explored technique in depth but is a promising approach for evaluating the security of embedded applications. We discuss the challenges of different ways of running a process in two different Linux kernels. We implement through a framework these transfers for a Linux process with its system calls and memory accesses between its emulated environment and its original environment on the physical device. To overcome the challenges of using physical devices for these security tests, we also present a new test platform to reproduce hardware-in-the-loop security experiments

APA, Harvard, Vancouver, ISO, and other styles

36

Rahmoun, Smail. "Optimisation multi-objectifs d'architectures par composition de transformation de modèles." Electronic Thesis or Diss., Paris, ENST, 2017. http://www.theses.fr/2017ENST0004.

Full text

Abstract:

Nous proposons dans cette thèse une nouvelle approche pour l'exploration d’espaces de conception. Plus précisément, nous utilisons la composition de transformations de modèles pour automatiser la production d'alternatives architecturales, et les algorithmes génétiques pour explorer et identifier des alternatives architecturales quasi-optimales. Les transformations de modèles sont des solutions réutilisables et peuvent être intégrées dans des algorithmes génétiques et ainsi être combinées avec des opérateurs génétiques tels que la mutation et le croisement. Grâce à cela, nous pouvons utiliser (ou réutiliser) différentes transformations de modèles implémentant différents patrons de conception sans pour autant modifier l’environnement d’optimisation. En plus de cela, les transformations de modèles peuvent être validées (par rapport aux contraintes structurelles) en amont et ainsi rejeter avant l’exploration les transformations générant des alternatives architecturales incorrectes. Enfin, les transformations de modèles peuvent être chainées entre elles afin de faciliter leur maintenance, leur réutilisabilité et ainsi concevoir des modèles plus détaillés et plus complexes se rapprochant des systèmes industrielles. A noter que l’exploration de chaines de transformations de modèles a été intégrée dans l’environnement d’optimisation
In this thesis, we propose a new exploration approach to tackle design space exploration problems involving multiple conflicting non functional properties. More precisely, we propose the use of model transformation compositions to automate the production of architectural alternatives, and multiple-objective evolutionary algorithms to identify near-optimal architectural alternatives. Model transformations alternatives are mapped into evolutionary algorithms and combined with genetic operators such as mutation and crossover. Taking advantage of this contribution, we can (re)-use different model transformations, and thus solve different multiple-objective optimization problems. In addition to that, model transformations can be chained together in order to ease their maintainability and re-usability, and thus conceive more detailed and complex systems

APA, Harvard, Vancouver, ISO, and other styles

37

Girard, Pierre. "Formalisation et mise en œuvre d'une analyse statique de code en vue de la vérification d'applications sécurisées." Toulouse, ENSAE, 1996. http://www.theses.fr/1996ESAE0010.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

38

Ciarletta, Laurent. "Contribution à l'évaluation des technologies de l'informatique ambiante." Nancy 1, 2002. http://www.theses.fr/2002NAN10234.

Full text

Abstract:

L'informatique et les réseaux s'embarquent toujours plus dans notre quotidien. L' " informatique (devenant) ambiante " est à la convergence de quatre domaines classiques : les réseaux (qui assureront l'interconnexion des divers éléments), l'informatique personnelle (et les services qu'elle fournit), l'informatique embarquée (et les progrès de la miniaturisation matérielle et logicielle), ainsi que l'interaction homme-machine (où l'intelligence artificielle fournira l'intelligence nécessaire à cette interaction). Le document présente ce domaine émergent et les différents outils, architectures et méthodes d'évaluation de ces technologies développés pendant ma thèse : le modèle LCP de l'informatique ambiante, la plate-forme d'évaluation EXiST et l'architecture de sécurité VPSS. Ils sont une première étape à la résolution des problèmes de sécurité, de standardisation, d'intégration et de convergence des technologies en jeu. Il présente aussi les résultats de nos expérimentations avec les adaptateurs Aroma (fournissant de l'intelligence adhoc à des appareils électroniques), une salle de conférence intelligente et l'utilisation d'agents intelligents avec EXiST
Computer Science and Networks are more and more embedded into our daily life. Pervasive or Ubiquitous Computing is at the crossroad of four typical areas: Networking (connecting the elements), Personal Computing (providing services), Embedded Computing (improving software and hardware miniaturization), and Computer-Human Interaction (where artificial intelligence will provide the needed cleverness). This document introduces this emerging technology and the tools, architectures and methods that were developed during the course of my PhD: the Layered Pervasive Computing model, EXiST, the evaluation and distributed simulation platform and the VPSS security architecture. They are first steps towards the resolution of security, standardization, integration, and convergence issues of the technologies at play. Some prototypes and implementations, such as the Aroma Adapter (providing adhoc "intelligence" to electronic devices), a Smart conference Room and a version of EXiST working with Intelligent Agents, are also detailed

APA, Harvard, Vancouver, ISO, and other styles

39

Lesas, Anne-Marie. "Vers un environnement logiciel générique et ouvert pour le développement d'applications NFC sécurisées." Thesis, Aix-Marseille, 2017. http://www.theses.fr/2017AIXM0286/document.

Full text

Abstract:

Dans le domaine des transactions et du paiement électronique avec une carte à puce, le standard de communication en champ proche « Near Field Communication » (NFC) s’est imposé comme la technologie des transactions sans contact mobiles sécurisées pour le paiement, le contrôle d’accès, ou l’authentification. Les services sans contact mobiles sécurisés sont basés sur le mode émulation de carte du standard NFC qui implique une composante matérielle à accès restreint de type carte à puce appelée « Secure Element » (SE) dans laquelle sont stockées les données confidentielles et les fonctions sensibles. Malgré les efforts de standardisation de l'écosystème, les modèles proposés pour la mise en œuvre du SE sont complexes et souffrent du manque de généricité, à la fois pour offrir des mécanismes d’abstraction, pour le développement d’applications de haut niveau, et pour la mise en œuvre et la vérification des contraintes de sécurité des applications.L’objectif de la thèse est de concevoir et réaliser un environnement logiciel basé sur un modèle générique compatible avec les standards établis et peu sensible aux évolutions technologiques. Cet environnement devrait permettre à des non-experts de développer des applications multiplateformes, multimodes, multi-facteurs de forme, qui s’interfacent avec le SE dans un smartphone NFC
In the field of electronic transactions and payment with a smart card, the Near Field Communication (NFC) standard has stood out against other candidate technologies for secure mobile contactless transactions for payment, access control, or authentication. Secure mobile contactless services are based on the card emulation mode of the NFC standard which involves a smart card type component with restricted access called "Secure Element" (SE) in which sensitive data and sensitive functions are securely stored and run. Despite considerable standardization efforts around the SE ecosystem, the proposed models for the implementation of SE are complex and suffer from the lack of genericity, both to offer abstraction mechanisms, for the development of high-level applications, and for the implementation and verification of applications security constraints.The objective of the thesis is to design and realize a software environment based on a generic model that complies with established standards and which is not very sensitive to technological evolutions. This environment should enable non-experts to develop multi-platform, multi-mode, multi-factor SE-based applications running into the NFC smartphone

APA, Harvard, Vancouver, ISO, and other styles

40

Corteggiani, Nassim. "Towards system-wide security analysis of embedded systems." Electronic Thesis or Diss., Sorbonne université, 2020. http://www.theses.fr/2020SORUS285.

Full text

Abstract:

Cette thèse se consacre à l'amélioration des techniques d'analyse dynamiques permettant la vérification de logiciels conçus pour des systèmes embarqués, couramment appelé micrologiciel. Au vu de l'augmentation significative de la connectivité des appareils électroniques, les préoccupations concernant leur sécurité s'intensifient. Les conséquences d'une faille de sécurité sur ces appareils peuvent impliquer des répercussions économiques non négligeables et des difficultés techniques importantes pour appliquer un correctif. C’est le cas notamment des amorceurs de code qui sont généralement stockés sur des mémoires mortes et intégrées dans les couches physiques qui constituent le microcontrôleur. Par conséquent, l’analyse de code source spécifique aux systèmes embarqués pendant la phase de production des micro-contrôleurs est cruciale. Cette thèse présente des techniques d'analyse afin de tester la sécurité de composants logiciel et matériel à l'échelle du système. En particulier, nous nous intéressons aux techniques de test basé sur l'émulation partielle dont nous améliorons les capacités avec trois nouvelles approches. Premièrement, Inception un outil d’analyse dynamique permettant d’appliquer des méthodes de tests exhaustifs (exécution symbolique) sur le code source de micrologiciel même lorsque ce dernier dépend de code plus bas niveau (exemple, code binaire ou assembleur). Deuxièmement, une sonde haute performance basé sur le protocol USB 3.0 afin de réduire la latence lors des communications entre l'outil d'analyse et le vrai matériel. Troisièmement, HardSnap une méthode permettant de générer des instantanés des périphériques matériel afin d'augmenter le contrôle et la visibilité lors de l'exécution symbolique. Cet outil permet de réaliser une exploration concurrente de plusieurs chemins d'exécution sans inconsistance
This thesis is dedicated to the improvement of dynamic analysis techniques allowing the verification of software designed for embedded systems, commonly called firmware. It is clear that the increasing pervasiveness and connectivity of embedded devices significantly increase their exposure to attacks. The consequences of a security issue can be dramatic not least in the economical field, but on the technical stage as well. Especially because of the difficulty to patch some devices. For instance, offline devices or code stored in a mask rom which are read only memory programmed during the chip fabrication. For all these reasons, it is important to thoughtfully test firmware program before the manufacturing process. This thesis presents analysis methods for system-wide testing of security and hardware components. In particular, we propose three impvrovements for partial emulation. First, Inception a dynamic analysis tool to test the security of firmware programs even when mixing different level of semantic (e.g., C/C++ mixed with assembly). Second, Steroids a high performance USB 3.0 probe that aims at minimizing the latency between the analyzer and the real device. Finally, HardSnap a hardware snapshotting method that offers higher visibility and control over the hardware peripherals. It enables testing concurently different execution paths without corrupting the hardware peripherals state

APA, Harvard, Vancouver, ISO, and other styles

41

Jakob, Henner. "Vers la sécurisation des systèmes d'informatique ubiquitaire par le design : une approche langage." Thesis, Bordeaux 1, 2011. http://www.theses.fr/2011BOR14269/document.

Full text

Abstract:

Dans de multiples domaines, un nombre grandissant d'applications interagissant avec des entités communicantes apparaissent dans l'environnement pour faciliter les activités quotidiennes~(domotique et télémédecine). Leur impact sur la vie de tous les jours des utilisateurs rend ces applications critiques: leur défaillance peut mettre en danger des personnes et leurs biens. Bien que l'impact de ces défaillances puisse être majeur, la sécurité est souvent considérée comme un problème secondaire dans le processus de développement et est traitée par des approches ad hoc.Cette thèse propose d'intégrer des aspects de sécurité dans le cycle de développement des systèmes d'informatique ubiquitaire. La sécurité est spécifiée à la conception grâce à des déclarations dédiées et de haut niveau. Ces déclarations sont utilisées pour générer un support de programmation afin de faciliter l'implémentation des mécanismes de sécurité, tout en séparant ces aspects de sécurité de la logique applicative. Notre approche se concentre sur le contrôle d'accès aux entités et la protection de la vie privée. Notre travail a été implémenté et fait levier sur une suite outillée existante couvrant le cycle de développement logiciel
A growing number of environments is being populated with a range of networked devices. Applications leverage these devices to support everyday activities in a variety of areas (e.g., home automation and patient monitoring). As these devices and applications get woven into our everyday activities, they become critical: their failure can put people and assets at risk. Failures can be caused by malicious attacks and misbehaving applications. Although the impact of such situations can be major, security concerns are often considered a secondary issue in the development process, and treated with ad hoc approaches. This thesis proposes to address security concerns throughout the development lifecycle of a pervasive computing system. Security is addressed at design time thanks to dedicated, high-level declarations. These declarations are processed to implement security mechanisms, and to generate programming support to ease the development of the security logic, while keeping it separate from the application logic. Our approach is studied in the context of access control and privacy concerns. Our work has been implemented and leverages an existing software-design language and a suite of tools that covers the software development lifecycle

APA, Harvard, Vancouver, ISO, and other styles

42

Benayoun, Vincent. "Analyse de dépendances ML pour les évaluateurs de logiciels critiques." Electronic Thesis or Diss., Paris, CNAM, 2014. http://www.theses.fr/2014CNAM0915.

Full text

Abstract:

Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes
Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis

APA, Harvard, Vancouver, ISO, and other styles

43

Lahbib, Asma. "Distributed management framework based on the blockchain technology for industry 4.0 environments." Electronic Thesis or Diss., Institut polytechnique de Paris, 2020. http://www.theses.fr/2020IPPAS017.

Full text

Abstract:

En raison de l'avancement technologique dans les domaines des communications sans fil ainsi que ceux de l’informatique mobile et embarquée, les frontières entre les mondes physique et digital se rétrécissent pour introduire une nouvelle technologie également appelée l’internet des objets. Cette technologie est en train de devenir une partie intégrante de nos vies. Allant des capteurs de puissance et capabilités réduites, aux Appareils électroménagers intelligents et objets de télé santé jusqu’aux usines interconnectées et intelligentes dans lesquelles les employés, les machines, les processus, les services et même les produits interagissent de manière à fournir une meilleure adaptabilité dans la production ainsi qu’une allocation plus efficace des ressources, et ce, pour répondre plus rapidement au marché, d’une façon plus personnalisée et à moindre coût. L'intégration de ces technologies dans l'environnement et les processus de fabrication en combinaison avec d'autres technologies telles que le cloud computing, les systèmes physiques cybernétiques, les technologies de l'information et de la communication ainsi que l’analyse des données et l’intelligence artificielle a introduit la quatrième révolution industrielle appelée également Industrie 4.0. Dans ce futur monde, les machines parleront aux machines (M2M) pour organiser la production et coordonner leurs actions en fonction des informations collectées et échangées entre les différents capteurs et entités. Cependant, l'ouverture de la connectivité au monde externe soulève plusieurs questions sur la sécurité des données qui n'étaient pas un problème lorsque les appareils étaient contrôlés localement et que seuls quelques-uns d'entre eux étaient connectés à d'autres systèmes distants. Les risques de sécurité de tels objets représentent des ressources potentielles pour des acteurs malveillants. Une fois compromises, ces ressources peuvent être utilisées dans des attaques à large échelle contre d’autres systèmes. C’est pourquoi il est essentiel d’assurer une communication sécurisée entre les différents appareils hétérogènes déployés dans des environnements dynamiques et décentralisés pour protéger les informations échangées contre le vol ou la falsification par des cyber attaquants malveillants et par conséquent obtenir l'acceptation des utilisateurs de telles solutions. Dans cette direction, cette thèse est concentrée sur quatre questions complémentaires, principalement (1) la Gestion dynamique, basée sur la confiance de l'accès aux ressources partagées au sein d'un système distribué et collaboratif de l’industrie 4.0, (2) le protection des données personnelles et sensibles des utilisateurs tout au long des procédures de gestion d’accès et tout en éliminant le besoin de s'appuyer sur des tiers supplémentaires, (3) la vérification de la sécurité ainsi que l'exactitude fonctionnelle du cadre conçu et enfin (4) l'évaluation de degré de confiance fiabilité des parties en interaction en plus du stockage sécurisé des informations relatives afin de garantir leur confidentialité, intégrité et traçabilité. En se concentrant sur ces questions et en tenant compte des caractéristiques conventionnelles des environnements IoT et IIoT, nous avons proposé dans cette thèse un environnement générique sécurisé et décentralisé de gestion des ressources dans les environnements Industrie 4.0. Le cadre spécifié basé sur la technologie blockchain et piloté par un réseau peer to peer permet non seulement la gestion dynamique d’accès aux ressources partagées mais aussi la gouvernance distribuée du système, la protection de vie privée, la gestion de confiance et la vérification formelle des spécifications établies afin de valider leur respect des spécifications établies. Enfin, une conception et mise en œuvre de la plateforme est assurée afin de prouver sa faisabilité et d'analyser ses performances
The evolution of the Internet of Things (IoT) started decades ago as part of the first face of the digital transformation, its vision has further evolved due to a convergence of multiple technologies, ranging from wireless communication to the Internet and from embedded systems to micro-electromechanical systems. As a consequence thereof, IoT platforms are being heavily developed, smart factories are being planned to revolutionize the industry organization and both security and trust requirements are becoming more and more critical. The integration of such technologies within the manufacturing environment and processes in combination with other technologies has introduced the fourth industrial revolution referred to also as Industry 4.0. In this future world machines will talk to machines (M2M) to organize the production and coordinate their actions. However opening connectivity to the external world raises several questions about data and IT infrastructure security that were not an issue when devices and machines were controlled locally and just few of them were connected to some other remote systems. That’s why ensuring a secure communication between heterogeneous and reliable devices is essential to protect exchanged information from being stolen or tampered by malicious cyber attackers that may harm the production processes and put the different devices out of order. Without appropriate security solutions, these systems will never be deployed globally due to all kinds of security concerns. That’s why ensuring a secure and trusted communication between heterogeneous devices and within dynamic and decentralized environments is essential to achieve users acceptance and to protect exchanged information from being stolen or tampered by malicious cyber attackers that may harm the production processes and put the different devices out of order. However, building a secure system does not only mean protecting the data exchange but it requires also building a system where the source of data and the data itself is being trusted by all participating devices and stakeholders. In this thesis our research focused on four complementary issues, mainly (I) the dynamic and trust based management of access over shared resources within an Industry 4.0 based distributed and collaborative system, (ii) the establishment of a privacy preserving solution for related data in a decentralized architecture while eliminating the need to rely on additional third parties, (iii) the verification of the safety, the correctness and the functional accuracy of the designed framework and (iv) the evaluation of the trustworthiness degree of interacting parties in addition to the secure storage and sharing of computed trust scores among them in order to guarantee their confidentiality, integrity and privacy. By focusing on such issues and taking into account the conventional characteristics of both IoT and IoT enabled industries environments, we proposed in this thesis a secure and distributed framework for resource management in Industry 4.0 environments. The proposed framework, enabled by the blockchain technology and driven by peer to peer networks, allows not only the dynamic access management over shared resources but also the distribute governance of the system without the need for third parties that could be their-selves vulnerable to attacks. Besides and in order to ensure strong privacy guarantees over the access control related procedures, a privacy preserving scheme is proposed and integrated within the distributed management framework. Furthermore and in order to guarantee the safety and the functional accuracy of our framework software components, we focused on their formal modeling in order to validate their safety and compliance with their specification. Finally, we designed and implemented the proposal in order to prove its feasibility and analyze its performances

APA, Harvard, Vancouver, ISO, and other styles

44

Szlifierski, Nicolas. "Contrôle sûr de chaînes d'obfuscation logicielle." Thesis, Ecole nationale supérieure Mines-Télécom Atlantique Bretagne Pays de la Loire, 2020. http://www.theses.fr/2020IMTA0223.

Full text

Abstract:

L’obfuscation de code est une technique de protection de programme qui consiste à rendre la rétro-ingénierie d’un programme plus difficile, afin de protéger des secrets, de la propriété intellectuelle, ou de compliquer la détection (malware). L’obfuscation est généralement effectuée à l’aide d’un ensemble de transformations sur le programme cible. L’obfuscation est également souvent utilisée en conjonction avec d’autres techniques de protection de programmes telles que le watermarking ou le tamperproofing. Ces transformations sont généralement intégrées dans les transformations de code appliquées pendant le processus de compilation, comme les optimisations. Cependant, appliquer des transformations d’obfuscation demande plus de préconditions sur le code et de précisions dans l’application pour offrir un compromis performance/sécurité acceptable ce qui rend les compilateurs traditionnels peu adaptés à l’obfuscation. Pour répondre à ces problèmes, cette thèse propose SCOL, un langage qui permet de décrire le processus de compilation d’un programme en prenant en compte les problématiques spécifiques à l’obfuscation. Celui-ci permet de décrire des chaînes de compilation avec un haut niveau d’abstraction, tout en permettant une précision élevée sur la composition des transformations. Le langage possède un système de types qui permet de vérifier la cohérence de la chaîne de compilation. C’est-à-dire que vérifier que la composition des transformations permet d’obtenir le niveau de protection et de couverture visé
Code obfuscation is a software protection technique that is designed to make reverse engineering a program more challenging, in order to protect secrets, intellectual property, or to complicate detection (malware). The obfuscation is generally carried out using a set of transformations on the target program. Obfuscation is also often used in conjunction with other software protection techniques, such as watermarking or tamperproofing. These transformations are usually integrated into code transformations applied during the compilation process, such as optimisations. However, the application of obfuscation transformations requires more preconditions on the code and more precision in the application to provide an acceptable performance/safety trade-off, making traditional compilers unsuitable for obfuscation. To address these problems, this thesis presents SCOL, a language that is able to describe the process of compiling a program while considering the specific problems of obfuscation. This allows you to describe compilation chains with a high level of abstraction, while allowing a high degree of accuracy on the composition of the transformations. The language has a type system which checks the correctness of the compilation chain. That means that the composition of transformations provides the targeted level of protection and coverage

APA, Harvard, Vancouver, ISO, and other styles

45

Bel, Hadj Aissa Nadia. "Maîtrise du temps d'exécution de logiciels déployés dans des dispositifs personnels de confiance." Thesis, Lille 1, 2008. http://www.theses.fr/2008LIL10133/document.

Full text

Abstract:

La prolifération de petits équipements ouverts tels que les dispositifs personnels de confiance a favorisé l'essor des environnements d'exécution dynamiquement adaptables. Ainsi, de nouveaux logiciels peuvent être déployés à la volée après que les équipements soient délivrés à leurs porteurs. Par nos travaux, nous aspirons à garantir que chaque nouveau logiciel, dont le déploiement aboutit, est en mesure de délivrer les réponses aux requêtes qui lui sont adressées dans un délai maximal préalablement établi. Les garanties apportées sont cruciales tant en terme de sûreté de fonctionnement que de sécurité. À cet effet, nous avons proposé de distribuer le calcul du temps d'exécution au pire cas à la manière des approches de codes porteurs de preuve. Le fournisseur de code se voit attribuer les calculs gourmands en ressources matérielles ne supposant aucune connaissance préalable de l'environnement d'exécution sur lequel s'exécutera son logiciel, en l'occurrence la détermination des bornes des boucles. Quant au consommateur, il vérifie grâce à la preuve les bornes inférées par le fournisseur et calcule le temps d'exécution au pire cas. Nous avons évalué expérimentalement le bien-fondé de notre démarche sur une architecture matérielle et logicielle répondant aux exigences des dispositifs personnels de confiance. Enfin, nous nous sommes préoccupés du cas où plusieurs logiciels, émanant d'entité différentes, coexistent. Nous avons mis l'accent sur l'impact de l'interaction entre ces logiciels sur les garanties préalablement apportées par le système sur le temps d'exécution au pire cas et nous avons ébauché une solution basée sur les contrats pour maintenir ces garanties
The proliferation of small and open objects such as personal trusted devices has encouraged the spread of dynamically adaptable runtime environments. Thus, new software can be deployed on the fly after the devices are delivered to their holders. Through our work, we aim to ensure that each new software, whose deployment is successful, will be able to deliver responses within a maximum delay previously established. These guarantees are crucial in terms of safety and security. To this end, we propose to distribute the computation of worst case execution time. Our solution embraces a proof carrying code approach making distinction between a powerful but untrusted computer used to produce the code, and a safe but resource constrained code consumer. The producer does not assume any prior knowledge of the runtime environment on which its software will be executed. The code is statically analyzed to extract loop bounds and a proof containing this information is joint to the software. By a straightforward inspection of the code, the consumer can verify the validity of the proof and compute the global worst case execution time. We experimentally validate our approach on a hardware and software architecture which meets the requirements of trusted personal devices. Finally, we address the challenges raised when software from different service providers potentially untrusted can coexist and interact in a single device. We focus on the impact of the interaction between different software units on the guarantees previously given by the system on the worst case execution time and we outline a solution based on contracts to maintain these guarantees

APA, Harvard, Vancouver, ISO, and other styles

46

Boulanger, Jean-Louis. "Expression et validation des propriétés de sécurité logique et physique pour les systèmes informatiques critiques." Compiègne, 2006. http://www.theses.fr/2006COMP1622.

Full text

Abstract:

Dans le cadre de nos activités de recherche, nous nous sommes intéressés à la mise en sécurité des systèmes dits critiques (pouvant en cas de défaillance causer des dommages sérieux aux personnes ou aux biens). La mise en sécurité de tels systèmes passe par l'expression de recommandations liées à la sécurité. Ces recommandations peuvent provenir d'une demande du client (clauses du cahier des charges), de l'état de l'art, d'un référentiel légal (normes, décrets, arrêtés,. . ) ou d'études sur les conséquences des défaillances du système sur l'environnement, les personnes, l'image de marque de l'entreprise, etc. À partir des recommandations introduites dans le cahier des charges du client, il est donc possible d'identifier des "exigences". Il faudra alors démontrer que ces exigences sont prises en compte sur l'ensemble du cycle de réalisation du système. Dans le cadre de cette thèse, nous proposons une méthode et des exemples de mise en œuvre qui se basent sur l'identification, l'expression et la vérification des exigences liées à la sécurité
Within the framework of our research activities, we were interested in the safety of critical systems (whose failure can cause serious damage to people, goods or environment). The design of the safety of such systems requires the expression of safety-related recommendations. These recommendations can come from requirements of the customer (contractual clauses), from the state of the art, from legal reference frame (standards, decrees, laws) or from studies of the consequences of the failures on the system, the people, the environment. Starting from the safety recommendations coming from contractual conditions of the customer, it is thus possible to identify "safety requirements". It will have then to be proved that these safety requirements are taken into account during the whole design and lifecycle of the system. Within the framework of this thesis, we propose a method and implementation examples, which are based on the identification, the expression and the verification of the safety requirements

APA, Harvard, Vancouver, ISO, and other styles

47

Benaïssa, Nazim. "La composition des protocoles de sécurité avec la méthode B événementielle." Thesis, Nancy 1, 2010. http://www.theses.fr/2010NAN10034/document.

Full text

Abstract:

De nos jours, la présence de réseaux à grande échelle dans notre société bouleverse nos habitudes avec l'apparition de nouveaux services distants avec des besoins en matière de sécurité de plus en plus important. Nous abordons dans cette thèse la problématique de la composition des protocoles de sécurité, nous nous focalisons notamment sur les protocoles cryptographiques ainsi que sur les politiques de contrôle d'accès. La première partie de la thèse est consacrée à la composition des protocoles cryptographiques ainsi que leurs intégration avec d'autres types de protocoles. Nous introduisons notamment la notion de mécanismes cryptographiques qui sont des protocoles cryptographiques simples qui peuvent être composés pour obtenir des protocoles plus complexes sous réserve de faire les preuves nécessaires. Nous proposons également une méthode pour la reconstitution d'éventuelles attaques. La seconde partie de la thèse est consacrée à l'implémentation des politiques de contrôle d'accès par le raffinement, l'idée consiste à partir de politiques de sécurité abstraites et de les raffiner afin d'obtenir des politiques plus concrètes. Nous proposons également de combiner la technique de raffinement avec la technique de composition pour rendre plus efficace la procédure d'implémentation des politiques de contrôle d'accès
The presence of big scale networks in our modern society is affecting our usual practice, which as a result is generating the need to introduce a more and more important level of remote security services. We address in this thesis the problem of security protocols composition, we focus in particular on cryptographic protocols as well as access control policies. The first part of the thesis is dedicated to the composition of cryptographic protocols and to their integration other classes of protocols. We introduce the notion of cryptographic mechanisms. Mechanisms are simple cryptographic protocols that can be composed to obtain more complex protocols if the necessary proof obligations are discharged. We also introduce a technique for a proof based attack reconstruction. The second part of the thesis is dedicated to the deployment of access control policies using refinement, the idea consists in refining abstract policies to obtain a more concrete access control policies. We also propose to combine the refinement technique with the composition technique to obtain a more efficient access control policies deployment techniques

APA, Harvard, Vancouver, ISO, and other styles

48

Palisse, Aurélien. "Analyse et détection de logiciels de rançon." Thesis, Rennes 1, 2019. http://www.theses.fr/2019REN1S003/document.

Full text

Abstract:

La thèse s'intéresse aux logiciels de rançon, présente une plateforme d'analyse automatique et propose des contre-mesures. Nos contre-mesures sont conçues pour être temps réel et déployées sur une machine, c'est-à-dire ''End-Hosts''. En 2013 les logiciels de rançon font de nouveau parler d'eux, pour finalement devenir une des menaces les plus sérieuses à partir de 2015. Un état de l'art détaillé des contre-mesures existantes est fourni. On peut ainsi situer les contributions de cette thèse par rapport à la littérature. Nous présentons également une plateforme d'analyse automatique de logiciels malveillants composée de machines nues. L'objectif est de ne pas altérer le comportement des échantillons analysés. Une première contre-mesure basée sur l'utilisation d'une librairie cryptographique par les logiciels de rançon est proposée. Celle-ci peut être facilement contournée. Nous proposons donc une seconde contre-mesure générique et agnostique. Cette fois, des indicateurs de compromission sont utilisés pour analyser le comportement des processus sur le système de fichiers. Nous détaillons comment de manière empirique nous avons paramétré cette contre-mesure pour la rendre~: utilisable et efficace. Un des challenges de cette thèse étant de faire concilier performance, taux de détection et un faible taux de faux positifs. Enfin, les résultats d'une expérience utilisateur sont présentés. Cette expérience analyse le comportement des utilisateurs face à une menace. En dernière partie, nous proposons des améliorations à nos contributions mais aussi des pistes à explorer
This phD thesis takes a look at ransomware, presents an autonomous malware analysis platform and proposes countermeasures against these types of attacks. Our countermeasures are real-time and are deployed on a machine (i.e., end-hosts). In 2013, the ransomware become a hot subject of discussion again, before becoming one of the biggest cyberthreats beginning of 2015. A detailed state of the art for existing countermeasures is included in this thesis. This state of the art will help evaluate the contribution of this thesis in regards to the existing current publications. We will also present an autonomous malware analysis platform composed of bare-metal machines. Our aim is to avoid altering the behaviour of analysed samples. A first countermeasure based on the use of a cryptographic library is proposed, however it can easily be bypassed. It is why we propose a second generic and agnostic countermeasure. This time, compromission indicators are used to analyse the behaviour of process on the file system. We explain how we configured this countermeasure in an empiric way to make it useable and effective. One of the challenge of this thesis is to collate performance, detection rate and a small amount of false positive. To finish, results from a user experience are presented. This experience analyses the user's behaviour when faced with a threat. In the final part, I propose ways to enhance our contributions but also other avenues that could be explored

APA, Harvard, Vancouver, ISO, and other styles

49

Louboutin, Etienne. "Sensibilité de logiciels au détournement de flot de contrôle." Thesis, Ecole nationale supérieure Mines-Télécom Atlantique Bretagne Pays de la Loire, 2021. http://www.theses.fr/2021IMTA0230.

Full text

Abstract:

La sécurité d'un logiciel peut être prise en compte dès la conception. Cette approche, appelée security by design, permet d'influer au plus tôt de la conception pour influer sur l'architecture d'un logiciel. Les protections contre les attaques par détournement de flot d'exécution, comme le return oriented programming, ne sont pas pensées pour changer la manière de concevoir un logiciel, mais permettent de protéger un logiciel soit lors de sa compilation soit en travaillant directement sur le binaire produit. Dans cette thèse, nous proposons des métriques permettant à un développeur d'évaluer la sensibilité d'un logiciel face aux attaques par détournement de flot d'exécution. Pour aider le développement, les métriques définies permettent d'identifier les paramètres de production de binaires d'un logiciel qui entrainent une sensibilité accrue à ces attaques. L'utilisation de ces métriques sont illustrées dans cette thèse en étudiant l'influence de compilateurs et de leurs options, de langages et architectures matérielles
The security of a software can be taken into account right from the design stage. This approach, called security by design, allows to influence as early as possible the design to influence the architecture of a software. The protections against control flow hijacks, such as return oriented programming, are not designed to change the way of designing the software. They often aim to protect a software either during its compilation or by working directly on the binary produced. In this thesis, we propose metrics allowing a developer to evaluate the sensitivity of a software program to attacks by control flow hijacks. To ease development, metrics defined allow to identify the parameters used in the production of binaries of a software that result in increased sensitivity to these attacks. The use of of these metrics are illustrated in this thesis by studying the influence of compilers and their options, languages and hardware architectures

APA, Harvard, Vancouver, ISO, and other styles

50

Vu, Son Tuan. "Optimizing Property-Preserving Compilation." Electronic Thesis or Diss., Sorbonne université, 2021. http://www.theses.fr/2021SORUS435.

Full text

Abstract:

Afin d’assurer des garanties sécuritaires des applications binaires, des analyses et vérifications doivent avoir lieu au niveau binaire. Ces analyses et vérifications nécessitent des propriétés de sécurité ou fonctionnelles des applications. Il est donc nécessaire de transporter et transposer ces propriétés portant sur le code source au niveau du code compilé. La préservation de propriétés tout au long du flot de compilation est un problème difficile à cause des optimisations qui réorganisent les calculs ou éliminent les variables inutiles. Cette thèse présente des approches permettant de propager et préserver des propriétés tout au long d’un flot de compilation optimisant sans modifier les passes d’optimisation du compilateur. Dans l’implémentation dans LLVM, les propriétés sont émises dans le code binaire sous forme d’information de débug DWARF permettant leur utilisation par des outils d’analyse binaire. Les mécanismes proposés peuvent être utilisés pour préserver des protections insérées dans le code source tout en activant les optimisations du compilateur
In order to ensure security guarantees of binary applications, program analyses and verifications have to be performed at the binary level. These analyses and verifications require various security or functional properties about the program being analyzed. It is thus necessary to propagate these properties,usually expressed in the source level, down to binary code. However, preserving these properties throughout the optimizing compilation flow is hard due to code optimizations which reorder computations or eliminate unused variables. This thesis presents different approaches to preserve and propagate program properties throughout the optimizing compilation flow with minimal changes to individual transformation passes. In the implementations in LLVM, properties are emitted into executable binaries as DWARF debug information, which can next beused by binary analysis tools. Our mechanisms can be applied to address the problem of preserving security protections inserted at the source level, compiled with optimizations enabled

APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic 'Logiciel – Mesures de sûreté'

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