Дисертації: "Analyse des logiciels malveillants"

1

Calvet, Joan. "Analyse Dynamique de Logiciels Malveillants." Phd thesis, Université de Lorraine, 2013. http://tel.archives-ouvertes.fr/tel-00922384.

Повний текст джерела

Анотація:

L'objectif de cette thèse est le développement de méthodes de compréhension des logiciels malveillants, afin d'aider l'analyste humain à mieux appréhender cette menace. La première réalisation de cette thèse est une analyse à grande échelle et en profondeur des protections de logiciels malveillants. Plus précisément, nous avons étudié des centaines d'exemplaires de logiciels malveillants, soigneusement sélectionnés pour leur dangerosité. En mesurant de façon automatique un ensemble de caractéristiques originales, nous avons pu alors montrer l'existence d'un modèle de protection particulièrement prévalent dans ces programmes, qui est basé sur l'auto modification du code et sur une limite stricte entre code de protection et code utile. Ensuite, nous avons développé une méthode d'identification d'implémentations cryptographiques adaptée aux programmes en langage machine protégés. Nous avons validé notre approche en identifiant de nombreuses implémentations d'algorithmes cryptographiques -- dont la majorité sont complètement invisibles pour les outils existants --, et ceci en particulier dans des protections singulièrement obscures de logiciels malveillants. Finalement, nous avons développé ce qui est, à notre connaissance, le premier environnement d'émulation de réseaux de machines infectées avec plusieurs milliers de machines. Grâce à cela, nous avons montré que l'exploitation d'une vulnérabilité du protocole pair-à-pair du réseau Waledac permet de prendre son contrôle.

Стилі APA, Harvard, Vancouver, ISO та ін.

2

Thierry, Aurélien. "Désassemblage et détection de logiciels malveillants auto-modifiants." Thesis, Université de Lorraine, 2015. http://www.theses.fr/2015LORR0011/document.

Повний текст джерела

Анотація:

Cette thèse porte en premier lieu sur l'analyse et le désassemblage de programmes malveillants utilisant certaines techniques d'obscurcissement telles que l'auto-modification et le chevauchement de code. Les programmes malveillants trouvés dans la pratique utilisent massivement l'auto-modification pour cacher leur code utile à un analyste. Nous proposons une technique d'analyse hybride qui utilise une trace d'exécution déterminée par analyse dynamique. Cette analyse découpe le programme auto-modifiant en plusieurs sous-parties non auto-modifiantes que nous pouvons alors étudier par analyse statique en utilisant la trace comme guide. Cette seconde analyse contourne d'autres techniques de protection comme le chevauchement de code afin de reconstruire le graphe de flot de contrôle du binaire analysé. Nous étudions également un détecteur de programmes malveillants, fonctionnant par analyse morphologique : il compare les graphes de flot de contrôle d'un programme à analyser à ceux de programmes connus comme malveillants. Nous proposons une formalisation de ce problème de comparaison de graphes, des algorithmes permettant de le résoudre efficacement et détaillons des cas concrets d'application à la détection de similarités logicielles
This dissertation explores tactics for analysis and disassembly of malwares using some obfuscation techniques such as self-modification and code overlapping. Most malwares found in the wild use self-modification in order to hide their payload from an analyst. We propose an hybrid analysis which uses an execution trace derived from a dynamic analysis. This analysis cuts the self-modifying binary into several non self-modifying parts that we can examine through a static analysis using the trace as a guide. This second analysis circumvents more protection techniques such as code overlapping in order to recover the control flow graph of the studied binary. Moreover we review a morphological malware detector which compares the control flow graph of the studied binary against those of known malwares. We provide a formalization of this graph comparison problem along with efficient algorithms that solve it and a use case in the software similarity field

Стилі APA, Harvard, Vancouver, ISO та ін.

3

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

Повний текст джерела

Анотація:

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 та ін.

4

Beaucamps, Philippe. "Analyse de Programmes Malveillants par Abstraction de Comportements." Phd thesis, Institut National Polytechnique de Lorraine - INPL, 2011. http://tel.archives-ouvertes.fr/tel-00646395.

Повний текст джерела

Анотація:

L'analyse comportementale traditionnelle opère en général au niveau de l'implantation du comportement malveillant. Pourtant, elle s'intéresse surtout à l'identification d'un comportement donné, indépendamment de sa mise en œuvre technique, et elle se situe donc plus naturellement à un niveau fonctionnel. Dans cette thèse, nous définissons une forme d'analyse comportementale de programmes qui opère non pas sur les interactions élémentaires d'un programme avec le système mais sur la fonction que le programme réalise. Cette fonction est extraite des traces d'un programme, un procédé que nous appelons abstraction. Nous définissons de façon simple, intuitive et formelle les fonctionnalités de base à abstraire et les comportements à détecter, puis nous proposons un mécanisme d'abstraction applicable à un cadre d'analyse statique ou dynamique, avec des algorithmes pratiques à complexité raisonnable, enfin nous décrivons une technique d'analyse comportementale intégrant ce mécanisme d'abstraction. Notre méthode est particulièrement adaptée à l'analyse des programmes dans des langages de haut niveau ou dont le code source est connu, pour lesquels l'analyse statique est facilitée : les programmes conçus pour des machines virtuelles comme Java ou .NET, les scripts Web, les extensions de navigateurs, les composants off-the-shelf. Le formalisme d'analyse comportementale par abstraction que nous proposons repose sur la théorie de la réécriture de mots et de termes, les langages réguliers de mots et de termes et le model checking. Il permet d'identifier efficacement des fonctionnalités dans des traces et ainsi d'obtenir une représentation des traces à un niveau fonctionnel ; il définit les fonctionnalités et les comportements de façon naturelle, à l'aide de formules de logique temporelle, ce qui garantit leur simplicité et leur flexibilité et permet l'utilisation de techniques de model checking pour la détection de ces comportements ; il opère sur un ensemble quelconque de traces d'exécution ; il prend en compte le flux de données dans les traces d'exécution ; et il permet, sans perte d'efficacité, de tenir compte de l'incertitude dans l'identification des fonctionnalités. Nous validons nos résultats par un ensemble d'expériences, menées sur des codes malicieux existants, dont les traces sont obtenues soit par instrumentation binaire dynamique, soit par analyse statique.

Стилі APA, Harvard, Vancouver, ISO та ін.

5

Lebel, Bernard. "Analyse de maliciels sur Android par l'analyse de la mémoire vive." Master's thesis, Université Laval, 2018. http://hdl.handle.net/20.500.11794/29851.

Повний текст джерела

Анотація:

Les plateformes mobiles font partie intégrante du quotidien. Leur flexibilité a permis aux développeurs d’applications d’y proposer des applications de toutes sortes : productivité, jeux, messageries, etc. Devenues des outils connectés d’agrégation d’informations personnelles et professionnelles, ces plateformes sont perçues comme un écosystème lucratif par les concepteurs de maliciels. Android est un système d’exploitation libre de Google visant le marché des appareils mobiles et est l’une des cibles de ces attaques, en partie grâce à la popularité de celuici. Dans la mesure où les maliciels Android constituent une menace pour les consommateurs, il est essentiel que la recherche visant l’analyse de maliciels s’intéresse spécifiquement à cette plateforme mobile. Le travail réalisé dans le cadre de cette maîtrise s’est intéressé à cette problématique, et plus spécifiquement par l’analyse de la mémoire vive. À cette fin, il a fallu s’intéresser aux tendances actuelles en matière de maliciels sur Android et les approches d’analyses statiques et dynamiques présentes dans la littérature. Il a été, par la suite, proposé d’explorer l’analyse de la mémoire vive appliquée à l’analyse de maliciels comme un complément aux approches actuelles. Afin de démontrer l’intérêt de l’approche pour la plateforme Android, une étude de cas a été réalisée où un maliciel expérimental a été conçu pour exprimer les comportements malicieux problématiques pour la plupart des approches relevées dans la littérature. Une approche appelée l’analyse différentielle de la mémoire vive a été présentée afin de faciliter l’analyse. Cette approche utilise le résultat de la différence entre les éléments présents après et avant le déploiement du maliciel pour réduire la quantité d’éléments à analyser. Les résultats de cette étude ont permis de démontrer que l’approche est prometteuse en tant que complément aux approches actuelles. Il est recommandé qu’elle soit le sujet d’études subséquentes afin de mieux détecter les maliciels sur Android et d’en automatiser son application.
Mobile devices are at the core of modern society. Their versatility has allowed third-party developers to generate a rich experience for the user through mobile apps of all types (e.g. productivity, games, communications). As mobile platforms have become connected devices that gather nearly all of our personal and professional information, they are seen as a lucrative market by malware developers. Android is an open-sourced operating system from Google targeting specifically the mobile market and has been targeted by malicious activity due the widespread adoption of the latter by the consumers. As Android malwares threaten many consumers, it is essential that research in malware analysis address specifically this mobile platform. The work conducted during this Master’s focuses on the analysis of malwares on the Android platform. This was achieved through a literature review of the current malware trends and the approaches in static and dynamic analysis that exists to mitigate them. It was also proposed to explore live memory forensics applied to the analysis of malwares as a complement to existing methods. To demonstrate the applicability of the approach and its relevance to the Android malwares, a case study was proposed where an experimental malware has been designed to express malicious behaviours difficult to detect through current methods. The approach explored is called differential live memory analysis. It consists of analyzing the difference in the content of the live memory before and after the deployment of the malware. The results of the study have shown that this approach is promising and should be explored in future studies as a complement to current approaches.

Стилі APA, Harvard, Vancouver, ISO та ін.

6

Puodzius, Cassius. "Data-driven malware classification assisted by machine learning methods." Electronic Thesis or Diss., Rennes 1, 2022. https://ged.univ-rennes1.fr/nuxeo/site/esupversions/3dabb48c-b635-46a5-bcbe-23992a2512ec.

Повний текст джерела

Анотація:

Historiquement, l'analyse des logiciels malveillants (ou MW) a fortement fait appel au savoir-faire humain pour la création manuelle de signatures permettant de détecter et de classer les MW. Cette procédure est très coûteuse et prend beaucoup de temps, ce qui ne permet pas de faire face aux scénario modernes de cybermenaces. La solution consiste à automatiser largement l'analyse des MW. Dans ce but, la classification des MW permet d'optimiser le traitement de grands corpus de MW en identifiant les ressemblances entre des instances similaires. La classification des MW est donc une activité clé liée à l'analyse des MW. Cette thèse aborde le problème de la classification des MW en adoptant une approche pour laquelle l'intervention humaine est évitée autant que possible. De plus, nous contournons la subjectivité inhérente à l'analyse humaine en concevant la classification uniquement à partir de données directement issues de l'analyse des MW, adoptant ainsi une approche dirigée par les données. Notre objectif est d'améliorer l'automatisation de l'analyse des MW et de la combiner avec des méthodes d'apprentissage automatique capables de repérer et de révéler de manière autonome des points communs imprévisibles au sein des données. Nous avons échelonné notre travail en trois étapes. Dans un premier temps, nous nous sommes concentrés sur l'amélioration de l'analyse des MW et sur son automatisation, étudiant de nouvelles façons d'exploiter l'exécution symbolique dans l'analyse des MW et développant un cadre d'exécution distribué pour augmenter notre puissance de calcul. Nous nous sommes ensuite concentrés sur la représentation du comportement des MW, en accordant une attention particulière à sa précision et à sa robustesse. Enfin, nous nous sommes focalisés sur le partitionnement des MW, en concevant une méthodologie qui qui ne restreint pas la combinaison des caractéristiques syntaxiques et comportementales, et qui monte bien en charge en pratique. Quant à nos principales contributions, nous revisitions l'usage de l'exécution symbolique pour l'analyse des MW en accordant une attention particulière à l'utilisation optimale des tactiques des solveurs SMT et aux réglages des hyperparamètres ; nous concevons un nouveau paradigme d'évaluation pour les systèmes d'analyse des MW ; nous formulons une représentation compacte du comportement sous la forme de graphe, ainsi qu'une fonction associée pour le calcul de la similarité par paire, qui est précise et robuste ; et nous élaborons une nouvelle stratégie de partitionnement des MW basée sur un partitionnement d'ensemble flexible en ce qui concerne la combinaison des caractéristiques syntaxiques et comportementales
Historically, malware (MW) analysis has heavily resorted to human savvy for manual signature creation to detect and classify MW. This procedure is very costly and time consuming, thus unable to cope with modern cyber threat scenario. The solution is to widely automate MW analysis. Toward this goal, MW classification allows optimizing the handling of large MW corpora by identifying resemblances across similar instances. Consequently, MW classification figures as a key activity related to MW analysis, which is paramount in the operation of computer security as a whole. This thesis addresses the problem of MW classification taking an approach in which human intervention is spared as much as possible. Furthermore, we steer clear of subjectivity inherent to human analysis by designing MW classification solely on data directly extracted from MW analysis, thus taking a data-driven approach. Our objective is to improve the automation of malware analysis and to combine it with machine learning methods that are able to autonomously spot and reveal unwitting commonalities within data. We phased our work in three stages. Initially we focused on improving MW analysis and its automation, studying new ways of leveraging symbolic execution in MW analysis and developing a distributed framework to scale up our computational power. Then we concentrated on the representation of MW behavior, with painstaking attention to its accuracy and robustness. Finally, we fixed attention on MW clustering, devising a methodology that has no restriction in the combination of syntactical and behavioral features and remains scalable in practice. As for our main contributions, we revamp the use of symbolic execution for MW analysis with special attention to the optimal use of SMT solver tactics and hyperparameter settings; we conceive a new evaluation paradigm for MW analysis systems; we formulate a compact graph representation of behavior, along with a corresponding function for pairwise similarity computation, which is accurate and robust; and we elaborate a new MW clustering strategy based on ensemble clustering that is flexible with respect to the combination of syntactical and behavioral features

Стилі APA, Harvard, Vancouver, ISO та ін.

7

Nisi, Dario. "Unveiling and mitigating common pitfalls in malware analysis." Electronic Thesis or Diss., Sorbonne université, 2021. http://www.theses.fr/2021SORUS528.

Повний текст джерела

Анотація:

L'importance des systèmes informatiques dans les sociétés modernes ne cesse de croître, tout comme les dommages causés par les logiciels malveillants. L'industrie de la sécurité et les auteurs de logiciels malveillants se sont engagés dans une course aux armements, dans laquelle les premiers créent de meilleurs systèmes de détection tandis que les seconds tentent de les contourner. En fait, toute hypothèse erronée (aussi subtile soit-elle) dans la conception d'un outil anti-malware peut créer de nouvelles voies pour échapper à la détection. Cette thèse se concentre sur deux aspects souvent négligés des techniques modernes d'analyse des logiciels malveillants : l'utilisation d'informations au niveau de l'API pour coder le comportement malveillant et la réimplémentation des routines d'analyse des formats de fichiers exécutables dans les outils orientés sécurité. Nous montrons qu'il est possible de tirer parti de ces pratiques à grande échelle et de manière automatisée. En outre, nous étudions la possibilité de résoudre ces problèmes à la racine, en mesurant les difficultés que les architectes anti-malware peuvent rencontrer et en proposant des stratégies pour les résoudre
As the importance of computer systems in modern-day societies grows, so does the damage that malicious software causes. The security industry and malware authors engaged in an arms race, in which the first creates better detection systems while the second try to evade them. In fact, any wrong assumption (no matter how subtle) in the design of an anti-malware tool may create new avenues for evading detection. This thesis focuses on two often overlooked aspects of modern malware analysis techniques: the use of API-level information to encode malicious behavior and the reimplementation of parsing routines for executable file formats in security-oriented tools. We show that taking advantage of these practices is possible on a large and automated scale. Moreover, we study the feasibility of fixing these problems at their roots, measuring the difficulties that anti-malware architects may encounter and providing strategies to solve them

Стилі APA, Harvard, Vancouver, ISO та ін.

8

Reynaud, Daniel. "Analyse de codes auto-modifiants pour la sécurité logicielle." Thesis, Vandoeuvre-les-Nancy, INPL, 2010. http://www.theses.fr/2010INPL049N/document.

Повний текст джерела

Анотація:

Les programmes auto-modifiants fonctionnent de manière singulière car ils sont capables de réécrire leur propre code en cours d'exécution. Absents des modèles de calcul théoriques, ils sont pourtant omniprésents dans les ordinateurs et les systèmes d'exploitations actuels. Ils sont en effet utilisés par les chargeurs d'amorçages, pour la compilation à la volée ou encore l'optimisation dynamique de code. Ils sont également omniprésents dans les programmes malveillants, dont les auteurs ont bien compris qu'ils constituaient des objets complexes à analyser. Ils sont également virtuellement présents dans tous les autres programmes mais de manière non-intentionnelle. En effet, on peut voir certaines classes de vulnérabilités, par exemple les failles par débordement de tampon, comme la possibilité d'exécuter accidentellement des données -- ce qui est un comportement caractéristique des programmes auto-modifiants.Au cours de cette thèse, nous avons proposé un modèle théorique permettant de caractériser un certain nombre de comportements auto-modifiants avancés. Nous avons également mis au point un prototype, TraceSurfer, permettant de détecter efficacement ces comportements à partir de l'analyse de traces et de les visualiser sous forme de graphes d'auto-référence. Enfin, nous avons validé par l'expérience à la fois le modèle théorique et l'outil en les testant sur un grand nombre de programmes malveillants
Self-modifying programs run in a very specific way: they are capable to rewrite their own code at runtime. Remarkably absent from theoretical computation models, they are present in every modern computer and operating system. Indeed, they are used by bootloaders, for just-in-time compilation or dynamic optimizations. They are also massively used by malware authors in order to bypass antivirus signatures and to delay analysis. Finally, they are unintentionally present in every program, since we can model code injection vulnerabilities (such as buffer overflows) as the ability for a program to accidentally execute data.In this thesis, we propose a formal framework in order to characterize advanced self-modifying behaviors and code armoring techniques. A prototype, TraceSurfer, allows us to detect these behaviors by using fine-grained execution traces and to visualize them as self-reference graphs. Finally, we assess the performance and efficiency of the tool by running it on a large corpus of malware samples

Стилі APA, Harvard, Vancouver, ISO та ін.

9

Lemay, Frédérick. "Instrumentation optimisée de code pour prévenir l'exécution de code malicieux." Thesis, Université Laval, 2012. http://www.theses.ulaval.ca/2012/29030/29030.pdf.

Повний текст джерела

Стилі APA, Harvard, Vancouver, ISO та ін.

10

Khoury, Raphaël. "Détection du code malicieux : système de type à effets et instrumentation du code." Thesis, Université Laval, 2005. http://www.theses.ulaval.ca/2005/23250/23250.pdf.

Повний текст джерела

Анотація:

Ce mémoire traite en premier lieu des avantages et des désavantages des différentes approches visant à assurer la sûreté et la sécurité des logiciels. En second lieu, il présente une nouvelle approche pour combiner l'analyse statique et l'analyse dynamique afin de produire une architecture de sécurité plus puissante. Les premiers chapitres du mémoire comportent une revue analytique des différentes approches statiques, dynamiques et hybrides qui peuvent être utilisées afin de sécuriser le code potentiellement malicieux. L'exposé identifie alors les avantages et les inconvénients de chaque approche ainsi que le champ des politiques de sécurité dans lesquels on peut l'appliquer. Le dernier chapitre traite de la possibilité de combiner l'analyse statique et l'analyse dynamique par une nouvelle approche hybride. Cette approche consiste à instrumenter le code seulement là où c'est nécessaire pour assurer satisfaire une politique de sécurité définie par l'usager et exprimée en un ensemble de propriétés exprimées μ-calcul modal. Cette instrumentation est guidée par une analyse statique effectuée à priori et basée sur un système de type à effets. Les effets représentent les accès aux ressources protégées du système.
The purpose of this thesis is twofold. In the first place it presents a comparative study of the advantages and drawbacks of several approaches to insure software safety and security. It then focuses more particularly on combining static analyses and dynamic monitoring in order to produce a more powerful security architecture. The first chapters of the thesis present an analytical review of the various static, dynamic and hybrid approaches that can be used to secure a potentially malicious code. The advantages and drawbacks of each approach are thereby analyzed and the field of security properties that can be enforced by using it are identified. The thesis then focuses on the possibility of combining static and dynamic analysis through a new hybrid approach. This approach consists in a code instrumentation, that only alters those parts of a program where it is necessary to do so to insure the respect of a user-defined security policy expressed in a set of modal μ-calculus properties. this instrumentation is guided by a static analysis based on a type and effect system. The effects represent the accesses made to pretested system ressources.

Стилі APA, Harvard, Vancouver, ISO та ін.

11

Freyssinet, Eric. "Lutte contre les botnets : analyse et stratégie." Thesis, Paris 6, 2015. http://www.theses.fr/2015PA066390/document.

Повний текст джерела

Анотація:

Les botnets, ou réseaux d’ordinateurs infectés par un code malveillant et connectés à un système de commande et de contrôle, constituent le premier outil de la délinquance sur Internet. Ils permettent de concrétiser le développement d’un nouveau type d’activités criminelles: le crime comme un service (CaaS). Ils constituent un défi en matière de répression. D’abord par l’importance de leur impact sur la sécurité des réseaux et la commission d’infractions sur Internet. Ensuite par la dimension extrêmement internationale de leur diffusion et donc une certaine difficulté à mener des investigations. Enfin, par le grand nombre des acteurs qui peuvent être impliqués (codeurs, maîtres de botnets, intermédiaires financiers). Cette thèse porte sur l’étude des botnets (composantes, fonctionnement, acteurs), la proposition d’une méthode de collecte de données sur les activités liées aux botnets et les dispositifs techniques et organisationnels de lutte contre les botnets ; elle conclut sur des propositions en matière de stratégie pour cette lutte. Les travaux menés ont permis de confirmer la pertinence, pour l’étude efficace des botnets, d’un modèle englobant l’ensemble de leurs composants, y compris les infrastructures et les acteurs. Outre un effort de définition, la thèse apporte un modèle complet du cycle de vie d’un botnet et propose des méthodes de catégorisation de ces objets. Il en ressort la nécessité d’une stratégie partagée qui doit comporter les éléments de détection, de coordination et la possibilité, voire l’obligation, pour les opérateurs de mettre en œuvre des mesures de mitigation
Botnets, or networks of computers infected with malware and connected to a command and control system, is one of the main tools for criminal activities on the Internet today. They allow the development of a new type of crime: crime as a service (CaaS). They are a challenge for law enforcement. First by the importance of their impact on the security of networks and the commission of crimes on the Internet. Next, with regards to the extremely international dimension of their dissemination and therefore the enhanced difficulty in conducting investigations. Finally, through the large number of actors that may be involved (software developers, botnet masters, financial intermediaries, etc.). This thesis proposes a thorough study of botnets (components, operation, actors), the specificaion of a data collection method on botnet related activities and finally the technical and organizational arrangements in the fight against botnets; it concludes on proposals on the strategy for this fight. The work carried out has confirmed the relevance, for the effective study of botnets, of a model encompassing all their components, including infrastructure and actors. Besides an effort in providing definitions, the thesis describes a complete model of the life cycle of a botnet and offers methods for categorization of these objects. This work shows the need for a shared strategy which should include the detection elements, coordination between actors and the possibility or even the obligation for operators to implement mitigation measures

Стилі APA, Harvard, Vancouver, ISO та ін.

12

Pektaş, Abdurrahman. "Behavior based malware classification using online machine learning." Thesis, Université Grenoble Alpes (ComUE), 2015. http://www.theses.fr/2015GREAM065/document.

Повний текст джерела

Анотація:

Les malwares, autrement dit programmes malicieux ont grandement évolué ces derniers temps et sont devenus une menace majeure pour les utilisateurs grand public, les entreprises et même le gouvernement. Malgré la présence et l'utilisation intensive de divers outils anti-malwares comme les anti-virus, systèmes de détection d'intrusions, pare-feux etc ; les concepteurs de malwares peuvent significativement contourner ses protections en utilisant les techniques d'offuscation. Afin de limiter ces problèmes, les chercheurs spécialisés dans les malwares ont proposé différentes approches comme l'exploration des données (data mining) ou bien l'apprentissage automatique (machine learning) pour détecter et classifier les échantillons de malwares en fonction de leur propriétés statiques et dynamiques. De plus les méthodes proposées sont efficaces sur un petit ensemble de malwares, le passage à l'échelle de ses méthodes pour des grands ensembles est toujours en recherche et n'a pas été encore résolu.Il est évident aussi que la majorité des malwares sont une variante des précédentes versions. Par conséquent, le volume des nouvelles variantes créées dépasse grandement la capacité d'analyse actuelle. C'est pourquoi développer la classification des malwares est essentiel pour lutter contre cette augmentation pour la communauté informatique spécialisée en sécurité. Le challenge principal dans l'identification des familles de malware est de réussir à trouver un équilibre entre le nombre d'échantillons augmentant et la précision de la classification. Pour surmonter cette limitation, contrairement aux systèmes de classification existants qui appliquent des algorithmes d'apprentissage automatique pour sauvegarder les données ; ce sont des algorithmes hors-lignes ; nous proposons une nouvelle classification de malwares en ligne utilisant des algorithmes d'apprentissage automatique qui peuvent fournir une mise à jour instantanée d'un nouvel échantillon de malwares en suivant son introduction dans le système de classification.Pour atteindre notre objectif, premièrement nous avons développé une version portable, évolutive et transparente d'analyse de malware appelée VirMon pour analyse dynamique de malware visant les OS windows. VirMon collecte le comportement des échantillons analysés au niveau bas du noyau à travers son pilote mini-filtre développé spécifiquement. Deuxièmement, nous avons mis en place un cluster de 5 machines pour notre module d'apprentissage en ligne ( Jubatus);qui permet de traiter une quantité importante de données. Cette configuration permet à chaque machine d'exécuter ses tâches et de délivrer les résultats obtenus au gestionnaire du cluster.Notre outil proposé consiste essentiellement en trois niveaux majeures. Le premier niveau permet l'extraction des comportements des échantillons surveillés et observe leurs interactions avec les ressources de l'OS. Durant cette étape, le fichier exemple est exécuté dans un environnement « sandbox ». Notre outil supporte deux « sandbox »:VirMon et Cuckoo. Durant le second niveau, nous appliquons des fonctionnalités d'extraction aux rapports d'analyses. Le label de chaque échantillon est déterminé Virustotal, un outil regroupant plusieurs anti-virus permettant de scanner en ligne constitués de 46 moteurs de recherches. Enfin au troisième niveau, la base de données de malware est partitionnée en ensemble de test et d'apprentissage. L'ensemble d'apprentissage est utilisé pour obtenir un modèle de classification et l'ensemble de test est utilisé pour l'évaluation.Afin de valider l'efficacité et l'évolutivité de notre méthode, nous l'avons évalué en se basant sur une base de 18 000 fichiers malicieux récents incluant des virus, trojans, backdoors, vers etc, obtenue depuis VirusShare. Nos résultats expérimentaux montrent que permet la classification de malware avec une précision de 92 %
Recently, malware, short for malicious software has greatly evolved and became a major threat to the home users, enterprises, and even to the governments. Despite the extensive use and availability of various anti-malware tools such as anti-viruses, intrusion detection systems, firewalls etc., malware authors can readily evade these precautions by using obfuscation techniques. To mitigate this problem, malware researchers have proposed various data mining and machine learning approaches for detecting and classifying malware samples according to the their static or dynamic feature set. Although the proposed methods are effective over small sample set, the scalability of these methods for large data-set are in question.Moreover, it is well-known fact that the majority of the malware is the variant of the previously known samples. Consequently, the volume of new variant created far outpaces the current capacity of malware analysis. Thus developing malware classification to cope with increasing number of malware is essential for security community. The key challenge in identifying the family of malware is to achieve a balance between increasing number of samples and classification accuracy. To overcome this limitation, unlike existing classification schemes which apply machine learning algorithm to stored data, i.e., they are off-line, we proposed a new malware classification system employing online machine learning algorithms that can provide instantaneous update about the new malware sample by following its introduction to the classification scheme.To achieve our goal, firstly we developed a portable, scalable and transparent malware analysis system called VirMon for dynamic analysis of malware targeting Windows OS. VirMon collects the behavioral activities of analyzed samples in low kernel level through its developed mini-filter driver. Secondly we set up a cluster of five machines for our online learning framework module (i.e. Jubatus), which allows to handle large scale of data. This configuration allows each analysis machine to perform its tasks and delivers the obtained results to the cluster manager.Essentially, the proposed framework consists of three major stages. The first stage consists in extracting the behavior of the sample file under scrutiny and observing its interactions with the OS resources. At this stage, the sample file is run in a sandboxed environment. Our framework supports two sandbox environments: VirMon and Cuckoo. During the second stage, we apply feature extraction to the analysis report. The label of each sample is determined by using Virustotal, an online multiple anti-virus scanner framework consisting of 46 engines. Then at the final stage, the malware dataset is partitioned into training and testing sets. The training set is used to obtain a classification model and the testing set is used for evaluation purposes .To validate the effectiveness and scalability of our method, we have evaluated our method on 18,000 recent malicious files including viruses, trojans, backdoors, worms, etc., obtained from VirusShare, and our experimental results show that our method performs malware classification with 92% of accuracy

Стилі APA, Harvard, Vancouver, ISO та ін.

13

Lespérance, Pierre-Luc. "Détection des variations d'attaques à l'aide d'une logique temporelle." Thesis, Université Laval, 2006. http://www.theses.ulaval.ca/2006/23481/23481.pdf.

Повний текст джерела

Анотація:

La principale contribution de ce travail est de proposer une nouvelle logique, inspirée de la logique temporelle linéaire, qui permet d'améliorer les techniques standard de détection d'intrusions utilisant l'approche par scénarios, avec la possibilité de détecter des variantes d'attaques connues. La logique suggées pourrait trouver une trace de paquets qui correspondent, même partiellement avec une distance calculée, avec la formule qui décrit l'attaque. La deuxième partie consistera à décrire son implémentation et de montrer la contribution pour augmenter la performance et l'expressivité des règles des systèmes de détection d'intrusions et plus précisément, du système Snort.

Стилі APA, Harvard, Vancouver, ISO та ін.

14

Ta, Thanh Dinh. "Modèle de protection contre les codes malveillants dans un environnement distribué." Thesis, Université de Lorraine, 2015. http://www.theses.fr/2015LORR0040/document.

Повний текст джерела

Анотація:

La thèse contient deux parties principales: la première partie est consacrée à l’extraction du format des messages, la deuxième partie est consacrée à l’obfuscation des comportements des malwares et la détection. Pour la première partie, nous considérons deux problèmes: "la couverture des codes" et "l’extraction du format des messages". Pour la couverture des codes, nous proposons une nouvelle méthode basée sur le "tainting intelligent" et sur l’exécution inversée. Pour l’extraction du format des messages, nous proposons une nouvelle méthode basée sur la classification de messages en utilisant des traces d’exécution. Pour la deuxième partie, les comportements des codes malveillants sont formalisés par un modèle abstrait pour la communication entre le programme et le système d’exploitation. Dans ce modèle, les comportements du programme sont des appels systèmes. Étant donné les comportements d’un programme bénin, nous montrons de façon constructive qu’il existe plusieurs programmes malveillants ayant également ces comportements. En conséquence, aucun détecteur comportemental n’est capable de détecter ces programmes malveillants
The thesis consists in two principal parts: the first one discusses the message for- mat extraction and the second one discusses the behavioral obfuscation of malwares and the detection. In the first part, we study the problem of “binary code coverage” and “input message format extraction”. For the first problem, we propose a new technique based on “smart” dynamic tainting analysis and reverse execution. For the second one, we propose a new method using an idea of classifying input message values by the corresponding execution traces received by executing the program with these input values. In the second part, we propose an abstract model for system calls interactions between malwares and the operating system at a host. We show that, in many cases, the behaviors of a malicious program can imitate ones of a benign program, and in these cases a behavioral detector cannot distinguish between the two programs

Стилі APA, Harvard, Vancouver, ISO та ін.

15

Lacasse, Alexandre. "Approche algébrique pour la prévention d'intrusions." Thesis, Université Laval, 2006. http://www.theses.ulaval.ca/2006/23379/23379.pdf.

Повний текст джерела

Анотація:

Dans ce travail, nous définissons une nouvelle algèbre de processus basée sur CCS. Cette algèbre, qui est destinée à la sécurisation formelle de réseaux, est munie d’un opérateur de surveillance qui permet de contrôler les entrées et les sorties d’un processus, ou d’un sous-processus, à l’image d’un pare-feu dans un réseau informatique. L’algèbre permet donc de modéliser des réseaux munis de moniteurs, et également, n’importe quel système communicant devant être contrôlé par des moniteurs. Avant d’entrer dans le vif du sujet, nous débutons par une revue des approches globales en détection d’intrusions, soient l’approche comportementale et l’approche par scénarios. Nous parcourons par la suite différents langages formels destinés à la modélisation de systèmes communicants, en prêtant une attention particulière aux algèbres de processus.

Стилі APA, Harvard, Vancouver, ISO та ін.

16

Ferrara, Pietro. "ANALYSE STATIQUE DE LOGICIELS MULTITÂCHES PAR INTERPRÉTATION ABSTRAITE." Phd thesis, Ecole Polytechnique X, 2009. http://tel.archives-ouvertes.fr/tel-00417502.

Повний текст джерела

Анотація:

Le but de cette thèse est de présenter une analyse statique générique pour des programmes multitâche écrits en Java.
Les programmes multitâche exécutent plusieurs tâches en parallèle. Ces tâches communiquent implicitement par le biais de la mémoire partagée et elles se synchonisent sur des moniteurs (les primitives wait-notify, etc..). Il y a quelques années, les architectures avec double processeurs ont commencé à être disponibles sur le marché à petit prix. Aujourd'hui, presque tous les ordinateurs ont au moins deux noyaux, la tendance actuelle du marché étant de mettre de plus en plus de processeurs par puce. Cette révolution amène également de nouveaux défis en matière de programmation, car elle demande aux développeurs d'implanter des programmes multitâche. Le multitâche est supporté en natif par la plupart des langages de programmation courants, comme Java et C#.
Le but de l'analyse statique est de calculer des informations sur le comportement d'un programme, de manière conservative et automatique. Une application de l'analyse statique est le développement d'outils qui aident au débogage des programmes. Plusieurs méthodes d'analyse statique ont été proposées. Nous suivrons le cadre de l'interprétation abstraite, une théorie mathématique permettant de définir des approximations correctes de sémantiques de programmes. Cette méthode a déjà été utilisée pour un large spectre de langages de programmation.
L'idée fondamentale des analyseurs statiques génériques est de développer un outils qui puissent être interfacé avec différents domaines numériques et différentes propriétés. Pendant ces dernières années, beaucoup de travaux se sont attaqués à cet enjeu, et ils ont été appliqué avec succès pour déboguer des logiciels industriels. La force de ces analyseurs réside dans le fait qu'une grande partie de l'analyse peut être réutilisée pour vérifier plusieurs propriétés. L'utilisation de différents domaines numériques permet le développement d'analyses plus rapides mais moins précises, ou plus lentes mais plus précises.

Dans cette thèse, nous présentons la conception d'un analyseur générique pour des programmes multitâche. Avant tout, nous définissons le modèle mémoire, appelé happens-before memory model. Puis, nous approximons ce modéle mémoire en une semantique calculable. Les modéles mémoire définissent les comportements autorisés pendant l'exé-cution d'un programme multitâche. Commençant par la définition (informelle) de ce modèle mémoire particulier, nous définissons une sémantique qui construit toutes les exécutions finies selon ce modèle mémoire. Une exécution d'un programme multitâche est décrite par une function qui associe les tâches à des séquences (ou traces) d'états. Nous montrons comment concevoir une sémantique abstraite calculable, et nous montrons formellement la correction des résultat de cette analyse.
Ensuite, nous définissons et approximons une nouvelle propriété qui porte sur les comportements non-déterministes causés par le multitâche, c'est à dire aux entrelacements arbitraires pendant l'exécution de differentes instructions de lecture. Avant tout, le non déterminisme d'un programme multitâche se définit par une différence entre plusieurs exécutions. Si deux exécutions engendrent des comportements différents dus au valeurs qui sont lues ou écrites en mémoire partagée, alors le programme est non déterministe. Nous approximons cette propriété en deux étapes: dans un premier temps, nous regroupons, pour chaque tâche, la valeur (abstraite) qui peut être écrite dans la mémoire partagée à un point de programme donné. Dans un deuxième temps, nous résumons toutes les valeurs pouvant être écrites en parallèle, tout en nous rapellant l'ensemble des tâches qui pourraient les avoir écrites. à un premier niveau d'approximation, nous introduisons un nouveau concept de déterminisme faible. Nous proposons par ailleurs d'autres manière affaiblir la propriété de déterminisme, par exemple par projection des traces et des états, puis nous définissons une hierarchie globale de ces affaiblissements. Nous étudions aussi comment la présence de conflit sur les accès des données peut affecter le déterminisme du programme.
Nous appliquons ce cadre de travail théorique à Java. En particulier, nous définissons une sémantique du language objet de Java, selon sa spécification. Ensuite, nous approximons cette sémantique afin de garder uniquement l'information qui est nécessaire pour l'analyse des programmes multitâche. Le cœur de cette abstraction est une analyse d'alias qui approxime les références afin d'identifier les tâches, de vérifier les accès en mémoire partagée, et de détecter quand deux tâches ont un moniteur commun afin d'en déduire quelles parties du code ne peuvent pas être éxécutées en parallèle.
L'analyseur générique qui est décrit ci-dessus a été entierement implanté, dans un outils appelé Checkmate. Checkmate est ainsi le premier analyseur générique pour des programmes multitâche écrits en Java. Des résultats expérimentaux sont donnés et analysés en détails. En particulier, nous étudions la précision de l'analyse lorsqu'elle est appliquée à des schémas courants de la programmation concurrente, ainsi qu'à d'autres exemples. Nous observons également les performances de l'analyse lorsqu'elle est appliquée à une application incrémentale, ainsi qu'à des exemples de références bien connus.
Une autre contribution de cette thèse est l'extension d'un analyseur générique existant qui s'appelle Clousot et qui permet de vérifier le non débordement des mémoires tampons. Il s'avère que cette analyse passe à l'échelle des programmes industriels et qu'elle est précise. En résumé, nous présentons une application d'un analyseur statique générique industriel existant pour détecter et prouver une propriété présentant un intérêt pratique, ce qui montre la puissance de cette approche dans le développement d'outils qui soient utiles pour les développeurs.

Стилі APA, Harvard, Vancouver, ISO та ін.

17

Chaabane, Rim. "Analyse et optimisation de patterns de code." Paris 8, 2011. http://www.theses.fr/2011PA084174.

Повний текст джерела

Анотація:

Our work is performed in the context of a financial company that develops and maintains legacy software. This software has been existing for more than twenty years, it was written in a proprietary, procedural and 4GL language called ADL (or Application Development Language). This software was initially developed for VMS system and deals with old generation of DBMS. For commercial reasons, the software has been ported to UNIX systems and to new RDBMS; Oracle and Sybase. It has also been extended to offer web interfaces. This legacy software has to face some new challenges as databases grow. During these last 20 years, some phenomenons like the merging of two companies, make data grow up to more than 1Terabyte and will reach 1Petabyte in a few years. In these new contexts, the ADL language shows limits to handle such a mass of data. Some patterns of code with database access have been suspected to be responsible for important decrease in performance. Our work consists in detecting all the instances of a suspected pattern of code in the source code or procedures, and identifying the instances of code, the most often called and the most time consuming. We developed a first tool called Adlmap, which is based on static analysis. It detects all DB accesses and flags those that are suspected patterns of code. The second tool we developed, named Pmonitor, is based on hybrid analysis; a combination of static and dynamic analysis. We use it to highlight inefficient code patterns instances
Notre travail consiste en l’analyse et l’optimisation du code source d’applications de type système hérité (ou legacy system). Nous avons particulièrement travaillé sur un logiciel, appelé GP3, qui est développé et maintenu par la société de finances Sungard. Ce logiciel existe depuis plus d’une vingtaine d’années, il est écrit en un langage propriétaire, procédural et de 4ème génération, appelé ADL (ou Application Development Language). Ce logiciel à été initialement développé sous VMS et accédait à des bases de données d’ancienne génération. Pour des raisons commerciales, il fut porté sous UNIX et s’adresse maintenant à des SGBD-R de nouvelles génération ; Oracle et Sybase. Il a également été étendu de manière à offrir une interface web. Ce système hérité doit maintenant faire face à de nouveaux défis, comme la croissance de la taille des bases de données. Durant ces 20 dernières années, nous avons pu observer la fusion de plusieurs entreprises, ce qui implique la fusion de bases de données. Ces dernières peuvent dépasser les 1 Téra de données et plus encore sont à prévoir à l’avenir. Dans ce nouveau contexte, le langage ADL montre des limites à traiter une aussi importante masse de données. Des patterns de code, désignant des structures d’accès en base, sont suspectés d’être responsables de dégradations des performances. Notre travail consiste à détecter toutes les instances de patterns dans le code source, puis d’identifier les instances les plus consommatrices en temps d’exécution et en nombre d’appels. Nous avons développé un premier outil, nommé Adlmap, basé sur l’analyse statique de code, et qui permet de détecter toutes les accès en base dans le code source. Les accès en base identifiés comme patterns de code sont marqués. Le second outil que nous avons développé, nommé Pmonitor, est basé sur une analyse hybride ; combinaison d’analyses statique et dynamique. Cet outil nous permet de mesurer les performances des patterns de code et ainsi, d’identifier les instances les moins performantes

Стилі APA, Harvard, Vancouver, ISO та ін.

18

Millon, Etienne. "Analyse de sécurité de logiciels système par typage statique." Phd thesis, Université Pierre et Marie Curie - Paris VI, 2014. http://tel.archives-ouvertes.fr/tel-01067475.

Повний текст джерела

Анотація:

Les noyaux de systèmes d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilèges d'un attaquant. Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur. La plupart des systèmes d'exploitation sont écrits dans le langage C. On commence par en isoler un sous-langage sûr nommé Safespeak. Sa sémantique opérationnelle et un premier système de types sont décrits, et les propriétés classiques de sûreté du typage sont établies. La manipulation des états mémoire est formalisée sous la forme de lentilles bidirectionnelles, qui permettent d'encoder les mises à jour partielles des états et variables. Un première analyse sur ce langage est décrite, permettant de distinguer les entiers utilisés comme bitmasks, qui sont une source de bugs dans les programmes C.

Стилі APA, Harvard, Vancouver, ISO та ін.

19

Marteau, Hubert. "Une méthode d'analyse de données textuelles pour les sciences sociales basée sur l'évolution des textes." Tours, 2005. http://www.theses.fr/2005TOUR4028.

Повний текст джерела

Анотація:

Le but est d'apporter aux sociologues un outil informatique permettant l'analyse d'entretiens ouverts semi-directifs. Le traitement est en deux étapes : une indexation des entretiens suivi d'une classification. Les méthodes d'indexation habituelles reposent sur une analyse statistiques plus adaptées à des textes de contenu et de structure (textes littéraires, scientifiques,. . . ) marqués qu'à des entretiens limités à l'usage de peu de mots (1000 mots pour des textes de discussion). Partant de l'hypothèse que l'appartenance sociologique induit fortement la forme du discours, nous évaluons la structure et l'évolution des textes en proposant de nouvelles représentations des textes (image, signal) qui conduisent à l'extraction de valeurs indexant le texte, mesures statiques ou liées à l'évolution du texte. La classification choisie est arborée (NJ). Elle repose sur ces caractéristiques par sa faible complexité et son respects des distances, elle fournit une aide à la classification
This PhD Thesis aims at bringing to sociologists a data-processing tool wich allows them to analyse of semi-directing open talks. The proposed tool performs in two steps : an indexation of the talks followed by a classification. Usually, indexing methods rely on a general stastistical analysis. Such methods are suited for texts having contents and structure ( literary texts, scientific texts,. . . ). These texts have more vocabulary and structure than talks (limitation to 1000 words for suche texts). On the basis of the assumption that the sociological membership strongly induces the form of the speech, we propose various methods to evaluate the structure and the evolution of the texts. The methods attempt to find new representations of texts (image, signal) and to extract values from these new representations. Selected classification is a classification by trees (NJ). It has a low complexity and it respects distances, then this method is a good solution to provide a help to classification

Стилі APA, Harvard, Vancouver, ISO та ін.

20

Benayoun, Vincent. "Analyse de dépendances ML pour les évaluateurs de logiciels critiques." Phd thesis, Conservatoire national des arts et metiers - CNAM, 2014. http://tel.archives-ouvertes.fr/tel-01062785.

Повний текст джерела

Анотація:

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.

Стилі APA, Harvard, Vancouver, ISO та ін.

21

Babau, Jean-Philippe. "Etude du comportement temporel des applications temps réel à contraintes strictes basée sur une analyse d'ordonnançabilité." Poitiers, 1996. http://www.theses.fr/1996POIT2305.

Повний текст джерела

Анотація:

Les applications temps reel a contraintes strictes sont des applications multitaches ou les contraintes temporelles (delais d'execution) doivent etre strictement satisfaites. La methodologie developpee permet la validation de ce type d'applications. L'environnement de conception integre la prise en compte des requetes periodiques et aperiodiques et des schemas de programmes exprimant des cooperations fixes ou variables entre les taches. Apres transformation de ce modele comportemental de l'application en un ensemble de taches sous forme normale associees a un graphe de precedence, la validation est basee sur une analyse d'ordonnancabilite. Cette validation est effectuee sur les comportements realistes de l'application et permet d'evaluer les performances temporelles de l'application. Une optimisation des caracteristiques temporelles est alors possible afin d'ameliorer ses performances

Стилі APA, Harvard, Vancouver, ISO та ін.

22

Mordal, Karine. "Analyse et conception d'un modèle de qualité logiciel." Paris 8, 2012. http://www.theses.fr/2012PA084030.

Повний текст джерела

Анотація:

Nous présentons un modèle et un prototype d'analyse et d'évaluation de la qualité de grands logiciels de taille industrielle, le modèle Squash, fondé sur le modèle empirique conçu par les entreprises Qualixo et Air-France KLM. Nous déterminons une méthodologie précise d'évaluation de principes de qualité, tant au niveau technique que fonctionnel. A partir de notre méthodologie nous avons formalisé un modèle de qualité prenant en compte les particularités et exigences du domaine industriel. L'implémentation de ce modèle est en cours de validation chez Générali. A partir de l’étude des domaines du développement informatique et de la validation fonctionnelle, nous avons formalisé un modèle de qualité hiérarchique fondé sur les normes ISO 9126 et SquARE. Ce modèle est composé de deux niveaux : le niveau conceptuel de la qualité qui définit les grands principes de qualité à évaluer et le niveau technique de la qualité qui décrit des règles techniques de base et les mesures associées permettant l'évaluation du niveau supérieur. La principale difficulté dans l’élaboration de ce type de modèle consiste à déterminer comment passer des principes de qualité aux mesures et vice versa, tout en respectant deux principes fondamentaux : ne pas masquer les progrès et mettre en évidence les problèmes. Pour y parvenir nous utilisons d'une part, des formules de combinaison et d’agrégation de métriques et d'autre part, des formules à base de logique floue permettant d'évaluer la qualité à partir de mesures non issues de métriques
We present a model and prototype for analysis and assess quality of large size industrial software, Squash model based on the empirical model developed by Qualixo and Air France-KLM enterprises. We determine an evaluation methodology for both technical and functional quality principles. Then we formalized a quality model taking into account the industrial applications requirements from this methodology. The implementation of this model is being validated by Generali. From the domain of software development and functional validation, we have formalized a model based on hierarchical quality models from standards ISO 9126 and Square. This model is divided into two levels: the conceptual quality level that defines the main quality principles and the technical quality that defines basic technical rules and measures used to assess the top level. The main issue of quality model conception is how to bring the gap between metrics and quality principles : the metrics meannig often defined for individual components cannot be easily transposed to higher abstraction levels. Furthermore, we need to highlight problems and do not hide progress. To achieve this, we use combinaison and aggregation formulas to asses quality principles from metrics and fuzzy logic to assess quality principles from non-metric measurements

Стилі APA, Harvard, Vancouver, ISO та ін.

23

BARROS, SERGE. "Analyse a priori des consequences de la modification de systemes logiciels : de la theorie a la pratique." Toulouse 3, 1997. http://www.theses.fr/1997TOU30267.

Повний текст джерела

Анотація:

Longtemps consideree comme une besogne de second ordre dans l'ombre d'activites bien plus nobles, la maintenance du logiciel, au dela de la simple correction d'erreurs, revele aujourd'hui d'autres facettes, comme la reutilisation de composants ou l'adaptation des systemes a des evolutions de besoins ou d'environnement, qui contribuent a en faire un des points cles de l'amelioration de la competitivite de l'industrie du logiciel. Toutefois, les couts de la maintenance etant generalement sous estimes, la maintenance ne se fait pas dans de bonnes conditions et les logiciels vieillissent mal, devenant des edifices instables, la moindre modification pouvant en compromettre l'equilibre. Il est donc primordial de pouvoir prevoir les consequences d'une modification avant meme de la realiser, ce qui est l'objectif de l'analyse d'impact. Nous presentons dans ce memoire une nouvelle approche generique de l'analyse d'impact, basee sur une propagation automatique, controlee par des regles, d'evenements sur un graphe des dependances modelisant le systeme. Elle permet de concilier la simplicite et la puissance des analyses automatiques a la precision des analyses manuelles. De plus, au travers de la realisation d'un outil implementant cette technique, puis de sa mise en oeuvre sur divers systemes representatifs, nous montrons que cette approche est particulierement adaptee a des systemes logiciels volumineux, necessitant un haut niveau de qualite, tels que ceux que l'on rencontre dans l'industrie spatiale. Mots cles : maintenance de logiciels, maitrise des evolutions, analyse d'impact.

Стилі APA, Harvard, Vancouver, ISO та ін.

24

Garoche, Pierre-Loïc Sallé Patrick. "Analyse statistique d'un calcul d'acteurs par interprétation abstraite Statistic analysis of an actor-based process calculus by abstract interpretation /." Toulouse : INP Toulouse, 2008. http://ethesis.inp-toulouse.fr/archive/00000629.

Повний текст джерела

Стилі APA, Harvard, Vancouver, ISO та ін.

25

Irfan, Muhammad Naeem. "Analyse et optimisation d'algorithmes pour l'inférence de modèles de composants logiciels." Phd thesis, Université de Grenoble, 2012. http://tel.archives-ouvertes.fr/tel-00767894.

Повний текст джерела

Анотація:

Les Components-Off-The-Shelf (COTS) sont utilisés pour le développement rapide et efficace de logiciels tout en limitant le coût. Il est important de tester le fonctionnement des composants dans le nouvel environnement. Pour les logiciels tiers,le code source des composants, les spécifications et les modèles complets ne sont pas disponibles. Dans la littérature de tels systèmes sont appelés composants "boîte noire". Nous pouvons vérifier leur fonctionnement avec des tests en boîte noire tels que le test de non-régression, le test aléatoire ou le test à partir de modèles. Pour ce dernier, un modèle qui représente le comportement attendu du système sous test(SUT) est nécessaire. Ce modèle contient un ensemble d'entrées, le comportement du SUT après stimulation par ces entrées et l'état dans lequel le système se trouve.Pour les systèmes en boîte noire, les modèles peuvent être extraits à partir des traces d'exécutions, des caractéristiques disponibles ou encore des connaissances des experts. Ces modèles permettent ensuite d'orienter le test de ces systèmes.Les techniques d'inférence de modèles permettent d'extraire une information structurelle et comportementale d'une application et de la présenter sous forme d'un modèle formel. Le modèle abstrait appris est donc cohérent avec le comportement du logiciel. Cependant, les modèles appris sont rarement complets et il est difficile de calculer le nombre de tests nécessaires pour apprendre de façon complète et précise un modèle.Cette thèse propose une analyse et des améliorations de la version Mealy de l'algorithme d'inférence L* [Angluin 87]. Elle vise à réduire le nombre de tests nécessaires pour apprendre des modèles. La version Mealy de L* nécessite d'utiliser deux types de test. Le premier type consiste à construire les modèles à partir des sorties du système, tandis que le second est utilisé pour tester l'exactitude des modèles obtenus. L'algorithme utilise ce que l'on appelle une table d'observation pour enregistrer les réponses du système.Le traitement d'un contre-exemple peut exiger d'envoyer un nombre conséquent de requêtes au système. Cette thèse aborde ce problème et propose une technique qui traite les contre-exemples de façon efficace. Nous observons aussi que l'apprentissage d'un modèle ne nécessite pas de devoir remplir complètement ces tables. Nous proposons donc un algorithme d'apprentissage qui évite de demander ces requêtes superflues.Dans certains cas, pour apprendre un modèle, la recherche de contre-exemples peut coûter cher. Nous proposons une méthode qui apprend des modèles sans demander et traiter des contre-exemples. Cela peut ajouter de nombreuses colonnes à la table d'observation mais au final, nous n'avons pas besoin d'envoyer toutes les requêtes. Cette technique ne demande que les requêtes nécessaires.Ces contributions réduisent le nombre de tests nécessaires pour apprendre des modèles de logiciels, améliorant ainsi la complexité dans le pire cas. Nous présentons les extensions que nous avons apportées à l'outil RALT pour mettre en oeuvre ces algorithmes. Elles sont ensuite validées avec des exemples tels que les tampons, les distributeurs automatiques, les protocoles d'exclusion mutuelle et les planificateurs.

Стилі APA, Harvard, Vancouver, ISO та ін.

26

Nassar, Mahmoud Coulette Bernard. "Analyse/conception par points de vue le profil VUML /." Toulouse : INP Toulouse, 2005. http://ethesis.inp-toulouse.fr/archive/00000179.

Повний текст джерела

Стилі APA, Harvard, Vancouver, ISO та ін.

27

Boudjema, El Habib. "Défense contre les attaques de logiciels." Thesis, Paris Est, 2018. http://www.theses.fr/2018PESC1015/document.

Повний текст джерела

Анотація:

Dans ce début du troisième millénium, nous sommes témoins d'un nouvel âge. Ce nouvel âge est caractérisé par la transition d'une économie industrielle vers une économie basée sur la technologie de l'information. C'est l’âge de l'information. Aujourd’hui le logiciel est présent dans pratiquement tous les aspects de notre vie. Une seule vulnérabilité logicielle peut conduire à des conséquences dévastatrices. La détection de ces vulnérabilités est une tâche qui devient de plus en plus dure surtout avec les logiciels devenant plus grands et plus complexes. Dans cette thèse, nous nous sommes intéressés aux vulnérabilités de sécurité impactant les applications développées en langage C et particulièrement les vulnérabilités provenant de l'usage des fonctions de ce langage. Nous avons proposé une liste de vérifications pour la détection des portions de code causant des vulnérabilités de sécurité. Ces vérifications sont sous la forme de conditions rendant l'appel d'une fonction vulnérable. Des implémentations dans l'outil Carto-C et des expérimentations sur la base de test Juliet et les sources d'applications réelles ont été réalisées. Nous nous sommes également intéressés à la détection de vulnérabilités exploitables au niveau du code binaire. Nous avons défini en quoi consiste le motif comportemental d'une vulnérabilité. Nous avons proposé une méthode permettant de rechercher ces motifs dans les traces d'exécutions d'une application. Le calcul de ces traces d'exécution est effectué en utilisant l'exécution concolique. Cette méthode est basée sur l'annotation de zones mémoires sensibles et la détection d'accès dangereux à ces zones. L'implémentation de cette méthode a été réalisée dans l'outil Vyper et des expérimentations sur la base de test Juliet et les codes binaires d'applications réelles ont été menées avec succès
In the beginning of the third millennium we are witnessing a new age. This new age is characterized by the shift from an industrial economy to an economy based on information technology. It is the Information Age. Today, we rely on software in practically every aspect of our life. Information technology is used by all economic actors: manufactures, governments, banks, universities, hospitals, retail stores, etc. A single software vulnerability can lead to devastating consequences and irreparable damage. The situation is worsened by the software becoming larger and more complex making the task of avoiding software flaws more and more difficult task. Automated tools finding those vulnerabilities rapidly before it is late, are becoming a basic need for software industry community. This thesis is investigating security vulnerabilities occurring in C language applications. We searched the sources of these vulnerabilities with a focus on C library functions calling. We dressed a list of property checks to detect code portions leading to security vulnerabilities. Those properties give for a library function call the conditions making this call a source of a security vulnerability. When these conditions are met the corresponding call must be reported as vulnerable. These checks were implemented in Carto-C tool and experimented on the Juliet test base and on real life application sources. We also investigated the detection of exploitable vulnerability at binary code level. We started by defining what an exploitable vulnerability behavioral patterns are. The focus was on the most exploited vulnerability classes such as stack buffer overflow, heap buffer overflow and use-after-free. After, a new method on how to search for this patterns by exploring application execution paths is proposed. During the exploration, necessary information is extracted and used to find the patterns of the searched vulnerabilities. This method was implemented in our tool Vyper and experimented successfully on Juliet test base and real life application binaries.level. We started by defining what an exploitable vulnerability behavioral patterns are. The focus was on the most exploited vulnerability classes such as stack buffer overflow, heap buffer overflow and use-after-free. After, a new method on how to search for this patterns exploring application execution paths is proposed. During the exploration, necessary information is extracted and used to find the patterns of the searched vulnerabilities. This method was implemented in our Vyper tool and experimented successfully on Juliet test base and real life application binaries

Стилі APA, Harvard, Vancouver, ISO та ін.

28

Fontalbe, Patrick. "Evaluation partielle symbolique : une analyse semantique des programmes c en vue de leur verification." Paris 6, 1996. http://www.theses.fr/1996PA066147.

Повний текст джерела

Анотація:

Nous proposons dans cette these une technique d'analyse semantique statique des programmes c elaboree a partir de l'evaluation partielle et de l'evaluation symbolique. La premiere methode consiste a reduire un programme en fixant la valeur d'un sous-ensemble de ses parametres pour obtenir un programme residuel ayant la meme semantique que l'original pour ces valeurs ; la seconde consiste a evaluer le programme en propageant dans son code des symboles de valeurs donnes arbitrairement a ses variables d'entree. L'evaluation partielle symbolique (eps) que nous proposons est une synthese de ces deux methodes. Son but est non seulement de verifier statiquement la semantique d'un programme c donne, en detectant statiquement des erreurs run-time comme dans l'evaluation symbolique, mais egalement de calculer un programme residuel dont la semantique est une abstraction de celle du programme original (et non pas une semantique equivalente comme dans le cas de l'evaluation partielle). Cette methode presente le caractere statique (off-line) de l'evaluation partielle et le caractere flow sensitive de l'evaluation symbolique. Ainsi l'interet du programme residuel est double: d'une part sa representation est debarrassee de tout ce qui ne contribue pas directement a sa semantique, d'autre part chacun de ses chemins d'executions possibles est distingue des autres ; ainsi il se prete a diverses utilisations ulterieures, par exemple d'autres analyses ou des series de tests, une bonne partie du travail etant alors deja effectuee

Стилі APA, Harvard, Vancouver, ISO та ін.

29

Aguila, Orieta Del. "Analyse et structuration des données dans les logiciels de CAO en électromagnétisme." Grenoble INPG, 1988. http://www.theses.fr/1988INPG0077.

Повний текст джерела

Анотація:

Cette étude s'inscrit dans le cadre de l'application de la méthode des éléments finis au calcul des champs électromagnétiques. La complexité des logiciels réalisés nous a conduit à clarifier les concepts de structures des données ainsi que les moyens informatiques qui permettent la mise en oeuvre de ces structures. Après avoir effectué une étude bibliographique exhaustive concernant les bases de données nous présentons les caractéristiques essentielles des données rencontrées en CAO afin de déterminer les modèles de données qui s'adaptent le mieux à notre problème. Bien qu'il n'y ait pas un modèle unique pour la CAO, nous fournirons les éléments permettant d'appréhender la solution la mieux adaptée à chacun des programmes rencontrés. Nous présentons ensuite deux logiciels de CAO qui utilisent la méthode des éléments finis FLUX 3D pour l'électromagnétisme, I-DEAS Supertab pour la mécanique et nous analysons leurs structures de données. Nous présentons enfin quelques algorithmes de maillage de surfaces en 3D ainsi que des algorithmes de visualisation d'objets avec élimination des parties cachets

Стилі APA, Harvard, Vancouver, ISO та ін.

30

Santana, Orieta. "Analyse et structuration des données dans les logiciels de CAO en électromagnétisme." Grenoble 2 : ANRT, 1988. http://catalogue.bnf.fr/ark:/12148/cb37613089w.

Повний текст джерела

Стилі APA, Harvard, Vancouver, ISO та ін.

31

Ferlin, Antoine. "Vérification de propriétés temporelles sur des logiciels avioniques par analyse dynamique formelle." Thesis, Toulouse, ISAE, 2013. http://www.theses.fr/2013ESAE0024/document.

Повний текст джерела

Анотація:

La vérification de logiciels est une activité dont l'importance est cruciale pour les logiciels embarqués critiques. Les différentes approches envisageables peuvent être classées en quatre catégories : les méthodes d'analyse statique non formelles, les méthodes d'analyse statique formelles, les méthodes d'analyse dynamique non formelles et les méthodes d'analyse dynamique formelles. L'objectif de cette thèse est de vérifier des propriétés temporelles dans un cadre industriel, par analyse dynamique formelle.La contribution comporte trois parties. Un langage adapté à l'expression des propriétés à vérifier, tirées du contexte industriel d'Airbus, a été dé ni. Il repose notamment sur la logique temporelle linéaire mais également sur un langage d'expressions régulières.La vérification d'une propriété temporelle s'effectue sur une trace d'exécution d'un logiciel, générée à partir d'un cas de test pré-existant. L'analyse statique est utilisée pour générer la trace en fonction des informations nécessaires à la vérification de la propriété temporelle formalisée.Cette approche de vérification propose une solution pragmatique au problème posé par le caractère ni des traces considérées. Des adaptations et des optimisations ont également été mises en œuvre pour améliorer l'efficacité de l'approche et faciliter son utilisation dans un contexte industriel. Deux prototypes ont été implémentés,des expérimentations ont été menées sur différents logiciels d'Airbus
Software Verification is decisive for embedded software. The different verification approaches can be classified in four categories : non formal static analysis,formal static analysis, non formal dynamic analysis and formal dynamic analysis.The main goal of this thesis is to verify temporal properties on real industrial applications,with the help of formal dynamic analysis.There are three parts for this contribution. A language, which is well adapted to the properties we want to verify in the Airbus context was defined. This language is grounded on linear temporal logic and also on a regular expression language.Verification of a temporal property is done on an execution trace, generated from an existing test case. Generation also depends on required information to verify the formalized property. Static analysis is used to generate the trace depending on the formalized property.The thesis also proposes a pragmatic solution to the end of trace problem. In addition,specific adaptations and optimisations were defined to improve efficiency and user-friendliness and thus allow an industrial use of this approach. Two applications were implemented. Some experiments were led on different Airbus software

Стилі APA, Harvard, Vancouver, ISO та ін.

32

Hourtolle, Catherine. "Conception de logiciels sûrs de fonctionnement : analyse de la sécurité des logiciels : mécanismes de décision pour la programmation en n-versions." Toulouse, INPT, 1987. http://www.theses.fr/1987INPT059H.

Повний текст джерела

Анотація:

Une etude d'analyse de securite permettant la recherche des fonctions et des modes de defaillance critiques du logiciel est presentee. Elle repose sur l'utilisation conjointe de trois techniques d'analyses: l'analyse des modes de defaillance et de leurs effets (amde), l'analyse par arbres des fautes et l'analyse par reseaux de petri. En ce qui concerne la tolerance aux fautes logicielles, la programmation en n-versions parait etre une approche prometteuse pour les logiciels temps reel. La mise en oeuvre du controleur d'un lociciel en n-versions, c'est a dire les mecanismes de recouvrement, de vote et de synchronisation

Стилі APA, Harvard, Vancouver, ISO та ін.

33

Hourtolle, Catherine. "Conception de logiciels sûrs de fonctionnement analyse de la sécurité des logiciels, mécanismes de décision pour la programmation en N-versions /." Grenoble 2 : ANRT, 1987. http://catalogue.bnf.fr/ark:/12148/cb37605979b.

Повний текст джерела

Стилі APA, Harvard, Vancouver, ISO та ін.

34

Bourmaud, Gaëtan Rabardel Pierre. "Les systèmes d' instruments méthodes d' analyse et perspectives de conception /." Saint-Denis : Université de Paris VIII, 2006. http://www.bu.univ-paris8.fr/web/collections/theses/bourmaud_gaetan.pdf.

Повний текст джерела

Стилі APA, Harvard, Vancouver, ISO та ін.

35

Brejon, Paul. "Les logiciels d'energetique des batiments : developpement, evaluation technique, illustrations." Paris, ENMP, 1988. http://www.theses.fr/1988ENMP0110.

Повний текст джерела

Стилі APA, Harvard, Vancouver, ISO та ін.

36

Errami, Mounir. "Analyse statistique des structures tridimensionnelles de protéines et validation de familles structurales à bas taux d'identité." Lyon 1, 2002. http://www.theses.fr/2002LYO10178.

Повний текст джерела

Анотація:

Le travail présenté comporte deux parties. Dans la première partie, nous présentons une stratégie originale pour l'étude statistique exhaustive et objective des structures tridimensionnelles de protéines. Cette stratégie est basée sur une architecture logicielle bioinformatique complexe grâce à laquelle nous établissons les relations entre les alignements multiples de séquences et la conservation de caractéristiques structurales particulières au sein de protéines. Nous montrons que les acides aminés des ponts disulfures, des interactions hydrophobes ou électrostatiques sont particulièrement conservés dans les alignements multiples, suggérant l'apport potentiel des alignements multiples pour la prédiction des structures tridimensionnelles. Par ailleurs, nous montrons que les alignements les plus informatifs sont constitués de séquences apparentées faiblement similaires. Cependant, il est difficile de valider les familles structurales à faible similarité. Dans la seconde partie du travail, nous présentons une méthode qui permet à partir d'un alignement multiple de séquences, de détecter les séquences " intruses " n'ayant pas de parenté avec les autres séquences de l'alignement. Cette méthode s'appuie sur la prédiction des structures secondaires et l'analyse de leur compatibilité dans les alignements multiples. Cette méthode automatique fournit un moyen efficace de s'assurer de la cohérence des alignements multiples et peut être utilisée pour réaliser de manière itérative, les alignement les plus divergents possibles et donc les plus informatifs. Par ailleurs, cette méthode peut être utile dans d'autres domaines : la caractérisation et la classification des protéines, l'amélioration des alignements multiples de séquences et des outils d'alignements et la modélisation des structures de protéines. Ces champs d'étude offrent des perspectives intéressantes pour les outils développés et les travaux réalisés durant cette thèse.

Стилі APA, Harvard, Vancouver, ISO та ін.

37

El, Hatib Souad. "Une approche sémantique de détection de maliciel Android basée sur la vérification de modèles et l'apprentissage automatique." Master's thesis, Université Laval, 2020. http://hdl.handle.net/20.500.11794/66322.

Повний текст джерела

Анотація:

Le nombre croissant de logiciels malveillants Android s’accompagne d’une préoccupation profonde liée aux problèmes de la sécurité des terminaux mobiles. Les enjeux deviennent sans conteste de plus en plus importants, suscitant ainsi beaucoup d’attention de la part de la communauté des chercheurs. En outre, la prolifération des logiciels malveillants va de pair avec la sophistication et la complexité de ces derniers. En effet, les logiciels malveillants plus élaborés, tels que les maliciels polymorphes et métamorphiques, utilisent des techniques d’obscurcissement du code pour créer de nouvelles variantes qui préservent la sémantique du code original tout en modifiant sa syntaxe, échappant ainsi aux méthodes de détection usuelles. L’ambition de notre recherche est la proposition d’une approche utilisant les méthodes formelles et l’apprentissage automatique pour la détection des maliciels sur la plateforme Android. L’approche adoptée combine l’analyse statique et l’apprentissage automatique. En effet, à partir des applications Android en format APK, nous visons l’extraction d’un modèle décrivant de manière non ambiguë le comportement de ces dernières. Le langage de spécification formelle choisi est LNT. En se basant sur le modèle généré, les comportements malicieux exprimés en logique temporelle sont vérifiés à l’aide d’un vérificateur de modèle. Ces propriétés temporelles sont utilisées comme caractéristiques par un algorithme d’apprentissage automatique pour classifier les applications Android.
The ever-increasing number of Android malware is accompanied by a deep concern about security issues in the mobile ecosystem. Unquestionably, Android malware detection has received much attention in the research community and therefore it becomes a crucial aspect of software security. Actually, malware proliferation goes hand in hand with the sophistication and complexity of malware. To illustrate, more elaborated malware like polymorphic and metamorphic malware, make use of code obfuscation techniques to build new variants that preserve the semantics of the original code but modify it’s syntax and thus escape the usual detection methods. In the present work, we propose a model-checking based approach that combines static analysis and machine learning. Mainly, from a given Android application we extract an abstract model expressed in terms of LNT, a process algebra language. Afterwards, security related Android behaviours specified by temporal logic formulas are checked against this model, the satisfaction of a specific formula is considered as a feature, finally machine learning algorithms are used to classify the application as malicious or not.

Стилі APA, Harvard, Vancouver, ISO та ін.

38

Josse, Sébastien. "Analyse et détection dynamique de code viraux dans un contexte cryptographique (et application à l'évaluation de logiciel antivirus)." Palaiseau, Ecole polytechnique, 2009. http://www.theses.fr/2009EPXX0019.

Повний текст джерела

Анотація:

Cette thèse est consacrée à la problématique de l’évaluation des produits antivirus. L’utilisateur final d’un produit antivirus ne sait pas toujours quelle confiance il peut placer dans son produit antivirus pour parer convenablement la menace virale. Pour répondre à cette question, il est nécessaire de formuler la problématique de sécurité à laquelle doit répondre un tel produit et de disposer d’outils et de critères méthodologiques, techniques et théoriques permettant d’évaluer la robustesse des fonctions de sécurité et la pertinence des choix de conception au regard d’une menace virale identifiée. Je concentre mon analyse de la menace virale sur quelques mécanismes (mécanismes cryptographiques, transformations de programme) adaptés au contexte boîte blanche, i. E. Permettant à un virus de protéger ses données critiques en confidentialité et de masquer son fonctionnement dans un environnement complètement maîtrisé par l’attaquant. Une première étape incontournable avant toute organisation d’une ligne de défense consiste à analyser les virus, afin d’en comprendre le fonctionnement et les effets sur le système. Les méthodes et techniques de la rétro-ingénierie logicielle occupent ici - au côté des techniques de cryptanalyse - une place centrale. J’ai pris le parti de focaliser sur les méthodes dynamiques d’extraction d’information fondées sur une émulation du matériel supportant le système d’exploitation. L’évaluation d’un moteur de détection selon des critères objectifs requiert un effort de modélisation. J’étudie quelques modèles utilisés actuellement (grammaires formelles, interprétation abstraite, statistique). Chacun de ces modèles permet de formaliser certains aspects du problème de la détection virale. Je m’attache à l’étude des critères qu’il est possible de définir dans chacun de ces cadres formels et à leur utilisation pour partie des travaux d’évaluation d’un moteur de détection. Mes travaux m’ont conduit à la mise en oeuvre d’une approche méthodologique et d’une plate-forme de tests pour l’analyse de robustesse des fonctions et mécanismes d’un produit anti-virus. J’ai développé un outil d’analyse de code viral, appelé VxStripper, dont les fonctionnalités sont utiles à la réalisation de plusieurs des tests. Les outils formels sont utilisés pour qualifier en boîte blanche - ou sur la base des documents de conception détaillée - la conformité et l’efficacité d’un moteur de détection
This thesis is devoted to the problem of anti-virus software evaluation. The end user of an anti-virus software package does not always know what confidence he can place in his product to counter effectively the viral threat. In order to answer this question, it is necessary to formulate the security issue which such a product must respond to and to have tools and methodological, technical and theoretical criteria for assessing the robustness of security functions and the relevance of design choices against an identified viral threat. I concentrate my analysis of the viral threat on a few mechanisms suited to the white box context, i. E. Allowing a virus to protect the confidentiality of its critical data and to mask its operations in an environment completely controlled by the attacker. A first mandatory step before any organization of a line of defense is to analyze viruses, in order to understand their operation and impact on the system. Software reverse-engineering methods and techniques occupy a central place here (alongside cryptanalysis methods). I basically focus on the dynamic methods of information extraction based on an emulation of the hardware supporting the operating system. The evaluation of a detection engine based on objective criteria requires an effort of modeling. I study a few models (formal grammars, abstract interpretation, statistics). Each of these models makes it possible to formalize some aspects of the viral detection problem. I make every effort to study the criteria it is possible to define in each of these formal frameworks and their use for part of the evaluation tasks of a detection engine. My work led me to implement a methodological approach and a testing platform for the robustness analysis of the functions and mechanisms of an anti-virus. I developed a tool to analyze viral code, called VxStripper, whose features are useful to several tests. The formal tools are used to qualify (on the basis of the detailed design information) compliance and effectiveness of a detection engine

Стилі APA, Harvard, Vancouver, ISO та ін.

39

Zhioua, Abir. "Analyse de diverses distances en vérification formelle probabiliste." Thesis, Université Laval, 2012. http://www.theses.ulaval.ca/2012/28874/28874.pdf.

Повний текст джерела

Анотація:

Dans ce mémoire nous nous intéressons à une branche de la vérification qui consiste à comparer une spécification (fonctionnement idéal) à son implémentation (système réel). Tous les deux sont sous forme de systèmes probabilistes, c’est-à-dire des systèmes dont le comportement est incertain mais quantifié par des distributions de probabilité. Il y a plusieurs méthodes disponibles pour comparer les systèmes : la bisimulation, la simulation, l’équivalence de traces, ou bien les distances qui s’adaptent au comportement probabiliste auquel nous nous intéressons. En effet, plutôt que de dire si oui ou non les deux systèmes à comparer sont « équivalents » une distance nous donne une valeur qui quantifie leur différence. Si la distance est 0 les deux systèmes sont équivalents. Il y a plusieurs notions de distances pour les systèmes probabilistes, le but de ce mémoire est de comparer trois d’entre elles : -distance, K-moment et Desharnais et al. Le principal résultat de cette comparaison est que les trois méthodes ont des résultats qui ne sont pas fondamentalement différents, bien qu’elles soient conçues de façon difficilement comparable. Il arrive souvent que les distances se suivent. Les principales différences se manifestent dans le temps de calcul, la capacité de traitement et l’atténuation du futur. Nous démontrons que les performances de chaque distance varient selon le type de système traité. Cela signifie que pour choisir la meilleure méthode, il faut déterminer le type de système que nous avons. En prenant par exemple un système dont nous n’avons pas le modèle, c’est la famille K-moment qui sera la seule capable de calculer une distance. Par ailleurs, nous avons pu intégrer dans la -distance un facteur qui atténue les différences les plus lointaines par rapport à celles plus proches. Cela nous a amené à définir une nouvelle distance : -distance atténuée.

Стилі APA, Harvard, Vancouver, ISO та ін.

40

Sims, Elodie-Jane. "Analyse statique de pointeurs et logique de séparation." Palaiseau, Ecole polytechnique, 2007. http://www.theses.fr/2007EPXX0038.

Повний текст джерела

Анотація:

Le cadre de cette thèse est l'analyse statique modulaire par interprétation abstraite de logiciels en vue de leur vérification automatique. Nous nous intéressons en particulier aux programmes comportant des objets alloués dynamiquement sur un tas et repérés par des pointeurs. Le but final étant de trouver des erreurs dans un programme (problèmes de déréférencements et d'alias) ou de prouver qu'un programme est correct (relativement à ces problèmes) de façon automatique. Isthiaq, Pym, O'Hearn et Reynolds ont développé récemment des logiques de fragmentation (separation logics) qui sont des logiques de Hoare avec un langage d'assertions/de prédicats permettant de démontrer qu'un programme manipulant des pointeurs sur un tas est correct. La sémantique des triplets de la logique ({P}C{P′}) est définie par des transformateurs de prédicats de style plus faible pré-condition. Nous avons exprimé et prouvé la correction de ces plus faibles pré-conditions (wlp) et plus fortes post-conditions (sp), en particulier dans le cas de la commande while. L'avantage par rapport à ce qui est fait dans la communauté est que les wlp et sp sont définis pour toute formule alors que certaines des règles existantes avaient des restrictions syntaxiques. Nous avons rajouté des points fixes à la logique ainsi qu'une substitution retardée permettant d'exprimer des formules récursives. Nous avons exprimé les wlp et sp dans cette logique avec points fixes et prouvé leur correction. La substitution retardée a une utilité directe pour l'expression de formules récursives. Par exemple, nclist(x) = μXv. (x = nil) ∨ ∃x1, x2. (isval(x1) ∧ (x 7→ x1, x2 ∗ Xv[x2/x])) décrit l'ensemble des mémoires où x pointe vers une liste d'entiers. Le but ensuite était d'utiliser cette logique de fragmentation avec points fixes comme langage d'interface pour des analyses de pointeurs. Il s'agit de formuler une traduction des domaines de ces analyses en formules de la logique (et inversement) et d'en prouver la correction. On peut également parfois utiliser ces traductions pour prouver la correction de ces analyses. Nous avions déjà illustré cette approche pour une analyse très simple de partitionnement des pointeurs. Nous avons traduit les formules de la logique dans un nouveau langage abstrait permettant de décrire le type des valeurs associées aux variables dans la mémoire (nil, entier, bool, pointeur vers une paire de tel type, etc. ) ainsi que les relations d'aliasing et non-aliasing entre variables et entre points de la mémoire. Le principal apport est la définition de ce langage et de sa sa sémantique dans le domaine concret qui est celui utilisé pour la sémantique des formules. En particulier, les variables auxiliaires dont la sémantique est habituellement une question d'implémentation font ici explicitement part du langage et de sa sémantique. Ce langage est un produit cartésien de plusieurs sous domaines et peut être paramétré par les domaines numériques existants. Nous avons créé un sous-domaine qui est un tableau permettant de compenser le manque de précision dû à l'utilisation de graphes d'ensembles au lieu d'ensembles de graphes. Nous avons exprimé et prouvé les traductions des formules dans ce langage abstrait.

Стилі APA, Harvard, Vancouver, ISO та ін.

41

Blanchet, Christophe. "Logiciel MPSA et ressources bioinformatiques client-serveur web dédiés à l'analyse de séquences de protéine." Lyon 1, 1999. http://www.theses.fr/1999LYO10139.

Повний текст джерела

Анотація:

Depuis quelques annees les projets genomes se multiplient et leur duree de realisation diminue. Les genomes connus s'accumulent et permettent deja de mettre en evidence des genes homologues de differentes especes. Il est alors possible de supposer la fonction d'un gene par homologie avec ceux d'autres especes. Car c'est la qu'est le veritable enjeu de tous ces programmes de grand sequencage : identifier les fonctions des proteines codees par ces genes et leurs implications dans les chemins metaboliques. L'analyse de sequence de proteine prend alors tout son sens. En effet, elle essaye d'attribuer aux proteines codees par ces genes une fonction et des caracteristiques a partir des donnees deja connues. Les banques mondiales contenant ces donnees sont de plus en plus grandes et complexes. Les biologistes ont besoin d'outils efficaces pour travailler sur de tres grandes familles de proteines et pour integrer des donnees complexes et correlees. Dans ce contexte, nous avons developpe mpsa (multiple protein sequence analysis) et nps@ (network protein sequence analysis) : un ensemble d'outils et de ressources bio-informatiques dediees a l'analyse de sequences de proteine. Ces logiciels integrent plusieurs methodes necessaires a l'analyse de sequences de proteine comme la recherche de similarites dans les banques, les alignements multiples, les predictions de structures secondaires, les predictions de caracteristiques physico-chimiques. Mpsa integre notamment une methode de recherches de motifs proteiques dans les banques que nous avons mise au point. Cette methode ameliore le rapport signal/bruit lors d'une recherche en privilegiant l'information biologique des motifs. Les resultats de ces diverses methodes sont presentes graphiquement et relies les uns aux autres afin d'accelerer et d'ameliorer les processus d'analyse. Un accent particulier a ete mis sur la convivialite, la simplification et l'automatisation des taches fastidieuses pour l'utilisateur. La conception de mpsa en langage c et l'utilisation de bibliotheques d'une portabilite elevee l'affranchissent des contraintes liees aux architectures materielles (distribue pour unix, mac et pc). Dans un souci de reutilisabilite du code, les differentes methodes ont ete rassemblees dans une bibliotheque c nommee biolcp. Cette librairie portable est disponible pour de nouvelles utilisations par d'autres bio-informaticiens. Elle peut etre obtenue, tout comme mpsa, sur le site web de mpsa (http : //www. Ibcp. Fr/mpsa), qui propose egalement une aide en ligne et les informations sur le developpement de mpsa. L'adjonction d'un module client-serveur http (web) offre a mpsa les potentialites que sont a meme de proposer les grands serveurs biologiques : gestion centralisee des donnees et de leur mise a jour ; grande puissance de calcul. La partie serveur-mpsa, implementee en perl 5, est disponible sur le site web de mpsa et peut alors etre rapatriee et installee sur un serveur local ou un intranet.

Стилі APA, Harvard, Vancouver, ISO та ін.

42

Kriaa, Hassen. "Analyse et conception révisable par interaction entre agents : Une approche hybride." Pau, 2000. http://www.theses.fr/2000PAUU3011.

Повний текст джерела

Анотація:

Ce travail de these est centre sur la mise en place ou l'ebauche d'une methode d'analyse et de conception oriente agent et la conception et la construction d'un systeme d'information distribue interactif. Son domaine d'application est celui des systemes d'information cooperatifs et intelligents lies a la sante et en particulier au processus de suivi des patients a la chaine des urgences. La methode propose quelques idees essentielles : la combinaison de l'analyse ascendante et concourante fondee sur les points de vues multiples, l'analyse du dialogue entre acteurs en amont de l'analyse et de la conception, la representation des dialogues aux travers des scenarii dynamiquement construit. L'inclusion de la concourance et de la revision pour resoudre les conflits et assurer la continuite du developpement. Le prototype a ete concu en parfaite collaboration avec deux medecins urgentistes. C'est un veritable simulateur qui permet de tester, de verifier, de mettre a jour et de completer les connaissances lors du processus de la prise en charge des patients dans la chaine des urgences. Les agents prevus dans le systeme assurent differents aspects d'apprentissage, de tracabilite, de cooperation, d'aide et de controle de l'accreditation. Le travail peut etre poursuivi dans deux directions complementaires. Selon un axe genie logiciel, il reste a construire un atelier de genie logiciel informatise d'aide a la conception supportant la methode proposee. Selon un axe theorique, il reste a approfondir la contribution d'autres travaux de recherches pour l'analyse des taches, pour la gestion de la communication et pour l'implementation des agents afin d'ameliorer cette approche

Стилі APA, Harvard, Vancouver, ISO та ін.

43

Han, Woo-Suck. "Analyse linéaire et non-linéaire de plaques et coques par éléments finis en statique et dynamique sur micro-ordinateur." Vandoeuvre-les-Nancy, INPL, 1989. http://www.theses.fr/1989NAN10177.

Повний текст джерела

Анотація:

L'objectif de cette étude est la présentation d'un élément isoparamétrique tridimensionnel dégénéré à nombre de nœuds variables pour l'analyse linéaire, non linéaire géométrique et matériel (élasto-plasticité) des structures plaques et coques de forme générale, en tenant compte de l'effet de cisaillement sous les hypothèses de Mindlin, sur micro-ordinateur. Par les variations de divers exemples de plaques et coques, nous constatons, dans le premier chapitre, les performances des éléments quadratiques et cubiques de Serendip et de Lagrange, en comparant l'intégration numérique exacte avec l'intégration réduite. Dans le deuxième chapitre, les solutions en dynamique vibratoire sont obtenues en utilisant la méthode d'itération sur sous-espace, la méthode de superposition modale et la méthode d'intégration directe pas-à-pas. Dans les troisième et quatrième chapitres, nous avons étendu l'étude aux problèmes non linéaires géométriques et matériels (élasto-plasticité) en grands déplacements et grandes rotations, en utilisant la méthode incrémentale avec la formulation lagrangienne actualisée. Les équations d'équilibre non linéaires sont résolues par la méthode de Newton-Raphson modifiée. Dans la résolution en élasto-plasticité, on admet l'hypothèse des petites déformations. Un code de calcul par éléments finis a été spécialement développé sur micro-ordinateur pour traiter ces quatre cas

Стилі APA, Harvard, Vancouver, ISO та ін.

44

Garcia, Arnaud. "Analyse statistique et morphologique des images multivaluées : développements logiciels pour les applications cliniques." Phd thesis, École normale supérieure de Cachan - ENS Cachan, 2008. http://tel.archives-ouvertes.fr/tel-00422589.

Повний текст джерела

Анотація:

La détection et la segmentation de formes dans les images à partir d'un échantillon nécessitent de combiner une analyse statistique des données à une analyse morphologique de l'image. L'analyse statique a pour objectif un calcul local de la similarité de l'image au modèle ; l'analyse morphologique vient compléter ce dispositif en permettant la prise en compte de l'information géométrique pour finaliser les étapes de détection et de segmentation. Les images étudiées sont des images multivaluées : images couleur, images multimodalité ou pile d'images émergeant d'une analyse multiéchelle d'une image scalaire... Le passage de l'image scalaire à l'image multivaluée pose des difficultés fondamentales, notamment pour l'analyse morphologique qui requiert de disposer d'un ordre total sur les valeurs manipulées. Contrairement aux scalaires, deux vecteurs ne sont pas comparables. La plupart des opérateurs définis dans le cas scalaire ne trouvent pas d'équivalent immédiat dans le cas vectoriel. Travailler à partir d'un échantillon permet de déverrouiller la situation, chaque élément de l'image multivaluée pouvant être ordonné selon sa similarité à l'échantillon. Sous réserve d'une relation univoque entre les vecteurs et leur rang dans l'espace des similarités, tous les opérateurs définis pour les images scalaires peuvent alors êtres étendus aux images vectorielles. Des applications sur les images couleur et sur des images médicales sont présentées. Une librairie "Open Source" (vmorph) a été réalisée afin détendre les opérateurs de morphologie mathématique aux vecteurs sur la base de nos travaux.

Стилі APA, Harvard, Vancouver, ISO та ін.

45

Lambert, Thierry. "Réalisation d'un logiciel d'analyse de données." Paris 11, 1986. http://www.theses.fr/1986PA112274.

Повний текст джерела

Стилі APA, Harvard, Vancouver, ISO та ін.

46

Chakkour, Tarik. "Développement, analyse et implémentation d’un modèle financier continu en temps." Thesis, Lorient, 2017. http://www.theses.fr/2017LORIS468/document.

Повний текст джерела

Анотація:

SOFI est un outil logiciel commercialisé par la société MGDIS. Il est destiné aux institutions publiques comme des collectivités locales pour élaborer un budget pluriannuel. SOFI est basé sur une modélisation financière discrète. Par conséquent, le défaut de SOFI est qu’il utilise des tableaux de type Excel. Dans ce travail, nous avons conçu un nouveau modèle utilisant un autre paradigme. Ce nouveau modèle se base sur une modélisation en temps continu et utilise des outils mathématiques de types convolution, intégration, etc. Le modèle financier continu en temps s’appuie sur la théorie de la mesure. Nous avons créé des mesures et des champs, nous les avons utilisés dans notre modélisation pour montrer la cohérence de ce modèle. Nous avons montré dans cette modélisation comment certains aspects du fonctionnement d’un emprunt à taux fixe peuvent être insérés dans un modèle continu en temps. Nous avons construit un modèle financier à taux variable qui permet de modéliser un taux d’emprunt fixe défini à la date d’emprunt. Nous établissons la densité de dépense algébrique σ en fonction de la densité d’emprunt (KE) par un opérateur mathématique. Cet opérateur n’est pas toujours inversible. Nous étudions ce problème inverse du modèle financier sur l’espace des fonctions de carré intégrable définies sur un compact, et sur l’espace de mesure de Radon. Nous avons développé deux librairies industrielles pour implémenter des mesures et des champs pour le modèle financier continu en temps. Nous les avons appelées LemfAN (Library Embedded Finance And Numerical Analysis) et Lemf (Library Embedded Finance). L’intégration et la validation de ces deux librairies
SOFI is a software tool marketed by the company MGDIS. It is designed to the public institutions such local communities to set out multiyear budgets. SOFI is based on a discrete financial modeling. Consequently, the default of SOFI is using tables of type Excel. In this thesis, we build a new model with using an other paradigm. This new model is based on continuous-in-time modeling and uses the mathematical tools such convolution and integration, etc. The continuous-in-time financial model relies on measure theory. We created measures and fields and we used them in our modeling in order to show the consistency of the model. We have showed in this modeling how some aspects of functioning of loan with constant rate could be inserted in continuous-in-time model. We build a financial model with variable rate which allows model a rate of constant loan which is defined at borrowed time. We set the algebraic spending density_ in terms of the loan density_E by a mathematical operator. This operator is not always invertible. We study this inverse problem of the financial model on the space of square-integrable functions defined on a compact, and on radon measure space. We have developed two industrials libraries to implement measures and fields for the continuous-in-time financial model. We called them LemfAN (Library Embedded Finance And Numerical Analysis) and Lemf (Library Embedded Finance). The integration and the validation of these libraries in SOFI are succefully made

Стилі APA, Harvard, Vancouver, ISO та ін.

47

Zinovieva-Leroux, Eléna. "Méthodes symboliques pour la génération de tests de systèmes réactifs comportant des données." Rennes 1, 2004. https://tel.archives-ouvertes.fr/tel-00142441.

Повний текст джерела

Анотація:

La complexité croissante des systèmes réactifs fait que le test devient une technique de plus en plus importante dans ledéveloppement de tels système. Un grand intérêt est notamment accordé au test de conformité qui consiste à vérifier si les comportements d'un système sous test sont corrects par rapport à sa spécification. Au cours des dernières années, les théories et outils de test de conformité pour la génération automatique de testse sont développées. Dans ces théories et algorithmes, les spécifications des systèmes réactifs sont souvent modélisées par différentes variantes des systèmes de transitions. Cependant, ces théories et outils ne prennent pas explicitement en compte les données du système puisque le modèle sous-jacent de système de transitions ne permet pas de le faire. Ceci oblige à énumérer les valeurs des données avant de construire le modèle de système de transitions d'un système, ce qui peut provoquer le problème de l'explosion de l'espace d'états. Cette énumération a également pour effet d'obtenir des cas de test où toutes les données sont instanciées. Or, cela contredit la pratique industrielle où les cas de test sont de vrais programmes avec des variables et des paramètres. La génération de tels cas de test exige de nouveaux modèles et techniques. Dans cette thèse, nous atteignons deux objectifs. D'une part, nous introduisons un modèle appelé système symbolique de transitions à entrée/sortie qui inclut explicitementtoutes les données d'un système réactif. D'autre part, nous proposons et implémentons une nouvelle technique de génération de test qui traite symboliquement les données d'un système en combinant l'approche de génération de test proposée auparavant par notre groupe de recherche avec des techniques d'interprétation abstraite. Les cas de test générés automatiquement par notre technique satisfont des propriétés de correction: ils émettent toujours un verdict correct.

Стилі APA, Harvard, Vancouver, ISO та ін.

48

Abdali, Abdelkebir. "Systèmes experts et analyse de données industrielles." Lyon, INSA, 1992. http://www.theses.fr/1992ISAL0032.

Повний текст джерела

Анотація:

L'analyse du fonctionnement des Systèmes de Production Industrielle s'appuie sur des informations de natures diverses. Une bonne partie d'entre elles se présentant sous forme numérisée, on leur applique des méthodes d'analyse des données dont les résultats doivent être confrontés, puis interprétés à l'aide des autres connaissances. Notre travail s'insère dans le cadre de l'application des techniques de l'Intelligence Artificielle à la Statistique. Il vise en particulier à étudier la faisabilité et le développement d'un Système Expert Statistique dans le domaine des Systèmes de Production Industrielle. Nous avons élaboré ALADIN (Aide Logicielle pour l'Analyse de Données Industrielles), un système destiné à aider un utilisateur non-spécialiste à analyser des données recueillies sur des procédés industriels. L'architecture de ce système est flexible et allie aspect qualitatif (connaissances sur les procédés industriels et connaissances sur les méthodes statistiques et d'analyse de données) et aspect quantitatif (collection de programmes d'analyse). Pour l'instant, nous nous sommes limités aux problèmes d'Analyse en Composantes Principales. Outre l'aspect industriel, ALADIN présente l'avantage de fournir une assistance au niveau de chacun des nombreux maillons de la conduite d'une analyse de données et particulièrement en amont de l'analyse proprement dite i. E. Lors de la phase de prétraitement et de préparation des données: cette étape, toujours nécessaire compte tenu de la nature des mesures, est en effet généralement longue et fastidieuse
To analyses industrial process behavio, many kinds of information are needed. As tye ar mostly numerical, statistical and data analysis methods are well-suited to this activity. Their results must be interpreted with other knowledge about analysis prcess. Our work falls within the framework of the application of the techniques of the Artificial Intelligence to the Statistics. Its aim is to study the feasibility and the development of statistical expert systems in an industrial process field. The prototype ALADIN is a knowledge-base system designed to be an intelligent assistant to help a non-specialist user analyze data collected on industrial processes, written in Turbo-Prolong, it is coupled with the statistical package MODULAD. The architecture of this system is flexible and combing knowledge with general plants, the studied process and statistical methods. Its validation is performed on continuous manufacturing processes (cement and cast iron processes). At present time, we have limited to principal Components analysis problems

Стилі APA, Harvard, Vancouver, ISO та ін.

49

Roume, Cyril. "Analyse et restructuration de hiérarchies de classes." Montpellier 2, 2004. http://www.theses.fr/2004MON20088.

Повний текст джерела

Стилі APA, Harvard, Vancouver, ISO та ін.

50

Garoche, Pierre-Loïc. "Analyse statistique d'un calcul d'acteurs par interprétation abstraite." Toulouse, INPT, 2008. http://ethesis.inp-toulouse.fr/archive/00000629/.

Повний текст джерела

Анотація:

Le modèle des Acteurs, introduit par Hewitt et Agha à la fin des années 80, décrit un système concurrent comme un ensemble d'agents autonomes au comportement non uniforme et communiquant de façon point-à-point par l'envoi de messages étiquetés. Le calcul CAP, proposé par Colaço, est un calcul de processus basé sur ce modèle qui permet de décrire sans encodage complexe des systèmes réalistes non triviaux. Ce calcul permet, entre autre, la communication de comportements via les messages et est, en ce sens, un calcul d'ordre supérieur. L'analyse de propriétés sur ce calcul a déjà fait l'objet de plusieurs travaux, essentiellement par inférence de type en utilisant des types comportementaux et du sous-typage. Par ailleurs, des travaux plus récents, effectués par Venet puis Feret, proposent une utilisation de l'interprétation abstraite pour l'analyse de calculs de processus. Ces approches permettent de calculer des propriétés non uniformes : elles permettent, par exemple, de différencier les instances récursives d'un même processus. Cette thèse s'inscrit donc dans la suite de ces deux approches, en appliquant l'interprétation abstraite à l'analyse de CAP. Suivant le cadre proposé par Feret, CAP est, tout d'abord, exprimé dans une forme non standard facilitant les analyses. L'ensemble des configurations atteignables est ensuite sur-approximé via une représentation, correcte par construction, dans des domaines abstraits. [. . . ]
The Actor model, introduced by Hewitt and Agha in the late 80s, describes a concurrent communicating system as a set of autonomous agents, with non uniform interfaces and communicating by the use of labeled messages. The CAP process calculus, proposed by Colaço, is based on this model and allows to describe non trivial realistic systems, without the need of complex encodings. CAP is a higher-order calculus: messages can carry actor behaviors. Multiple works address the analysis of CAP properties, mainly by the use of inference-based type systems using behavioral types and sub-typing. Otherwise, more recent works, by Venet and later Feret, propose the use of abstract interpretation to analyze process calculi. These approaches allow to compute non-uniform properties. For example, they are able to differentiate recursive instances of the same thread. This thesis is at the crossroad of these two approaches, applying abstract interpretation to the analysis of CAP. Following the framework of Feret, CAP is firstly expressed in a non standard form, easing its analysis. The set of reachable states is then over-approximated via a sound by construction representation within existing abstract domains. [. . . ]

Стилі APA, Harvard, Vancouver, ISO та ін.

Дисертації з теми "Analyse des logiciels malveillants"

Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями