Dissertations / Theses on the topic 'Sécurité de la mémoire'
To see the other types of publications on this topic, follow the link: Sécurité de la mémoire.
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the top 50 dissertations / theses for your research on the topic 'Sécurité de la mémoire.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Browse dissertations / theses on a wide variety of disciplines and organise your bibliography correctly.
1
Ouattara, Frédéric. "Primitives de sécurité à base de mémoires magnétiques." Thesis, Montpellier, 2020. http://www.theses.fr/2020MONTS072.
Abstract:
Les mémoires magnétiques (MRAM) font partie des technologies de mémoires non volatiles émergentes ayant connu un développement rapide cette dernière décennie. Un des avantages de cette technologie réside dans les domaines d’applications variées dans lesquelles elle peut intervenir. En plus de sa fonction principale de stockage d’information, la MRAM est utilisée de nos jours dans des applications de type capteurs, récepteur RF et sécurité matérielle. Dans cette thèse, nous nous sommes intéressés à l’utilisation des MRAM dans la conception des primitives de sécurité matérielle élémentaires. Dans un premier temps, une exploration dans la conception de TRNG (True Random Number Generator) basée sur des mémoires de type STT-MRAM (Spin Transfert Torque MRAM) a été menée dans le but de réaliser un démonstrateur et de prouver son efficacité pour les applications sécurisées. Les méthodes d’extraction d’aléa dans les mémoires STT et TAS (Thermally Assisted Switching) sont présentées. Nous avons ainsi évalué ces mémoires magnétiques dans le cadre des TRNG mais également pour la génération de PUF (Physically Unclonable Functions) sur des dispositifs physiquesMagnetic memories (MRAM) are one of the emerging non-volatile memory technologies that have experienced rapid development over the past decade. One of the advantages of this technology lies in the varied fields of application in which it can be used. In addition to its primary function of storing information, MRAM is nowadays used in applications such as sensors, RF receivers and hardware security. In this thesis, we are interested in the use of MRAMs in the design of elementary hardware security primitives. Initially, an exploration in the design of TRNG (True Random Number Generator) based on STT-MRAM (Spin Transfert Torque MRAM) type memories was carried out with the aim of producing a demonstrator and proving its effectiveness for secure applications. Random extraction methods in STT and TAS (Thermally Assisted Switching) memories are presented. We have thus evaluated these magnetic memories within the framework of TRNGs but also for the generation of PUFs (Physically Unclonable Functions) on physical devices
2
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.
Abstract:
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.
3
Millon, Etienne. "Analyse de sécurité de logiciels système par typage statique." Electronic Thesis or Diss., Paris 6, 2014. http://www.theses.fr/2014PA066120.
Abstract:
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 COperating system kernels need to manipulate data that comes from user programs through system calls. If it is done in an incautious manner, a security vulnerability known as the Confused Deputy Problem can lead to information disclosure or privilege escalation. The goal of this thesis is to use static typing to detect the dangerous uses of pointers that are controlled by userspace. Most operating systems are written in the C language. We start by isolating Safespeak, a safe subset of it. Its operational semantics as well as a type system are described, and the classic properties of type safety are established. Memory states are manipulated using bidirectional lenses, which can encode partial updates to states and variables. A first analysis is described, that identifies integers used as bitmasks, which are a common source of bugs in C programs. Then, we add to Safespeak the notion of pointers coming from userspace. This breaks type safety, but it is possible to get it back by assigning a different type to the pointers that are controlled by userspace. This distinction forces their dereferencing to be done in a controlled fashion. This technique makes it possible to detect two bugs in the Linux kernel: the first one is in a video driver for an AMD video card, and the second one in the ptrace system call for the Blackfin architecture
4
Eluard, Marc. "Analyse de sécurité pour la certification d'applications java card." Rennes 1, 2001. http://www.theses.fr/2001REN10079.
5
Clavier, Christophe. "De la sécurité physique des crypto-systèmes embarqués." Versailles-St Quentin en Yvelines, 2007. http://www.theses.fr/2007VERS0028.
Abstract:
Dans un monde défiant, l'augmentation du nombre et de la diversité des applications numériques ont rendu nécessaire l'existence d'un objet pratique intégrant les fonctions cryptographiques requises pour les besoins quotidiens de sécurité des transactions, de confidentialité des échanges, d'identification du porteur ou encore d'authentification pour l'accès à un service. Parmi les dispositifs cryptographiques embarqués aptes à proposer ces fonctionnalités, la carte à puce est certainement le plus utilisé de nos jours. Sa portabilité (un porte-feuille peut en contenir une dizaine) et sa capacité à protéger les données et programmes qu'elle contient contre les attaques intrusives, lui confèrent naturellement sa fonction essentielle de ``bunker'' pour le stockage de clés et l'exécution d'algorithmes cryptographiques dans les usages mobiles nécessitant un haut degré de sécurité. Évidemment nécessaire, la conception de schémas cryptographiques mathématiquement robustes, voire prouvés sûrs dans certains modèles, s'est malgré tout révélée insuffisante depuis la publication en 1996 des premières attaques physiques. Exploitant des vulnérabilités liées à la mise en oeuvre concrète des routines de sécurité et à leur implémentation, ces menaces comprennent l'analyse de canaux auxiliaires permettant d'obtenir de l'information sur l'état interne d'un processus, et l'exploitation de fautes provoquées ouvrant la voie à certaines cryptanalyses autrement impossibles. Cette thèse présente une série de travaux de recherche dans le domaine de la sécurité physique des crypto-systèmes embarqués. Deux parties de ce document sont consacrées à la description de certaines attaques et à l'étude de l'efficacité de possibles contre-mesures. Une troisième partie aborde le domaine particulier, et encore très peu exploré, de l'applicabilité des attaques physiques dans le cas où la fonction cryptographique considérée est en grande partie, voire totalement, inconnue de l'adversaireIn a world full of threats, the development of widespread digital applications has led to the need for a practical device containing cryptographic functions that provide the everyday needs for secure transactions, confidentiality of communications, identification of the subject or authentication for access to a particular service. Among the cryptographic embedded devices ensuring these functionalities, smart cards are certainly the most widely used. Their portability (a wallet may easily contain a dozen) and their ability to protect its data and programs against intruders, make it as the ideal ``bunker'' for key storage and the execution of cryptographic functions during mobile usage requiring a high level of security. Whilst the design of mathematically robust (or even proven secure in some models) cryptographic schemes is an obvious requirement, it is apparently insufficient in the light of the first physical attacks that were published in 1996. Taking advantage of weaknesses related to the basic implementation of security routines, these threats include side-channel analysis which obtains information about the internal state of the process, and the exploitation of induced faults allowing certain cryptanalysis to be performed which otherwise would not have been possible. This thesis presents a series of research works covering the physical security of embedded cryptosystems. Two parts of this document are dedicated to the description of some attacks and to a study of the efficiency of conceivable countermeasures. A third part deals with that particular and still mainly unexplored area which considers the applicability of physical attacks when the cryptographic function is, partly or totally, unknown by the adversary
6
Lacroix, Patrice. "RTL-Check : a practical static analysis framework to verify memory safety and more." Thesis, Université Laval, 2006. http://www.theses.ulaval.ca/2006/23909/23909.pdf.
Abstract:
Puisque les ordinateurs sont omniprésents dans notre société et que, de plus en
plus, nous dépendons de programmes pour accomplir nos activités de tous les jours,
les bogues peuvent parfois avoir des conséquences cruciales. Une grande proportion des
programmes existants sont écrits en C ou en C++ et la plupart des erreurs avec ces
langages sont dues à l’absence de sûreté d’accès à la mémoire. Notre objectif à long
terme est d’être en mesure de vérifier si un programme C ou C++ accède correctement
à la mémoire malgré les défauts de ces langages.
À cette fin, nous avons créé un cadre de développement d’analyses statiques que
nous présentons dans ce mémoire. Il permet de construire des analyses à partir de petits
composants réutilisables qui sont liés automatiquement par métaprogrammation. Il
incorpore également le modèle de conception (design pattern) du visiteur et des algorithmes
utiles pour faire de l’analyse statique. De plus, il fournit un modèle objet pour
le RTL, la représentation intermédiaire de bas niveau pour tous les langages supportés
par GCC. Ceci implique qu’il est possible de concevoir des analyses indépendantes des
langages de programmation.
Nous décrivons également les modules que comporte l’analyse statique que nous
avons développée à l’aide de notre cadre d’analyse et qui vise à vérifier si un programme
respecte les règles d’accès à la mémoire. Cette analyse n’est pas complète, mais elle
est conçue pour être améliorée facilement. Autant le cadre d’analyse que les modules
d’analyse des accès à la mémoire sont distribués dans RTL-Check, un logiciel libre.Since computers are ubiquitous in our society and we depend more and more on programs to accomplish our everyday activities, bugs can sometimes have serious consequences. A large proportion of existing programs are written in C or C++ and the main source of errors with these programming languages is the absence of memory safety. Our long term goal is to be able to verify if a C or C++ program accesses memory correctly in spite of the deficiencies of these languages. To that end, we have created a static analysis framework which we present in this thesis. It allows building analyses from small reusable components that are automatically bound together by metaprogramming. It also incorporates the visitor design pattern and algorithms that are useful for the development of static analyses. Moreover, it provides an object model for RTL, the low-level intermediate representation for all languages supported by GCC. This implies that it is possible to design analyses that are independent of programming languages. We also describe the modules that comprise the static analysis we have developed using our framework and which aims to verify if a program is memory-safe. This analysis is not yet complete, but it is designed to be easily improved. Both our framework and our memory access analysis modules are distributed in RTL-Check, an open-source project.
7
Saleh, Hayder. "Une architecture novatrice de sécurité à base de carte à puce Internet." Versailles-St Quentin en Yvelines, 2002. http://www.theses.fr/2002VERSA009.
Abstract:
Le protocole Smart TP, introduit dans ce mémoire, propose une nouvelle architecture de communication d'une carte à puce Internet permettant à la carte d'agir comme un vrai noeud d'Internet. Ainsi, cette carte pourra participer aux protocoles d'Internet les plus répandus de manière plus active et indépendamment du terminal hôte. La sécurité sur Internet est une des préoccupations majeures de notre société, mettant en action différents aspects, notamment économiques et technologiques. Le déploiement de la carte à puce en tant que dispositif hautement protégé au service des protocoles de sécutité sur Internet constitue le coeur du sujet de cette thèse. Les défis technologiques révélés par ce déploiement ont été étudiés et évalués à travers cette recherche. Une implémentation du protocole proposé a été réalisée pour loger un serveur WEB conforme aux normes Internet dans une carte à puce Java. Ceci a permis d'étudier les problèmes de performance et de faisabilité, ainsi que de découvrir les possibilités d'amélioration de ce protocole (SmartTP). Une démonstration à grande échelle a été ensuite conduite pour explorer les débouchés industriels de cette technologie. Une analyse approfondie a été faite sur l'implication d'une carte à puce dans le protocole SSL. Ce dernier, est pris comme un exemple pour extrapoler les points forts et les points faibles de la carte dans un environnement Internet. Les problèmes issus de l'exemple SSL et les recommandations apportées sont largement valables pour les autres protocoles et constituent les fruits de cette recherche.
8
Davidson, Tremblay Patrick. "Protection et intégrité des systèmes embarqués réseautés." Mémoire, Université de Sherbrooke, 2014. http://hdl.handle.net/11143/5896.
Abstract:
Depuis plusieurs années, l'utilisation et le déploiement de systèmes embarqués est en plein essor.
Ces systèmes complexes, autrefois isolés les uns des autres, peuvent aujourd'hui communiquer entre eux afin de répondre à de nouveaux besoins.
L'échange de données entre ces dispositifs et la facilité de les administrer à distance présentent deux avancées technologiques importantes. Par contre, d'un point de vue de la sécurité, cela les rend plus susceptibles de subir les attaques de pirates informatiques et de voir l'intégrité de leur micrologiciel compromise. Cette réalité est particulièrement vraie pour les systèmes embarqués réseautés domestiques qui sont en général moins bien protégés que leurs homologues en milieux industriels.
L'objectif de ce travail de recherche consiste à identifier et éliminer les failles de sécurité dans les systèmes embarqués réseautés domestiques. La phase d'analyse est primordiale, puisque les vulnérabilités dans ces systèmes ne peuvent être contrôlées et éliminées que si elles sont bien identifiées. Cette analyse permettra ensuite de mieux comprendre le déroulement ainsi que l'ampleur de telles attaques afin de mieux s'en prémunir. Une fois cette phase complétée, une exploration de diverses technologies pouvant mener à la protection et à l'intégrité de ces systèmes sera réalisée. Quelques-unes de ces technologies de protection seront finalement employées lors d'une tentative de sécurisation d'un système embarqué réseauté domestique.
9
Elbaz, Reouven. "Mécanismes Matériels pour des TransfertsProcesseur Mémoire Sécurisés dans lesSystèmes Embarqués." Phd thesis, Université Montpellier II - Sciences et Techniques du Languedoc, 2006. http://tel.archives-ouvertes.fr/tel-00142209.
Abstract:
Les systèmes embarqués actuels (téléphone portable, assistant personnel...) ne sont pas considéréscomme des hôtes de confiance car toute personne y ayant accès, sont des attaquants potentiels. Les données
contenues dans ces systèmes peuvent être sensibles (données privées du propriétaire, mot de passe, code d'un
logiciel...) et sont généralement échangées en clair entre le Système sur Puces (SoC – System on Chip) et la
mémoire dans laquelle elles sont stockées. Le bus qui relie ces deux entités constitue donc un point faible : un
attaquant peut observer ce bus et récupérer le contenu de la mémoire, ou bien a la possibilité d'insérer du code
afin d'altérer le fonctionnement d'une application s'exécutant sur le système. Afin de prévenir ce type d'attaque,
des mécanismes matériels doivent être mis en place afin d'assurer la confidentialité et l'intégrité des données.
L'approche conventionnelle pour atteindre cet objectif est de concevoir un mécanisme matériel pour chaque
service de sécurité (confidentialité et intégrité). Cette approche peut être implantée de manière sécurisée mais
empêche toute parallélisation des calculs sous-jacents.
Les travaux menés au cours de cette thèse ont dans un premier temps, consisté à faire une étude des
techniques existantes permettant d'assurer la confidentialité et l'intégrité des données. Dans un deuxième temps,
nous avons proposé deux mécanismes matériels destinés à la sécurisation des transactions entre un processeur et
sa mémoire. Un moteur de chiffrement et de contrôle d'intégrité parallélisé, PE-ICE (Parallelized Encryption and
Integrity Checking Engine) a été conçu. PE-ICE permet une parallélisation totale des opérations relatives à la
sécurité aussi bien en écriture qu'en lecture de données en mémoire. Par ailleurs, une technique basée sur une
structure d'arbre (PRV-Tree – PE-ICE protected Reference Values) comportant la même propriété de
parallélisation totale, a été spécifiée afin de réduire le surcoût en mémoire interne impliqué par les mécanismes de sécurité
10
Kamel, Nassima. "Sécurité des cartes à puce à serveur Web embarqué." Limoges, 2012. https://aurore.unilim.fr/theses/nxfile/default/9dc553cd-e9df-4530-a716-d3191d68dfa0/blobholder:0/2012LIMO4039.pdf.
Abstract:
Les cartes à puces sont des dispositifs sécurisés, de plus en plus utilisés dans le monde. Leur succès est principalement dû à leur aspect tamper-resistant qui permet de stocker des informations sensibles (clés de chiffrement) de manière sécurisée. Vu les nombreux sensibles domaines d’utilisation des cartes à puce (bancaire, médical, téléphonie), plusieurs recherches se sont intéressés à la sécurité et aux attaques possibles sur ces dispositifs. La nouvelle génération de cartes à puce définit un serveur Web embarqué. Il existe principalement deux types de spécifications pour ces nouveaux dispositifs, la première a été établie par l’organisation OMA qui propose un simple serveur HTTP nommé Smart Card Web Serveur (SCWS) indépendant de la plateforme d’exécution. La seconde est une nouvelle version de Java Card proposée par Sun Microsystems (actuellement Oracle), nommée Java Card 3, édition connectée ; elle inclue le support de l’API Java servlet 2. 4, et une amélioration significativement de l’API Java Card (thread, String, etc. ) et des fonctionnalités de sécurité supportées. L’intégration du serveur Web dans la carte à puce apporte un ensemble d’avantages et définit un nouvel usage de la carte à puce. En effet, en plus de l’aspect authentification robuste que la carte peut désormais fournir sur le réseau, l’utilisation des standards du Web permet d’avoir une expérience utilisateur continue et enrichit l’aspect et la convivialité des interfaces fournies via un navigateur Web. Face à ces avantages, les risques d’attaques augmentent. En plus des attaques classiques connues sur les cartes à puce (physiques et logiques), certaines attaques Web connues sur des applications Web standards peuvent se reproduire sur les cartes à puce. Parmi ces attaques, la Cross Site Scripting (appelée aussi XSS) est l’une des plus répandues ; elle est simple à réaliser mais ses conséquences peuvent être très graves. Cette attaque exploite des applications vulnérables qui ne filtrent pas les données non fiables (entrée par un utilisateur) avant de les utiliser. Elle consiste à injecter un code malicieux dans une entrée fournie par l’application, qui est ensuite retourné dans une ressource de l’application et exécuté dans le navigateur Web de la victime. D’autre part, les spécifications des cartes à serveur Web embarqué définissent des protocoles (HTTP, BIP, TCP/IP) qui doivent nécessairement être implémentés pour assurer la communication de la carte avec le navigateur Web et sur le réseau. Des failles d’implémentation de ces protocoles peuvent engendrer des vulnérabilités facilitant les attaques sur les cartes à puce. Dans cette thèse nous nous intéressons à la sécurité des cartes à puce à serveur Web embarqué à deux niveaux. Le premier concerne la sécurité des applications Web contre des attaques XSS. Nous proposons dans ce cadre un outil d’analyse statique des applications Web Java Card 3, qui a pour objectif de vérifier qu’une application est sécurisée contre ces attaques, incluant un filtrage des données non fiables. Notre outil peut être considéré comme un outil de certification de la robustesse des applications Web avant leur chargement dans la carte. Nous avons également implémenté une API de filtrage que le développeur peut importer dans son application. Le second niveau de sécurité exploré, concerne l’implémentation du protocole HTTP; nous suggérons un outil de fuzzing pour tester la conformité et la robustesse du protocole HTTP implémenté dans une carte. Cet outil apporte un ensemble d’optimisations qui réduit le temps du fuzzing et génère des données de test de manière intelligenteSmart cards are widely used secure devices in today’s world, which can store data in a secured manner and ensure data security during transactions. The success of smart card is mainly due to their tamper-resistant nature which allows them to store sensitive data’s like cryptographic keys. Since they are using in multiple secure domains, like banking, health insurance, etc. More and more researches are taken place in this domain for security and attacks. The last generation of smart card, defines an embedded web server. There are two types of specifications for these devices, the first one is defined by OMA organisation that propose a simple HTTP web server named Smart Card Web Server (SCWS), the second is proposed by Sun Microsystems (currently Oracle), consists of a Java card 3 connected edition platform, that includes a Java servlet 2. 4 API with improved Java Card API and security features. In addition to network benefits from the robustness of smart card, the use of web standards provide a continuous user experience, equivalent to that seen while surfing on the internet and it enhances the look and feel of GUI interfaces. The GUI interfaces are accessible from a browser which is located on the terminal on which the card is connected. However, in addition to the classical attacks (physical and logical), the integration of web server on smart card, exposes the smart card to some existing classical web application attacks. The most important one is the cross site scripting attack, also named XSS. It consists of injecting malicious data to the given web application inputs and if the resource returned to the browser includes the malicious code, it will be interpreted and executed, causing an attack. A web application is vulnerable to XSS if it uses an untrusted data without filtering malicious characters before. On the other hand, to ensure the communication between web applications and browser or other network entities, it is necessary to integrate some protocols to the smart card, for example HTTP, BIP or TCP/IP. The vulnerabilities in the implementation of these protocols can facilitate some attacks. Our contribution on this thesis is divided in two parts, in the first part, we are interested on the security of web applications against XSS attack. We suggest a static analysis tool, based on tainting approach, that allow to verify if a web application is secured or not, including filtering data in all insertion points where XSS is possible. We also implement, an API filter, compatible with Java Card 3 platform, that developers can import during the development of their applications. The second part consists of verifying the conformance and the robustness of the implemented HTTP protocol. For that we propose an intelligent fuzzing tool that includes a set of optimisations that allows to reduce the time of fuzzing
11
Sifakis, Emmanuel. "Programmation efficace et sécurisé d'applications à mémoire partagée." Phd thesis, Université de Grenoble, 2013. http://tel.archives-ouvertes.fr/tel-00823054.
Abstract:
L'utilisation massive des plateformes multi-cœurs et multi-processeurs a pour effet de favoriser la programmation parallèle à mémoire partagée. Néanmoins, exploiter efficacement et de manière correcte le parallélisme sur ces plateformes reste un problème de recherche ouvert. De plus, leur modèle d'exécution sous-jacent, et notamment les modèles de mémoire "relâchés", posent de nouveaux défis pour les outils d'analyse statiques et dynamiques. Dans cette thèse nous abordons deux aspects importants dans le cadre de la programmation sur plateformes multi-cœurs et multi-processeurs: l'optimisation de sections critiques implémentées selon l'approche pessimiste, et l'analyse dynamique de flots d'informations. Les sections critiques définissent un ensemble d'accès mémoire qui doivent être exécutées de façon atomique. Leur implémentation pessimiste repose sur l'acquisition et le relâchement de mécanismes de synchronisation, tels que les verrous, en début et en fin de sections critiques. Nous présentons un algorithme générique pour l'acquisition/relâchement des mécanismes de synchronisation, et nous définissons sur cet algorithme un ensemble de politiques particulier ayant pour objectif d'augmenter le parallélisme en réduisant le temps de possession des verrous par les différentes threads. Nous montrons alors la correction de ces politiques (respect de l'atomicité et absence de blocages), et nous validons expérimentalement leur intérêt. Le deuxième point abordé est l'analyse dynamique de flot d'information pour des exécutions parallèles. Dans ce type d'analyse, l'enjeu est de définir précisément l'ordre dans lequel les accès à des mémoires partagées peuvent avoir lieu à l'exécution. La plupart des travaux existant sur ce thème se basent sur une exécution sérialisée du programme cible. Ceci permet d'obtenir une sérialisation explicite des accès mémoire mais entraîne un surcoût en temps d'exécution et ignore l'effet des modèles mémoire relâchées. A contrario, la technique que nous proposons permet de prédire l'ensemble des sérialisations possibles vis-a-vis de ce modèle mémoire à partir d'une seule exécution parallèle ("runtime prediction"). Nous avons développé cette approche dans le cadre de l'analyse de teinte, qui est largement utilisée en détection de vulnérabilités. Pour améliorer la précision de cette analyse nous prenons également en compte la sémantique des primitives de synchronisation qui réduisent le nombre de sérialisations valides. Les travaux proposé ont été implémentés dans des outils prototype qui ont permit leur évaluation sur des exemples représentatifs.
12
Buret, Pierrick. "Sécurité temps réel dans les systèmes embarqués critiques." Thesis, Limoges, 2015. http://www.theses.fr/2015LIMO0140/document.
Abstract:
La croissance des flux d'information à travers le monde est responsable d'une importante utilisation de systèmes embarqués temps-réel, et ce notoirement dans le domaine des satellites. La présence de ces systèmes est devenue indispensable pour la géolocalisation, la météorologie, ou les communications. La forte augmentation du volume de ces matériels, impactée par l'afflux de demande, est à l'origine de l'accroissement de la complexité de ces derniers. Grâce à l'évolution du matériel terrestre, le domaine aérospatial se tourne vers de nouvelles technologies telles que les caches, les multi-coeurs, et les hyperviseurs. L'intégration de ces nouvelles technologies est en adéquation avec de nouveaux défis techniques. La nécessité d'améliorer les performances de ces systèmes induit le besoin de réduction du coût de fabrication et la diminution du temps de production. Les solutions technologiques qui en découlent apportent pour majeure partie des avantages en matière de diminution du nombre global de satellites à besoin constant. La densité d'information traitée est parallèlement accrue par l'augmentation du nombre d'exploitants pour chaque satellite. En effet, plusieurs clients peuvent se voir octroyer tout ou partie d'un même satellite. Intégrer les produits de plusieurs clients sur une même plateforme embarquée la rend vulnérable. Augmenter la complexité du système rend dès lors possible un certain nombre d'actes malveillants. Cette problématique autrefois à l'état d'hypothèse devient aujourd'hui un sujet majeur dans le domaine de l'aérospatial. Figure dans ce document, en premier travail d'exploration, une présentation des actes malveillants sur système embarqué, et en particulier ceux réalisés sur système satellitaire. Une fois le risque exposé, je développe la problématique temps-réel. Je m'intéresse dans cette thèse plus précisément à la sécurité des hyperviseurs spatiaux. Je développe en particulier deux axes de recherche. Le premier porte sur l'évolution des techniques de production et la mise en place d'un système de contrôle des caractéristiques temporelles d'un satellite. Le deuxième axe améliore les connaissances techniques sur un satellite en cours de fonctionnement et permet une prise de décision en cas d'acte malveillant. Je propose plus particulièrement une solution physique permettant de déceler une anomalie sur la gestion des mémoires internes au satellite. En effet, la mémoire est un composant essentiel du fonctionnement du système, et ses propriétés communes entre tous les clients la rend particulièrement vulnérable. De plus, connaître le nombre d'accès en mémoire permet un meilleur ordonnancement et une meilleure prédiction d'un système temps réel. Notre composant permet la détection et l'interprétation d'une potentielle attaque ou d'un problème de sûreté de fonctionnement. Cette thèse met en évidence la complémentarité des deux travaux proposés. En effet, la mesure du nombre d'accès en mémoire peut se mesurer via un algorithme génétique dont la forme est équivalente au programme cherchant le pire temps d'exécution. Il est finalement possible d'étendre nos travaux de la première partie vers la secondeSatellites are real-time embedded systems and will be used more and more in the world. Become essential for the geo-location, meteorology or communications across the planet, these systems are increasingly in demand. Due to the influx of requests, the designers of these products are designing a more and more complex hardware and software part. Thanks to the evolution of terrestrial equipment, the aero-space field is turning to new technologies such as caches, multi-core, and hypervisor. The integration of these new technologies bring new technical challenges. In effect, it is necessary to improve the performance of these systems by reducing the cost of manufacturing and the production time. One of the major advantages of these technologies is the possibility of reducing the overall number of satellites in space while increasing the number of operators. Multiple clients softwares may be together today in a same satellite. The ability to integrate multiple customers on the same satellite, with the increasing complexity of the system, makes a number of malicious acts possible. These acts were once considered as hypothetical. Become a priority today, the study of the vulnerability of such systems become major. In this paper, we present first work a quick exploration of the field of malicious acts on onboard system and more specifically those carried out on satellite system. Once the risk presentation we will develop some particular points, such as the problematic real-time. In this thesis we are particularly interested in the security of space hypervisors. We will develop precisely 2 lines of research. The first axis is focused on the development of production technics and implementing a control system of a satellite temporal characteristics. The objective is to adapt an existing system to the constraints of the new highly complex systems. We confront the difficulty of measuring the temporal characteristics running on a satellite system. For this we use an optimization method called dynamic analysis and genetic algorithm. Based on trends, it can automatically search for the worst execution time of a given function. The second axis improves the technical knowledge on a satellite in operation and enables decision making in case of malicious act. We propose specifically a physical solution to detect anomalies in the management of internal memory to the satellite. Indeed, memory is an essential component of system operation, and these common properties between all clients makes them particularly vulnerable to malicious acts. Also, know the number of memory access enables better scheduling and better predictability of a real time system. Our component allows the detection and interpretation of a potential attack or dependability problem. The work put in evidence the complementarity of the two proposed work. Indeed, the measure of the number of memory access that can be measured via a genetic algorithm whose shape is similar to the program seeking the worst execution time. So we can expand our work of the first part with the second
13
Kamel, Sarah. "Sécurité pour les réseaux sans fil." Thesis, Paris, ENST, 2017. http://www.theses.fr/2017ENST0011/document.
Abstract:
Aujourd’hui, le renforcement de la sécurité des systèmes de communications devient une nécessité, par anticipation du développement des ordinateurs quantiques et des nouvelles attaques qui en découleront. Cette thèse explore deux techniques complémentaires permettant d’assurer la confidentialité des données transmises sur des liens sans-fils. Dans la première partie de ce travail, nous nous intéressons au schéma de cryptographie à clé publique basée sur des réseaux de points, qui représente une des techniques les plus prometteuses pour la cryptographie post-quantique. En particulier, nous considérons le cryptosystème Goldreich-Goldwasser-Halevi (GGH), pour lequel nous proposons un nouveau schéma utilisant les GLD. Dans la seconde partie de ce travail, nous étudions la sécurité des canaux de diffusion multi-utilisateur, ayant accès à des mémoires de caches, en présence d'un espion. Nous considérons deux contraintes de sécurité: la contrainte de sécurité individuelle et la contrainte de sécurité jointe. Nous dérivons des bornes supérieure et inférieure pour le compromis sécurisé capacité-mémoire en considérant différentes distributions de cache. Afin d'obtenir la borne inférieure, nous proposons plusieurs schémas de codage combinant codage wiretap, codage basé sur la superposition et codage piggyback. Nous prouvons qu'il est plus avantageux d'allouer la mémoire de cache aux récepteurs les plus faiblesToday, there is a real need to strengthen the communication security to anticipate the development of quantum computing and the eventual attacks arising from it. This work explores two complementary techniques that provide confidentiality to data transmitted over wireless networks. In the first part, we focus on lattice-based public-key cryptography, which is one of the most promising techniques for the post-quantum cryptography systems. In particular, we focus on the Goldreich-Goldwasser-Halevi (GGH) cryptosystem, for which we propose a new scheme using GLD lattices. In the second part of this work, we study the security of multi-user cache-aided wiretap broadcast channels (BCs) against an external eavesdropper under two secrecy constraints: individual secrecy constraint and joint secrecy constraint. We compute upper and lower bounds on secure capacity-memory tradeoff considering different cache distributions. To obtain the lower bound, we propose different coding schemes that combine wiretap coding, superposition coding and piggyback coding. We prove that allocation of the cache memory to the weaker receivers is the most beneficial cache distribution scenario
14
Barbu, Guillaume. "De la sécurité des platesformes JavaCardTM face aux attaques matérielles." Electronic Thesis or Diss., Paris, ENST, 2012. http://www.theses.fr/2012ENST0037.
Abstract:
Les cartes à puce jouent un rôle crucial dans de nombreuses applications que nous utilisons quotidiennement : paiement par carte bancaire, téléphonie mobile, titres de transport électroniques, etc. C'est dans ce contexte que la technologie Java Card s'est imposée depuis son introduction en 1996, réduisant les coûts de développement et de déploiement d'applications pour cartes à puce et permettant la cohabitation de plusieurs applications au sein d'une même carte. La communauté scientifique a rapidement démontré que la possibilité donnée à un attaquant d'installer des applications sur les cartes représente une menace. Mais dans le même temps, la sécurité des systèmes embarqués a également été un sujet d'étude très productif, révélant que des algorithmes cryptographiques considérés comme sûrs pouvaient être facilement cassés si leurs implémentations ne prenaient pas en compte certaines propriétés physiques des composants électroniques qui les accueillent. En particulier, une partie des attaques publiées repose sur la capacité de l'attaquant à perturber physiquement le composant pendant qu'un calcul est exécuté. Ces attaques par injections de fautes n'ont que très peu été étudiées dans le contexte de la technologie Java Card. Cette thèse étudie et analyse la sécurité des Java Cards contre des attaques combinant injections de fautes et installations d'applications malicieuses. Tout d'abord, nous présentons différents chemins d'attaques combinées et exposons dans quelle mesure ces attaques permettent de casser différents mécanismes sécuritaires de la plateforme. En particulier, notre analyse sécuritaire permet de démontrer que la propriété de sûreté du typage, l'intégrité du flot de contrôle, ainsi que le mécanisme d'isolation des applications peuvent être contournés et exploités par des combinaisons adéquates. Puis, nous présentons différentes approches permettant d'améliorer la résistance de la plateforme Java Card ainsi que des applications qu'elle accueille contre des attaques combinées. Ainsi, nous définissons plusieurs contremesures rendant les attaques exposées ainsi que certaines attaques de l'état de l'art inopérantes, et ce en gardant à l'esprit les fortes contraintes inhérentes au monde des cartes à puceSmart cards play a key role in various applications we use on a daily basis: payment, mobile communication, public transports, etc. In this context, the Java Card technology has evolved since its introduction in the mid-nineties to become nowadays the world leading smart card platform. In the context of Java Card, researches on security have revealed that the possibility of loading malicious applications represents a real threat. In the meantime, the scientific community has also paid interest to the security of embedded cryptography, revealing that theoretically strong cryptosystems can be easily broken if their implementation does not take into account certain physical properties of the underlying hardware device. In particular, a part of the published attacks relies on the attacker’s capacity to physically perturb the component during a cryptographic operation. These latter fault attacks have been rarely considered in the literature in the Java Card context. In this thesis, we study and evaluate the security of Java Cards against the combination of fault and software attacks in order to enhance it. First, we present various attack paths involving both hardware and software attacks and expose how these attacks allow to break various security mechanisms of Java Cards. In particular, our security analysis proves that the type-safety property, the control-flow integrity and the application isolation can be tampered with by the combination of adequate fault injections and malicious applications. Then, with regards to the goal of this thesis and the results of our security analysis, we present different approaches allowing to improve the resistance of Java Cards and Java Card applications against combined attacks. Thus we define several countermeasures against the attack we exposed as well as against some of the state-of-the-art attacks, always bearing in mind the strong constraints relative to smart cards
15
Séré, Ahmadou Al Khary. "Tissage de contremesures pour machines virtuelles embarquées." Limoges, 2010. http://aurore.unilim.fr/theses/nxfile/default/ec9d960e-5234-4fd7-a38f-bd8107443f05/blobholder:0/2010LIMO4017.pdf.
Abstract:
L'objectif de ce travail de recherche est de proposer des moyens de garantir que l'on peut détecter une injection de faute causant la perturbation de la carte à puce. Nous souhaitons que cette détection soit automatique tout en respectant les contraintes de ressources mémoires et processeurs de la carte. Pour y parvenir, nous utilisons une fonctionnalité introduite par Java Card 3 qui est l'annotation de sécurité qui permet au programmeur de marquer les méthodes et classes sensibles de son application. Permettant à la machine virtuelle de passer dans un mode sécurisé lors de leur exécution. L'approche proposée est d'introduire des informations de sécurité dans le code et de modifier la machine virtuelle afin qu'elle les utilise pour détecter les attaques. Ces recherches se sont focalisées sur le développement de nouveaux moyens de lutter contre les attaques par injection en faute en vérifiant en temps réel l'intégrité du code ou celle du flot de contrôleOur goal, is to propose some way to guaranty that we can detect that a fault attack occurs tampering the smart card ship. And we want to do this in an automatic way that is affordable in resources (memory and CPU averhead) for the card. To achieve this goal, we use a functionality introduced by Java Card 3, the security annotations that allow a programmer to choose sensitive methods or classes of his application. Allowing the virtual machine to execute them in a secured mode. The developed approach is to use security information introduce in application code and to modify the java virtual machine to make good use of them to detect the attack. These researches focus on proposing different mechanisms that can help to fight against fault attacks in verifying during runtime the code integrity or the control flow integrity
16
Barbu, Guillaume. "De la sécurité des platesformes JavaCardTM face aux attaques matérielles." Phd thesis, Télécom ParisTech, 2012. http://pastel.archives-ouvertes.fr/pastel-00834324.
Abstract:
Les cartes à puce jouent un rôle crucial dans de nombreuses applications que nous utilisons quotidiennement : paiement par carte bancaire, téléphonie mobile, titres de transport électroniques, etc. C'est dans ce contexte que la technologie Java Card s'est imposée depuis son introduction en 1996, réduisant les coûts de développement et de déploiement d'applications pour cartes à puce et permettant la cohabitation de plusieurs applications au sein d'une même carte. La communauté scientifique a rapidement démontré que la possibilité donnée à un attaquant d'installer des applications sur les cartes représente une menace. Mais dans le même temps, la sécurité des systèmes embarqués a également été un sujet d'étude très productif, révélant que des algorithmes cryptographiques considérés comme sûrs pouvaient être facilement cassés si leurs implémentations ne prenaient pas en compte certaines propriétés physiques des composants électroniques qui les accueillent. En particulier, une partie des attaques publiées repose sur la capacité de l'attaquant à perturber physiquement le composant pendant qu'un calcul est exécuté. Ces attaques par injections de fautes n'ont que très peu été étudiées dans le contexte de la technologie Java Card. Cette thèse étudie et analyse la sécurité des Java Cards contre des attaques combinant injections de fautes et installations d'applications malicieuses. Tout d'abord, nous présentons différents chemins d'attaques combinées et exposons dans quelle mesure ces attaques permettent de casser différents mécanismes sécuritaires de la plateforme. En particulier, notre analyse sécuritaire permet de démontrer que la propriété de sûreté du typage, l'intégrité du flot de contrôle, ainsi que le mécanisme d'isolation des applications peuvent être contournés et exploités par des combinaisons adéquates. Puis, nous présentons différentes approches permettant d'améliorer la résistance de la plateforme Java Card ainsi que des applications qu'elle accueille contre des attaques combinées. Ainsi, nous définissons plusieurs contremesures rendant les attaques exposées ainsi que certaines attaques de l'état de l'art inopérantes, et ce en gardant à l'esprit les fortes contraintes inhérentes au monde des cartes à puce.
17
Dang, Alexandre. "Compilation sécurisée pour la protection de la mémoire." Thesis, Rennes 1, 2019. http://www.theses.fr/2019REN1S111.
Abstract:
Cette thèse porte sur la sécurité des programmes et particulièrement en utilisant la compilation pour parvenir à ses fins. La compilation correspond à la traduction des programmes sources écrits par des humains vers du code machine lisible par nos systèmes. Nous explorons les deux manières possible de faire de la compilation sécurisée : la sécurisation et la préservation. Premièrement, nous avons développé CompCertSFI, un compilateur qui sécurise des modules en les isolant dans des zones mémoires restreintes appelées bac à sable. Ces modules sont ensuite incapables d'accéder à des zones mémoires hors de leur bac à sable, ce qui empêche un module malveillant de corrompre d'autres entités du système. Sur le sujet de la préservation, nous avons défini une notion de Préservation de Flot d'Information qui s'applique aux transformations de programme. Cette propriété, lorsqu'elle est appliquée, permet de s'assurer qu'un programme ne devienne moins sécurité durant sa compilation. Notre propriété de préservation est spécifiquement conçus pour préserver les protections contre les attaques de type canaux cachés. Cette nouvelle catégorie d'attaque utilise des médiums physique comme le temps ou la consommation d'énergie qui ne sont pas pris en compte par les compilateurs actuelsOur society has been growingly dependent on computer systems and this tendency will not slow down in the incoming years. Similarly, interests over cybersecurity have been increasing alongside the possible consequences brought by successful attacks on these systems. This thesis tackles the issue of security of systems and especially focuses on compilation to achieve its goal. Compilation is the process of translating source programs written by humans to machine code readable by our systems. We explore the two possible behaviours of a secure compiler which are enforcement and preservation. First, we have developed CompCertSFI, a compiler which enforces the isolation of modules into closed memory areas called sandboxes. These modules are then unable to access memory regions outside of their sandbox which prevents any malicious module from corrupting other entities of the system. On the topic of security preservation, we defined a notion of Information Flow Preserving transformation to make sure that a program does get less secure during compilation. Our property is designed to preserve security against side-channel attacks. This new category of attacks uses physical mediums such as time or power consumption which are taken into account by current compilers
18
Kamel, Sarah. "Sécurité pour les réseaux sans fil." Electronic Thesis or Diss., Paris, ENST, 2017. http://www.theses.fr/2017ENST0011.
Abstract:
Aujourd’hui, le renforcement de la sécurité des systèmes de communications devient une nécessité, par anticipation du développement des ordinateurs quantiques et des nouvelles attaques qui en découleront. Cette thèse explore deux techniques complémentaires permettant d’assurer la confidentialité des données transmises sur des liens sans-fils. Dans la première partie de ce travail, nous nous intéressons au schéma de cryptographie à clé publique basée sur des réseaux de points, qui représente une des techniques les plus prometteuses pour la cryptographie post-quantique. En particulier, nous considérons le cryptosystème Goldreich-Goldwasser-Halevi (GGH), pour lequel nous proposons un nouveau schéma utilisant les GLD. Dans la seconde partie de ce travail, nous étudions la sécurité des canaux de diffusion multi-utilisateur, ayant accès à des mémoires de caches, en présence d'un espion. Nous considérons deux contraintes de sécurité: la contrainte de sécurité individuelle et la contrainte de sécurité jointe. Nous dérivons des bornes supérieure et inférieure pour le compromis sécurisé capacité-mémoire en considérant différentes distributions de cache. Afin d'obtenir la borne inférieure, nous proposons plusieurs schémas de codage combinant codage wiretap, codage basé sur la superposition et codage piggyback. Nous prouvons qu'il est plus avantageux d'allouer la mémoire de cache aux récepteurs les plus faiblesToday, there is a real need to strengthen the communication security to anticipate the development of quantum computing and the eventual attacks arising from it. This work explores two complementary techniques that provide confidentiality to data transmitted over wireless networks. In the first part, we focus on lattice-based public-key cryptography, which is one of the most promising techniques for the post-quantum cryptography systems. In particular, we focus on the Goldreich-Goldwasser-Halevi (GGH) cryptosystem, for which we propose a new scheme using GLD lattices. In the second part of this work, we study the security of multi-user cache-aided wiretap broadcast channels (BCs) against an external eavesdropper under two secrecy constraints: individual secrecy constraint and joint secrecy constraint. We compute upper and lower bounds on secure capacity-memory tradeoff considering different cache distributions. To obtain the lower bound, we propose different coding schemes that combine wiretap coding, superposition coding and piggyback coding. We prove that allocation of the cache memory to the weaker receivers is the most beneficial cache distribution scenario
19
Sauveron, Damien. "Etude et réalisation d'un environnement d'expérimentation et de modélisation pour la technologie Java Card : application à la sécurité." Bordeaux 1, 2004. http://www.theses.fr/2004BOR12930.
Abstract:
En s'appuyant sur une collaboration menée entre le LaBRI et SERMA Technologies sur la sécurité des Java Cards, cette thèse a pour objectif d'étudier les nouvelles problématiques de sécurité liées à l'apparition de la technologie Java Card. Elle a donné lieu au développement d'un émulateur Java Card capable de simuler des attaques au niveau matériel et logiciel. Elle a également mis en évidence un certain nombre de problèmes dans les spécifications Java Card et des vulnérabilités potentielles dans le cadre de la multi-application sur cartes à puce ouvertes. Par ailleurs, les travaux de cette thèse ont permis de proposer des solutions visant à protéger des codes mobiles pour faire du calcul distribué grâce à l'utilisation de Java Cards. Une application directe de ces travaux permettra de sécuriser le calcul sur la grille.
20
Maréchal, Catherine. "Etude de l'influence de la technologie et de l'association de composants logiques sur la sensibilité électromagnétique de cartes électroniques : Application à l'étude d'une fonction dont la sécurité est fondée sur la redondance matérielle." Lille 1, 1994. http://www.theses.fr/1994LIL10109.
Abstract:
Nous etudions l'influence de la technologie et de l'association des composants logiques sur la sensibilite electromagnetique des cartes electroniques. Dans une premiere partie, nous analysons le comportement d'un dispositif sous test simple vis-a-vis d'une perturbation electromagnetique de mode rayonne. Ce dispositif sous test est constitue de deux portes inverseuses connectees en serie par une ligne de transmission couplee a l'onde electromagnetique. Un outil statistique est developpe afin de caracteriser les defauts statiques qui apparaissent en sortie sur les etats logiques pour des perturbations de forte amplitude. Nous utilisons egalement une methode de mesure visualisant l'excursion du signal perturbe selon l'amplitude du champ electrique. Apres avoir etudie l'association de differentes familles d'une part de la technologie cmos (hc et hcu) et d'autre part de la technologie ttl (ls, als, as, f et s), nous analysons la propagation des perturbations le long d'une chaine de composants logiques. Nous utilisons le logiciel pspice afin de simuler les signaux induits sur la ligne de transmission. Dans une deuxieme partie, nous appliquons nos resultats experimentaux afin de tenter d'ameliorer la securite de systemes redondants soumis a une perturbation electromagnetique. Pour ce faire, nous etudions la sensibilite electromagnetique d'une fonction de securite effectivement implantee sur un systeme de transport. La securite de la carte est fondee sur une redondance materielle: une des voies de traitement de l'information emploi la technologie cmos et l'autre voie la technologie ttl.
21
Hély, David. "Conception en vue du test de circuits sécurisés." Montpellier 2, 2005. http://www.theses.fr/2005MON20123.
22
Bolignano, Pauline. "Formal models and verification of memory management in a hypervisor." Thesis, Rennes 1, 2017. http://www.theses.fr/2017REN1S026/document.
Abstract:
Un hyperviseur est un logiciel qui virtualise les ressources d'une machine physique pour permettre à plusieurs systèmes d'exploitation invités de s'exécuter simultanément dessus. L'hyperviseur étant le gestionnaire des ressources, un bug peut être critique pour les systèmes invités. Dans cette thèse nous nous intéressons aux propriétés d'isolation de la mémoire d'un hyperviseur de type 1, qui virtualise la mémoire en utilisant des Shadow Page Tables. Plus précisément, nous présentons un modèle concret et un modèle abstrait de l'hyperviseur, et nous prouvons formellement que les systèmes d'exploitation invités ne peuvent pas altérer ou accéder aux données privées des autres s'ils n'en ont pas la permission. Nous utilisons le langage et l'assistant de preuve développés par Prove & Run pour ce faire. Le modèle concret comporte beaucoup d'optimisations, qui rendent les structures de données et les algorithmes complexes, il est donc difficile de raisonner dessus. C'est pourquoi nous construisons un modèle abstrait dans lequel il est plus facile de raisonner. Nous prouvons les propriétés sur le modèle abstrait, et nous prouvons formellement sa correspondance avec le modèle concret, de telle manière que les preuves sur le modèle abstrait s'appliquent au modèle concret. La preuve correspondance n'est valable que pour des états concrets qui respectent certaines propriétés, nous prouvons que ces propriétés sont des invariants du système concret. La preuve s'articule donc en trois phases : la preuve d'invariants au niveau concret, la preuve de correspondance entre les modèles abstraits et concret, et la preuve des propriétés de sécurité au niveau abstraitA hypervisor is a software which virtualizes hardware resources, allowing several guest operating systems to run simultaneously on the same machine. Since the hypervisor manages the access to resources, a bug can be critical for the guest Oses. In this thesis, we focus on memory isolation properties of a type 1 hypervisor, which virtualizes memory using Shadow Page Tables. More precisely, we present a low-level and a high-level model of the hypervisor, and we formally prove that guest OSes cannot access or tamper with private data of other guests, unless they have the authorization to do so. We use the language and the proof assistant developed by Prove & Run. There are many optimizations in the low-level model, which makes the data structures and algorithms complexes. It is therefore difficult to reason on such a model. To circumvent this issue, we design an abstract model in which it is easier to reason. We prove properties on the abstract model, and we prove its correspondence with the low-level model, in such a way that properties proved on the abstract model also hold for the low-level model. The correspondence proof is valid only for low-level states which respect some properties. We prove that these properties are invariants of the low-level system. The proof can be divided into three parts : the proof of invariants preservation on the low-level, the proof of correspondence between abstract and low-level models, and proof of the security properties on the abstract level
23
Elbaz, Reouven. "Mécanismes matériels pour des transferts processeur mémoire sécurisés dans les systèmes embarqués." Montpellier 2, 2006. http://www.theses.fr/2006MON20119.
24
Bresch, Cyril. "Approches, Stratégies, et Implémentations de Protections Mémoire dans les Systèmes Embarqués Critiques et Contraints." Thesis, Université Grenoble Alpes, 2020. http://www.theses.fr/2020GRALT043.
Abstract:
Cette thèse traite de la problématique des corruptions de mémoire dans les dispositifs médicaux vitaux. Au cours des dernières années, plusieurs vulnérabilités telles que les exploits de mémoire ont été identifiées dans divers dispositifs connectés de l’Internet des objets médicaux (IoMT). Dans le pire des cas, ces vulnérabilités permettent à un attaquant de forcer à distance une application à exécuter des actions malveillantes. Si de nombreuses contre-mesures contre les exploits logiciels ont été proposées jusqu’à présent, seules quelques-unes d’entre elles semblent convenir aux dispositifs médicaux. En effet, ces dispositifs sont contraints de par leur taille, leurs performances en temps réel et les exigences de sûreté de fonctionnement, ce qui rend l’intégration de la sécurité difficile. Pour répondre à ce problème, la thèse propose deux approches. Toutes deux abordent la question de la sécurité de la mémoire depuis la conception du logiciel jusqu’à son exécution sur le matériel. Une première approche suppose que les défenses peuvent être mises en oeuvre à la fois dans le matériel et dans le logiciel. Cette approche aboutit à TrustFlow, une structure composée d’un compilateur capable de générer un code sécurisé pour un processeur modifié. Ce processeur peut prévenir, détecter, enregistrer et auto-guérir les applications critiques victimes d’une attaque mémoire. La seconde approche considère que le matériel est immuable. Selon cette contrainte, les défenses ne reposent que sur le logiciel. Cette seconde approche aboutit à BackGuard, un compilateur modifié qui renforce efficacement les applications embarquées tout en assurant l’intégrité du flot d’exécutionThis thesis deals with the memory safety issue in life-critical medical devices. Over the last few years, several vulnerabilities such as memory exploits have been identified in various Internet of Medical Things (IoMT) devices. In the worst case, such vulnerabilities allow an attacker to remotely force an application to execute malicious actions. While many countermeasures against software exploits have beenproposed so far, only a few of them seem to be suitable for medical devices. Indeed,these devices are constrained by their size, real-time performances, and safety requirements making the integration of security challenging. To address this issue,the thesis proposes two approaches. Both address the memory safety issue fromthe software design-time to its run-time on the hardware. A first approach assumesthat memory defenses can be implemented both in hardware and software. Thisapproach results in TrustFlow, a framework composed of a compiler able to generatesecure code for an extended processor that can prevent, detect, log, andself-heal critical applications from memory attacks. The second approach considersthat hardware is immutable. Following this constraint, defenses only rely uponsoftware. This second approach results in BackGuard a modified compiler that efficiently hardens embedded applications while ensuring control-flow integrity
25
Jensen, Christian Damsgaard. "Un modèle de contrôle d'accès générique et sa réalisation dans la mémoire virtuelle répartie unique Arias." Phd thesis, Université Joseph Fourier (Grenoble), 1999. http://tel.archives-ouvertes.fr/tel-00004841.
Abstract:
Un système à mémoire virtuelle répartie unique permet l'utilisation des adresses virtuelles comme identificateurs globaux uniques. Il faut donc séparer la résolution des adresses et le contrôle d'accès, parce qu'une adresse virtuelle est potentiellement visible par toute application dans le système. Nous proposons un modèle de contrôle d'accès pour une mémoire virtuelle répartie unique qui se base sur le modèle à capacités cachées. Le modèle se base sur les notions suivantes : la capacité (un droit d'accès simple), le domaine de protection (définit le contexte de protection par l'ensemble des capacités disponibles dans le domaine) et l'appel de changement de domaine (qui permet d'appeler une procédure désignée dans un autre domaine de protection). Deux principes de base sont très importants pour le modèle : l'utilisation des capacités confinées et la délégation contrôlée à travers des interfaces de protection. Les interfaces de protection permettent une séparation entre la spécification de la protection et le code de l'application. L'évaluation de notre modèle indique qu'il permet de réaliser la plupart des modèles de contrôle d'accès existants y compris le modèle mandataire de Bell & LaPadula. Le modèle à capacités cachées a été réalisé dans Arias, une mémoire virtuelle répartie unique conçue et développée au sein du projet SIRAC. Les expériences avec cette réalisation montrent que la séparation entre la spécification de la protection et le code de l'application facilite la réutilisation logicielle et l'évolution de l'application. L'efficacité d'un appel de changement de domaine correspond à celui d'un appel RPC standard.
26
Beringuier-Boher, Noémie. "Evaluation et amélioration de la sécurité des circuits intégrés analogiques." Thesis, Université Grenoble Alpes (ComUE), 2015. http://www.theses.fr/2015GREAT007.
Abstract:
Le nombre d'objets connectés utilisés quotidiennement ne cesse d'augmenter. Ces objets manipulent et stockent toute sorte de données personnelles et confidentielles. La contrainte de la sécurité devient alors importante pour la conception des systèmes sur puce (SoCs) destinés à des applications grand public. Et, dans un contexte de plus en plus exigeant en termes de performances et agressif en termes de coûts d'intégration et de développement, il est important de trouver des solutions de sécurisation des SoCs adaptées. Aussi, bien que la sécurité matérielle soit souvent envisagée d'un point de vue numérique, les SoCs actuels sont la plupart du temps mixtes. Les travaux présentés dans ce manuscrit s'intéressent alors à la sécurisation des circuits analogiques composant ces systèmes mixtes. Pour protéger au mieux un système quel qu'il soit, il est avant tout nécessaire d'en connaitre les vulnérabilités. Pour cela, une méthodologie d'analyse des vulnérabilités dédiée aux circuits analogiques a été développée. Ainsi, les contremesures adéquates peuvent être développées avant que le système ne soit complètement conçu. La sécurité du système est alors améliorée sans augmenter considérablement le temps de conception de celui-ci. L'analyse d'un système analogique largement utilisé dans les SoCs actuels et composé de nombreux sous-circuits a permis d'identifier les attaques en faute par Stimulation Photoélectrique Laser (SPL) , et par variation de la tension d'alimentation, comme présentant un risque important pour le système. Mais, a aussi mis en avant certaines difficultés. En effet, les circuits analogiques, contrairement aux circuits numériques, sont sensibles aux fautes paramétriques. Aussi, les nombreuses interconnections entre les différents sous-circuits rendent l'analyse de la propagation des fautes difficile. Pour cela, des simulations du système au niveau transistors sont nécessaires. Ces simulations étant coûteuses en temps, la modélisation des circuits analogiques pour l'analyse des effets des attaques par variations de la tension d'alimentation a été étudiée. Les modèles développés pour cette analyse doivent respecter différentes contraintes spécifiques. L'application de ces contraintes à la modélisation d'un circuit analogique concret a montré que les modèles pouvaient être utilisés pour identifier les formes d'attaques pouvant compromettre la sécurité du circuit. En revanche, l'étude n'a pas permis de déterminer le temps gagné par l'utilisation de modèles. Après avoir identifié les deux types d'attaques précédents et analysé leurs effets sur les circuits analogiques, la problématique de la protection des circuits a été abordée. Les contremesures existantes ont été comparées et évaluées. Pour les compléter, des circuits analogiques de détection d'attaques laser et d'attaques en tension actives ont été conçus en tenant compte des fortes contraintes de coûts et des différentes problématiques présentes au niveau d'un SoC. Les tests électriques de ces détecteurs en technologie CMOS 28nm FD-SOI ont prouvé leur efficacité. Finalement, ce travail présente les différentes étapes de la sécurisation d'un circuit analogique, de l'analyse des vulnérabilités à la conception de contremesures, en passant par la modélisation des attaques et de leurs effets, dans le contexte d'applications mixtes et à bas coûtWith the development of the Internet of things, the number of connected devices is in constant increase. These objects use a large amount of data including personal credentials. Therefore, security has become a major constraint for System on Chips (SoCs) designers. Moreover, in a context more and more aggressive in terms of performances and time to market, it is important to find low cost security solutions. Although the hardware security is often treated from a digital point of view, almost every SoCs is also using analog and mixed IP. Thus, this work presents different steps to improve the security of analog IPs, from vulnerability analysis to countermeasures design validation, and behavioral modeling in the context of mixed signals and low cost applications. To protect any system, the first requirement is to know its vulnerabilities. To do so, a vulnerability analysis methodology dedicated to analog circuit has been developed. Using the results of this analysis, countermeasures can be designed during the development of the circuit and not at the end. The circuit security is thus improved without dramatically increasing its cost in terms of design time. The analysis of a clock system generator, an analog IP widely used in current SoCs and composed with various sub-circuits, has shown fault attacks using Laser Photoelectric Stimulation (LPS) or supply voltage glitches as important threats. After having identified the 2 previous attacks types as major threats, their effects on analog circuits are analyzed. Existing countermeasures are then compared and evaluated for the protection of analog IPs. To complete these solutions, two analog detectors have been designed to detect laser and supply voltage glitch attacks considering SoCs level constraints. Electrical test of these detectors processed on CMOS 28nm FD-SOI technology proved their efficiency. Theoretical vulnerability analysis has shown some difficulties. Indeed, analog circuits are sensitive to numerous parametrical faults. Also, the high interconnection of various sub-circuits makes the faults propagation analysis quite difficult. To help this analysis, electrical simulations at transistor level are necessary. These simulations are quite long and, so the behavioral modeling of analog circuits to help the analysis of supply voltage glitch attack effects has been studied. To do so, the developed models must be developed according different constraints presented in this report and applied to the behavioral modeling of a real analog circuit. This illustration proved that behavioral models can be used to help to identify which attack shapes are the most likely to induce faults in the circuit
27
Pagani, Fabio. "Advances in memory forensics." Electronic Thesis or Diss., Sorbonne université, 2019. http://www.theses.fr/2019SORUS299.
Abstract:
L'adoption de la memory forensics - l'art d'extraire artefacts de la mémoire volatile d'un système compromis - est propagation dans les enquêtes de cybersécurité. De cette façon, les analystes en memory forensics peuvent gagner la grande image sur un comportement malveillant. Néanmoins, memory forensics a moins de deux décennies: de nombreux défis sont non résolus. Cette thèse donne une nouvelle perspective sur trois de ces problèmes. La première contribution étudie les effets non atomiques méthodes d'acquisition. La cause première de ce problème est que pendant la mémoire est acquise, l'utilisateur et les processus du noyau sont en cours d’exécution et modifient donc le contenu de la mémoire. Pour cette raison, la mémoire résultante le vidage ne représente pas l'état de la mémoire en un point donné dans le temps, mais plutôt un mélange de plusieurs points. La deuxième contribution se concentre sur l'extraction automatique d'un profil de forensics à partir d'un vidage de la mémoire. Avoir un profil valide est une exigence forte pour l'analyse de la mémoire, car sans aucun technique de forensics de la mémoire structurée peut être appliquée. Donc, ce problème empêche efficacement l'application de l'investigation judiciaire sur la mémoire dans les scénarios où la création d'un profil est plus difficile. La troisième et dernière contribution de cette thèse vise à changer la manière dont les règles de forensics, mieux connues sous le nom de plugins, sont créées. De nos jours, ces règles sont écrites manuellement par le noyau experts et praticiens de memory forensics. Malheureusement, cette approche n’a aucune garantie sur la qualité ni sur le l'unicité de ces règlesThe adoption of memory forensics - the art of extracting artifacts from the volatile memory of a compromised system - is spreading in cyber-security investigations. The main reason of this enthusiasm comes from the fact that many artifacts can not be found elsewhere. In this way, the forensics analysts can gain the big picture over a malicious behavior. Nevertheless, memory forensics is less than two decades old: many challenges are unsolved and many questions are unanswered. This thesis gives a new perspective over three of these problems. The first contribution studies the effects non-atomic acquisition methods. The root cause of this problem is quite straightforward to explain: while the memory is acquired, user and kernel processes are running and therefore modifying the content of the memory. For this reason, the resulting memory dump does not represent the state of the memory in a given point in time, but rather a mix of multiple points. The second contribution focus on automatically extracting a forensics profile from a memory dump. Having a valid profile is a strong requirement for memory analysis because without one any structured memory forensics technique can be applied. Therefore, this problem effectively prevents memory forensics to be applied in those scenarios where creating a profile is harder -- if not impossible. The third and last contribution of this thesis aims to change how forensics rules, better known as plugins, are created. Nowadays, these rules are manually written by kernel experts and forensics practitioners. Unfortunately, this manual approach does not have any guarantee on the quality or on the uniqueness of these rules
28
Coisel, Iwen. "Authentification et Anonymat à Bas-coût : Modélisations et Protocoles." Caen, 2009. http://www.theses.fr/2009CAEN2041.
Abstract:
Dans la vie de tous les jours, la sécurité de nombreuses applications est assurée par des mécanismes cryptographiques. Dans certains cas, le respect de la vie privée revêt une importance majeure. Par exemple, sur internet, un utilisateur attend du fournisseur de services que celui-ci ne divulgue pas son identité. Dans ce mémoire, je donne tout d'abord une définition formelle des preuves de connaissance à divulgation nulle de connaissance (ZKPK), très utiles pour concevoir des signatures numériques. Je prouve la sécurité d'une construction générique fournissant des preuves de connaissance d'un ensemble de relations de logarithmes discrets. Puis je présente l'état de l'art des différents schémas de signature assurant l'anonymat de l'utilisateur. J'en donne ensuite une version coopérative, dans laquelle un intermédiaire aide l'utilisateur à réaliser certains calculs au cours du protocole. Je définis également un modèle formel de sécurité tenant compte de la potentielle corruption de l'intermédiaire tout en améliorant l'efficacité du protocole. Dans la deuxième partie de ce mémoire, je présente les propriétés de sécurité requises d'un schéma d'authentification d'étiquettes RFID. Comme ces dispositifs sont susceptibles d'être intégrés dans différents produits, il faut qu'ils soient intraçables afin d'empêcher leur porteur d'être pisté. Cette propriété n'est pas assurée par l'anonymat seul et doit donc apparaître dans le modèle de sécurité. Enfin, je décris deux protocoles d'authentification. Le premier utilise une infrastructure à clé secrète et un mécanisme de mise à jour de clé. Le second utilise une infrastructure à clé publique et un algorithme de chiffrementIn our daily life, security of many applications are based on cryptographic mechanisms. In some of them, privacy issues are a major concern. For example in internet context, a user expects the service provider not to divulgate his identity. In this thesis, I first give a formal definition of zero-knowledge proofs of knowledge (ZKPK), very useful for designing digital signatures. I prove the security of a generic construction of proofs of knowledge of discrete logarithm relations set. Then, I present state of the art of different signature schemes ensuring users' anonymity. Afterwards I adapt these protocols to the cooperative set-up, in which an intermediary helps the user perform some computations during the protocol. I also define a formal security model which is robust against corruption of the intermediary, while improving protocol efficiency. In the second part of this thesis, I present the security requirements for RFID tags authentication protocols. As these small embedded devices are potentially integrated into many various products, they must be intraceable so that nobody can trace their holder. As anonymity does not provide this property on its own, it must be included in the security model. Finally, I describe two authentication protocols which provide this security level. The first one uses a secret key infrastructure and a key update mechanism. The other one uses a public key infrastructure and an encryption algorithm
29
Vaquié, Bruno. "Contributions à la sécurité des circuits intégrés face aux attaques par canaux auxiliaires." Thesis, Montpellier 2, 2012. http://www.theses.fr/2012MON20133/document.
Abstract:
Les attaques par canaux cachés telles que les attaques par analyse de la consommation sont une menace pour la sécurité des circuits intégrés. Elles exploitent les fuites physiques émises par les circuits lors des calculs cryptographiques pour récupérer les informations secrètes qu'ils contiennent. De nombreuses contremesures, notamment matérielles, ont donc été proposées par la communauté dans le but de protéger les crypto-systèmes contre ce type d'attaques. Malgré leur efficacité, leur inconvénient majeur est leur surcoût important en surface, vitesse et consommation. Cette thèse a pour objectif de proposer des contremesures avec un faible coût au niveau matériel visant à réduire ces fuites et offrant un bon compromis entre sécurité et surcoûts. Pour cela, nous identifions tout d'abord les principales sources de fuites d'un crypto-système intégrant une architecture matérielle itérative d'un algorithme symétrique. Puis nous proposons plusieurs contremesures, à faible coût matériel, qui visent à réduire ces fuites. Enfin, nous évaluerons la robustesse de nos solutions face aux attaques par canaux cachésSide channel attacks such as power analysis attacks are a threat to the security of integrated circuits.They exploit the physical leakage of circuits during the cryptographic computations to retrieve the secret informations they contain. Many countermeasures, including hardware, have been proposed by the community in order to protect cryptosystems against such attacks. Despite their effectiveness, their major drawback is their significant additional cost in area, speed and consumption. This thesis aims at proposing low cost countermeasures able to reduce the leaks and offering a good compromise between security and costs. First we identify the main sources of leakage of a cryptographic system that integrates an iterative hardware architecture of a symetric algorithm. Then we propose several low cost countermeasures, which aim at reducing this leakage. Finally, we evaluate the robustness of our solutions against side channel attacks
30
Vandewalle, Jean-Jacques. "Projet OSMOSE : modélisation et implémentation pour l'interopérabilité de services carte à microprocesseur par l'approche orientée objet." Lille 1, 1997. http://www.theses.fr/1997LIL10233.
Abstract:
Jusqu'a aujourd'hui, les cartes a puce ont ete utilisees comme des elements informatiques dedies. Leur systeme d'exploitation et leurs fonctions applicatives sont developpes sur mesure. Il en resulte des temps de developpement trop long, des difficultes a tirer benefice de l'existant et l'incapacite d'integrer facilement les cartes dans les systemes d'information. Pour traiter ces problemes, nous proposons, dans le cadre du projet osmose (operating system and mobile services), de concevoir la carte comme une machine generique servant de support pour des services pouvant etre charges tout le long de son cycle de vie. Nous presentons un modele global de systeme a cartes generiques base sur une definition objet des services carte. Ce modele a ete valide par trois developpements formant un ensemble coherent: 1. Une architecture de securite a base de certificats permet d'authentifier et de controler les droits d'acces des createurs et utilisateurs des services carte. Les certificats sont delivres aux utilisateurs de facon off-line et sont verifies par la carte on-line. Un protocole de securite a base de cryptographie asymetrique permet de verifier la validite des certificats. 2. Un systeme d'exploitation carte appele combo fournit un environnement d'execution securise par l'interpretation des programmes charges dans la carte. La machine virtuelle sous-jacente assure une independance totale entre les services en garantissant le respect de la propriete d'encapsulation des objets executes. 3. Une couche middleware d'interoperabilite permet de dynamiquement adapter un serveur generique d'acces aux services carte depuis des applications clientes developpees dans une architecture corba (common object request broker architecture). Le serveur generique appele coa (card object adapter) fournit une passerelle transparente de transport des requetes carte grace a la decouverte des interfaces des services au moment de l'execution.
31
Ouaarab, Salaheddine. "Protection du contenu des mémoires externes dans les systèmes embarqués, aspect matériel." Thesis, Paris, ENST, 2016. http://www.theses.fr/2016ENST0046/document.
Abstract:
Ces dernières années, les systèmes informatiques (Cloud Computing, systèmes embarqués, etc.) sont devenus omniprésents. La plupart de ces systèmes utilisent des espaces de stockage (flash,RAM, etc.) non fiables ou non dignes de confiance pour stocker du code ou des données. La confidentialité et l’intégrité de ces données peuvent être menacées par des attaques matérielles (espionnage de bus de communication entre le composant de calcul et le composant de stockage) ou logicielles. Ces attaques peuvent ainsi révéler des informations sensibles à l’adversaire ou perturber le bon fonctionnement du système. Dans cette thèse, nous nous sommes focalisés, dans le contexte des systèmes embarqués, sur les attaques menaçant la confidentialité et l’intégrité des données qui transitent sur le bus de communication avec la mémoire ou qui sont stockées dans celle-ci.Plusieurs primitives de protection de confidentialité et d’intégrité ont déjà été proposées dans la littérature, et notamment les arbres de Merkle, une structure de données protégeant efficacement l’intégrité des données notamment contre les attaques par rejeu. Malheureusement,ces arbres ont un impact important sur les performances et sur l’empreinte mémoire du système.Dans cette thèse, nous proposons une solution basée sur des variantes d’arbres de Merkle (arbres creux) et un mécanisme de gestion adapté du cache afin de réduire grandement l’impact de la vérification d’intégrité d’un espace de stockage non fiable. Les performances de cette solution ont été évaluées théoriquement et à l’aide de simulations. De plus, une preuve est donnée de l’équivalence, du point de vue de la sécurité, avec les arbres de Merkle classiques.Enfin, cette solution a été implémentée dans le projet SecBus, une architecture matérielle et logicielle ayant pour objectif de garantir la confidentialité et l’intégrité du contenu des mémoires externes d’un système à base de microprocesseurs. Un prototype de cette architecture a été réalisé et les résultats de l’évaluation de ce dernier sont donnésDuring the past few years, computer systems (Cloud Computing, embedded systems...) have become ubiquitous. Most of these systems use unreliable or untrusted storage (flash, RAM...)to store code or data. The confidentiality and integrity of these data can be threaten by hardware (spying on the communication bus between the processing component and the storage component) or software attacks. These attacks can disclose sensitive information to the adversary or disturb the behavior of the system. In this thesis, in the context of embedded systems, we focused on the attacks that threaten the confidentiality and integrity of data that are transmittedover the memory bus or that are stored inside the memory. Several primitives used to protect the confidentiality and integrity of data have been proposed in the literature, including Merkle trees, a data structure that can protect the integrity of data including against replay attacks. However, these trees have a large impact on the performances and the memory footprint of the system. In this thesis, we propose a solution based on variants of Merkle trees (hollow trees) and a modified cache management mechanism to greatly reduce the impact of the verification of the integrity. The performances of this solution have been evaluated both theoretically and in practice using simulations. In addition, a proof a security equivalence with regular Merkle treesis given. Finally, this solution has been implemented in the SecBus architecture which aims at protecting the integrity and confidentiality of the content of external memories in an embedded system. A prototype of this architecture has been developed and the results of its evaluation are given
32
Atallah, Eve. "Une solution pour l'établissement non planifié de groupes sécurisés permettant des communications sûres dans les réseaux MANets purs." Limoges, 2008. https://aurore.unilim.fr/theses/nxfile/default/dc02beb3-c3d0-4717-8d6f-6a3706b2da76/blobholder:0/2008LIMO4060.pdf.
Abstract:
Le travail présenté dans cette thèse porte sur les réseaux MANets sans centralisation ni administration dans lesquels les utilisateurs sont mobiles et non nécessairement liés entre eux par une organisation humaine. Notre contribution consiste en une architecture totalement décentralisée permettant de sécuriser les échanges au sein de tels réseaux. Sa concrétisation, l'application SManet, repose sur un module administrateur embarqué sur carte à puce chargé de tâches habituellement réalisées par une entité centralisée. Chaque dispositif utilisateur possède une carte équipée de ce module qui procède à toutes les opérations de contrôle assurant le bon comportement de son hôte et la sécurité des communications avec les autres possesseurs d'une carte. Cette solution permet de mettre en place des échanges sûrs, n'importe où, n'importe quand, sans aucune planification et donc sans aucune oraganisation humaine préalable sous-jacenteThe work presented in this thesis is about MANets with no centralization or administration and where users are highly mobile and not necessarily linked together within a human organization. Our contribution is a decentralized architecture that makes it possible to secure communication within such networks. Its implementation, the SManet application, is based on an administrator module embedded in a mart card which is in charge of the tasks usually carried out by a centralized entity. Each mobile treminal is equipped with a card embedding such a module that controls the operations ensuring the correct behavior of its host and the security of the communications with the other card holders. This solution supports the establishment of secure exchanges, anywhere, anytime, with no planning and thus without any prior underlying human organization
33
Karray, Achraf. "Conception, mise en œuvre et validation d’un environnement logiciel pour le calcul sécurisé sur une grille de cartes à puce de type Java." Thesis, Bordeaux 1, 2008. http://www.theses.fr/2008BOR13724/document.
Abstract:
Le calcul sur grille permet à un individu, une société, de disposer d’un ensemble d’unités de calcul fournies par des tiers. Dans ce type d’architecture, des problèmes de sécurité se posent : comment garantir à la fois la sécurité du matériel et de l’application. Pour ce qui concerne la sécurité de l’application, il s’agit principalement d’assurer la confidentialité du code et l’intégrité de son exécution. La sécurité du matériel consiste à protéger la machine contre tout code malveillant pouvant être contenu dans l’application. Aucun système ne permet aujourd’hui, de satisfaire ces contraintes fortes de sécurité. Notre objectif dans cette thèse est de proposer et de valider des solutions pour les problèmes de sécurité des grilles informatiques.Pour résoudre ces problèmes, nous proposons l’utilisation de la carte à puce comme support d’exécution hautement sécurisé à travers le déploiement de grilles de cartes à puce. Grâce aux mécanismes de sécurité qu’elles intègrent, les cartes à puce permettent en effet de protéger l’application et son code aussi bien que le support d’exécution. Le travail effectué dans cette thèse consiste à définir un environnement pour le calcul sécurisé sur grille de cartes à puceAbstract
34
Kussener-Combier, Edith. "Conception de circuits intégrés de régulation intelligente pour les microprocesseurs sécurisés (carte à puce)." Lille 1, 2002. https://pepite-depot.univ-lille.fr/RESTREINT/Th_Num/2002/50376-2002-117.pdf.
Abstract:
Les technologies utilisées pour la conception des cartes à puce migrent rapidement vers les procédés technologiques CMOS submicroniques les plus récents. Alors que pour les lecteurs de ces cartes cette migration est beaucoup plus lente. Pour ces technologies, la réduction constante des épaisseurs d'oxyde de grille contraint à adapter en interne la tension d'alimentation des cartes à puce avec celle fournie par les lecteurs. Cette adaptation doit se traduire par une conversion et une régulation de tension stable quelque soit les variations internes et externes. Dans le cadre de cette thèse, l'analyse des principales topologies de conversion statique a permis la conception de deux convertisseurs dédiés à l'alimentation de cartes à puce à microprocesseur de chez STM. Le premier convertisseur proposé est un convertisseur linéaire classique, utilisant une nouvelle référence de tension programmable. Le second convertisseur est un convertisseur linéaire intégrant un circuit additionnel, agissant par autorégulation sur la tension de grille du transistor de puissance en sortieCe circuit additionnel permet en particulier de réaliser une conversion et une régulation de tension de gain unitaire. La phase de conception de ces convertisseurs nécessite une interprétation correcte des résultats de simulation. Dans ce sens, vue de l'alimentation, une macro modélisation de l'activité du microprocesseur est nécessaire. Une macro modélisation basée sur la simulation et la programmation de plusieurs inverseurs logiques est proposée. Les mesures effectuées sur plusieurs prototypes confirment bien l'interprétation théorique proposée ainsi que les résultats attendus à partir des simulations. Différentes solutions permettent de crypter les informations confidentielles qui circulent aux travers des plots d'alimentations des cartes à puces. Les solutions proposées consistent à ajouter des blocs sécuritaires élémentaires pouvant être pilotés par le microprocesseur via des algorithmes de cryptage
35
Bozzio, Mathieu. "Security and implementation of advanced quantum cryptography : quantum money and quantum weak coin flipping." Electronic Thesis or Diss., Université Paris-Saclay (ComUE), 2019. http://www.theses.fr/2019SACLT045.
Abstract:
Les lois de la mécanique quantique présentent un fort potentiel d’amélioration pour la sécurité des réseaux de communication, du cryptage à clé publique au vote électronique, en passant par la banque en ligne. Cette thèse porte sur la sécurité pratique et l’implémentation de deux tâches cryptographiques quantiques : la monnaie quantique et le tirage à pile-ou-face faible. La monnaie quantique exploite le théorème de non-clonage quantique pour générer des jetons, billets ou cartes de crédit strictement infalsifiables. Nous réalisons la première démonstration expérimentale de cette fonctionnalité sur une plateforme photonique aux longueurs d’onde télécom. Nous développons ensuite une analyse de sécurité pratique pour les cartes de crédit quantique. La banque peut ainsi vérifier l’authenticité de la carte à distance, même en présence d’un terminal de paiement malhonnête. Enfin, nous proposons une expérience permettant le stockage sécurisé d’une carte de crédit quantique en utilisant la transparence électromagnétiquement induite au sein d’un nuage d’atomes refroidis. Le tirage à pile-ou-face faible est une primitive cryptographique fondamentale: elle permet en effet la construction de tâches plus complexes telles que la mise en gage de bit et le calcul multipartite sécurisé. Lors d’un tirage à pile ou face, deux entités distantes et méfiantes jettent une pièce. Grâce à l’intrication quantique, il est possible de limiter la probabilité que l’entité malhonnête biaise la pièce. Dans ce projet, nous proposons la première implémentation du pile-ou-face faible. Celle-ci requiert un photon unique et une plateforme d’optique linéaire. Nous présentons l’analyse de sécurité en présence d’erreurs et de pertes, et démontrons que le protocole est réalisable à l’échelle d’une ville. Enfin, nous proposons de réduire davantage la probabilité du biais du protocoleHarnessing the laws of quantum theory can drastically boost the security of modern communication networks, from public key encryption to electronic voting and online banking. In this thesis, we bridge the gap between theory and experiment regarding two quantum-cryptographic tasks: quantum money and quantum weak coin flipping. Quantum money exploits the no-cloning property of quantum physics to generate unforgeable tokens, banknotes, and credit cards. We provide the first proof-of-principle implementation of this task, using photonic systems at telecom wavelengths. We then develop a practical security proof for quantum credit card schemes, in which the bank can remotely verify a card even in the presence of a malicious payment terminal. We finally propose a setup for secure quantum storage of the credit card, using electromagnetically-induced transparency in a cloud of cold cesium atoms. Quantum weak coin flipping is a fundamental cryptographic primitive, which helps construct more complex tasks such as bit commitment and multiparty computation. It allows two distant parties to flip a coin when they both desire opposite outcomes. Using quantum entanglement then prevents any party from biasing the outcome of the flip beyond a certain probability. We propose the first implementation for quantum weak coin flipping, which requires a single photon and linear optics only. We provide the complete security analysis in the presence of noise and losses, and show that the protocol is implementable on the scale of a small city with current technology. We finally propose a linear-optical extension of the protocol to lower the coin bias
36
Ouaarab, Salaheddine. "Protection du contenu des mémoires externes dans les systèmes embarqués, aspect matériel." Electronic Thesis or Diss., Paris, ENST, 2016. http://www.theses.fr/2016ENST0046.
Abstract:
Ces dernières années, les systèmes informatiques (Cloud Computing, systèmes embarqués, etc.) sont devenus omniprésents. La plupart de ces systèmes utilisent des espaces de stockage (flash,RAM, etc.) non fiables ou non dignes de confiance pour stocker du code ou des données. La confidentialité et l’intégrité de ces données peuvent être menacées par des attaques matérielles (espionnage de bus de communication entre le composant de calcul et le composant de stockage) ou logicielles. Ces attaques peuvent ainsi révéler des informations sensibles à l’adversaire ou perturber le bon fonctionnement du système. Dans cette thèse, nous nous sommes focalisés, dans le contexte des systèmes embarqués, sur les attaques menaçant la confidentialité et l’intégrité des données qui transitent sur le bus de communication avec la mémoire ou qui sont stockées dans celle-ci.Plusieurs primitives de protection de confidentialité et d’intégrité ont déjà été proposées dans la littérature, et notamment les arbres de Merkle, une structure de données protégeant efficacement l’intégrité des données notamment contre les attaques par rejeu. Malheureusement,ces arbres ont un impact important sur les performances et sur l’empreinte mémoire du système.Dans cette thèse, nous proposons une solution basée sur des variantes d’arbres de Merkle (arbres creux) et un mécanisme de gestion adapté du cache afin de réduire grandement l’impact de la vérification d’intégrité d’un espace de stockage non fiable. Les performances de cette solution ont été évaluées théoriquement et à l’aide de simulations. De plus, une preuve est donnée de l’équivalence, du point de vue de la sécurité, avec les arbres de Merkle classiques.Enfin, cette solution a été implémentée dans le projet SecBus, une architecture matérielle et logicielle ayant pour objectif de garantir la confidentialité et l’intégrité du contenu des mémoires externes d’un système à base de microprocesseurs. Un prototype de cette architecture a été réalisé et les résultats de l’évaluation de ce dernier sont donnésDuring the past few years, computer systems (Cloud Computing, embedded systems...) have become ubiquitous. Most of these systems use unreliable or untrusted storage (flash, RAM...)to store code or data. The confidentiality and integrity of these data can be threaten by hardware (spying on the communication bus between the processing component and the storage component) or software attacks. These attacks can disclose sensitive information to the adversary or disturb the behavior of the system. In this thesis, in the context of embedded systems, we focused on the attacks that threaten the confidentiality and integrity of data that are transmittedover the memory bus or that are stored inside the memory. Several primitives used to protect the confidentiality and integrity of data have been proposed in the literature, including Merkle trees, a data structure that can protect the integrity of data including against replay attacks. However, these trees have a large impact on the performances and the memory footprint of the system. In this thesis, we propose a solution based on variants of Merkle trees (hollow trees) and a modified cache management mechanism to greatly reduce the impact of the verification of the integrity. The performances of this solution have been evaluated both theoretically and in practice using simulations. In addition, a proof a security equivalence with regular Merkle treesis given. Finally, this solution has been implemented in the SecBus architecture which aims at protecting the integrity and confidentiality of the content of external memories in an embedded system. A prototype of this architecture has been developed and the results of its evaluation are given
37
Lacharme, Patrick. "Générateur vraiment aléatoire dans un composant sécurisé." Toulon, 2007. http://www.theses.fr/2007TOUL0025.
Abstract:
Les systèmes de sécurité basés sur des algorithmes cryptographiques font un usage important de suites de bits aléatoires. Les générateurs aléatoires, comme tous les composants présents dans une carte à puce, ont toutefois l'obligation d'avoir des tailles très réduites sans pour autant contenir des failles de sécurité. L'objectif principal do cette thèse est de proposer une alternative moins coûteuse aux générateurs aléatoires existant, afin d'être facilement implantés clans de petits composants. Les axes de recherche sont la construction d'une architecture générale permettant d'étudier le fonctionnnement du générateur en cas de perturbations extérieures, l'analyse très précise du correcteur mathématique utilisé pour estimer la qualité de la sortie et les problèmes d'implêmentationSystems of security based on cryptographic algorithm; use a lot of random HP-quences. For smart card applications, a random generator must to have a small size, without fails in its security. The main objective of this thesis is to propose an alternative to classical generators, in order to be inplemented on small components. The differonts parts of this work are the construction of an architecture for a random generator for small size components, the analysis and the inplementation of the mathematical corrector for an estimation of the quality of the. Output random sequence
38
Oliveri, Andrea. "A Zero-Knowledge Approach to Memory Forensics." Electronic Thesis or Diss., Sorbonne université, 2023. http://www.theses.fr/2023SORUS312.
Abstract:
L'essor rapide des appareils embarqués et des objets IoT entraîne une multiplication des systèmes d'exploitation et des architectures de processeurs, qui ne sont généralement pas pris en charge par les outils forensiques actuels et nécessitent un effort considérable pour être adaptés. Pour surmonter ce problème, nous introduisons, le concept d’analyse forensique de la mémoire à connaissance nulle : réaliser une analyse forensique de la mémoire sans aucune connaissance du système d’exploitation sous-jacent. En supposant que nous ayons effectué un dump mémoire du système d’exploitation inconnu, en utilisant uniquement les informations dérivées de la configuration matérielle de la machine, nous affirmons qu’il est possible de reconstruire l’espace d’adressage du noyau de manière indépendante du système d’exploitation. À partir de ceux-ci, il est possible de reconstruire les structures de données du noyau en mémoire en utilisant uniquement leur topologieThe rapid increase of embedded devices and IoT objects is leading to a multiplication of operating systems and processor architectures, which are generally not supported by current forensic tools and require considerable effort to adapt. To overcome this problem, we introduce the concept of zero-knowledge memory forensics: performing a memory forensic analysis without any knowledge of the underlying operating system. Assuming that we have performed a memory dump of the unknown operating system, using only information derived from the machine's hardware configuration, we claim that it is possible to reconstruct the kernel address space independently of the operating system. From these, it is possible to reconstruct kernel data structures in memory using only their topology
39
Harrari, Mounia. "Hybridation CMOS/STT-MRAM des circuits intégrés pour la sécurité matérielle de l'Internet des Objets." Electronic Thesis or Diss., Aix-Marseille, 2019. http://www.theses.fr/2019AIXM0621.
Abstract:
Cette dernière décennie a été le théâtre du développement rapide de l'Internet des Objets. Celui-ci a renforcé les besoins et contraintes des circuits intégrés : une consommation faible et une surface silicium maîtrisée. Toutefois, cet engouement récent pour les objets connectés pousse souvent les fabricants à précipiter la mise sur le marché de leurs produits, parfois au détriment de la sécurité. Dans le cadre des travaux entrepris lors de cette thèse, nous nous sommes principalement intéressés aux atouts et inconvénients que peut apporter l’hybridation de la technologie CMOS avec la technologie mémoire non-volatile émergente STT-MRAM. Ces architectures innovantes doivent permettre le développement d’applications faible consommation visant la sécurité des objets connectés. Pour cela, la conception d’un algorithme de cryptographie légère hybride CMOS/STT-MRAM basé sur le chiffrement PRESENT a été réalisée. C’est pourquoi la première étude menée a consisté à étudier la robustesse de jonctions mémoires STT-MRAMs unitaires face aux attaques physiques de type perturbation, avant leur intégration dans le chiffrement. Pour ce faire, des injections de fautes Laser ont été effectuées afin d’évaluer l’intégrité des données qui y sont stockées. Suite aux observations des expérimentations réalisées sur ces mémoires de type STT-MRAM perpendiculaires, un nouveau capteur d’attaques physiques basé sur cette technologie mémoire a été proposé, le DDHP. Ce détecteur permet la détection simultanée d’attaques photoélectriques et d’attaques thermiques qui peuvent viser les circuits intégrésIn the last decade, the Internet of Things deployment highlighted new needs and constraints in terms of consumption and area for integrated circuits. However, the recent craze for connected objects and due to the extremely pressing time-to-market demand, the manufacturers commercialize their products, sometimes at the expense of their security. The main focus of the work undertook during this thesis consists in the hybridization of the CMOS technology with the emerging non-volatile memory technology STT-MRAM. This study aims to determine the assets and drawbacks of this hybridization. These innovating architectures must allow the development of low power applications and support the growth of secured connected objects. Thus, the design of a hybrid CMOS/STT-MRAM lightweight cryptographic algorithm based on the PRESENT cipher is realised.This is how the first study carried out consisted in investigating the robustness of STT-MRAM junctions facing physical attacks, before their integration in the cryptographic algorithm. To do this, laser fault injections were performed in order to evaluate the integrity of the sensitive data stored in the cells.Following the observations carried out on these experiments on perpendicular STT-MRAM memories, a new physical attack detector based on this memory technology is proposed, designated by DDHP. This sensor allows simultaneous detection of photoelectrical and thermal attacks that can target integrated circuits
40
Rammal, Darine. "Memory safety for synchronous reactive programming." Electronic Thesis or Diss., Orléans, 2024. http://www.theses.fr/2024ORLE1002.
Abstract:
Les langages réactifs synchrones constituent un excellent choix pour la programmation de l'IoT en raison de leur sémantique claire pour l'interaction entre le système et l'environnement. Cependant, en ce qui concerne les systèmes critiques en termes de sécurité ou contraints en ressources, des propositions récentes telles que Fairthreads ou ReactiveML font face à un problème bien connu. La gestion manuelle de la mémoire de Fairthreads peut entraîner des erreurs, tandis que la collecte des déchets de ReactiveML assure la sécurité de la mémoire mais introduit une surcharge d'exécution. Cette thèse vise à résoudre le problème de la sécurité de la mémoire en développant un langage de programmation réactif spécifiquement conçu pour les systèmes en temps réel, intégrant des threads coopératifs et une exécution synchrone. En nous appuyant sur le solide système de types du langage de programmation Rust, nous proposons un système de types similaire à Rust pour un langage de programmation réactif de noyau appelé MSSL. MSSL offre un modèle de threads coopératifs et facilite le partage de données mutables entre les threads tout en préservant la sécurité des types et des emprunts. Pour y parvenir, nous introduisons une nouvelle abstraction appelée Trc (Thread Reference Counting), qui combine la sécurité de propriété des références de Rust avec le mécanisme de comptage de références des pointeurs intelligents de Rust. Nous présentons ensuite la sémantique et le système de types de MSSL pour démontrer ses capacités à maintenir la sécurité des types, la sécurité des emprunts et la sécurité de la concurrence. De plus, nous étendons MSSL en introduisant des extensions réactives, en intégrant le concept de signaux qui offrent des moyens de communication puissants, flexibles et fiables. Enfin, nous fournissons une implémentation en Java de l'ensemble complet de MSSL, en basant sur la sémantique et les règles de typage de son système de typesSynchronous Reactive Languages are an excellent choice for IoT programming due to their clear system-environment interaction semantics. However, when it comes to safety- critial or resource-constrained systems, recent proposals like Fairthreads or ReactiveML face a well-known issue. Fairthreads' manual memory management can lead to errors, while ReactiveML's garbage collection ensures memory safety but introduces execution overhead. This thesis aims to address the memory safety issue by developing a reactive programming language specifically designed for real-time systems, incorporating cooperative threads and synchronous execution. Drawing from the robust type system of the Rust programming language, we propose a Rust-like type system for a kernel reactive programming language named MSSL. MSSL features a cooperative threading model and facilitates mutable data sharing between threads while preserving type and borrowing safety. To achieve this, we introduce a novel abstraction called Trc (Thread Reference Counting), which combines the ownership safety of Rust references with the reference counting mechanism of Rust smart pointers. Then, we present the semantics and type system of MSSL to demonstrate its capabilities in maintaining type safety, borrowing safety, and concurrency safety. Furthermore, we extend MSSL by introducing reactive extensions, incorporating the concept of signals that offer powerful, flexible, and reliable means of communication. Finally, we provide a Java implementation of the complete MSSL set, based on the semantic and typing rules of its type system
41
Benzine, Mehdi. "Combinaison sécurisée des données publiques et sensibles dans les bases de données." Versailles-St Quentin en Yvelines, 2010. http://www.theses.fr/2010VERS0024.
Abstract:
La protection des données sensibles est une problématique majeure dans le monde des bases de données. Plusieurs solutions logicielles et matérielles ont été proposées pour assurer une sécurité optimale lors du stockage et de la manipulation de ces données. Il est également nécessaire de sécuriser les opérations mettant en relation des données sensibles avec des données publiques. Pour cala, nous avons mis en place une architecture de stockage et d'interrogation offrant cette sécurité. Cette architecture est composée d'un serveur central regroupant les données publiques et d'un serveur sécurisé stockant les données privées. Ce serveur sécurisé est constitué (i) d'un microcontrôleur sécurisé associé à (ii) une mémoire persistante, de grande capacité, de type Flash NAND. Les requêtes mêlant données publiques et sensibles sont scinder en deux sous-requêtes, l'une portant sur les données publiques, l'autre sur les données sensibles. Chaque sous-requête est exécutée sur le serveur contenant les données appropriées. Enfin, le résultat de la sous-requête sur données publiques est envoyé au serveur sécurisé qui se charge de construire le résultat final en toute sécurité. Cette architecture résolvant les problèmes de sécurité introduit néanmoins de sévères problèmes de performances dues aux caractéristiques physiques du serveur sécurisé (peu de RAM, asymétrie des coûts de lecture et d'écriture. . . ) qu'il est impératif de résoudre par des techniques d'optimisation de requêtesProtection of sensitive data is a major issue in the databases field. Many software and hardware solutions have been designed to protect data when stored and during query processing. Moreover, it is also necessary to provide a secure manner to combine sensitive data with public data. To achieve this goal, we designed a new storage and processing architecture. Our solution combines a main server that stores public data and a secure server dedicated to the storage and processing of sensitive data. The secure server is a hardware token which is basically a combination of (i) a secured microcontroller and (ii) a large external NAND Flash memory. The queries which combine public and sensitive data are split in two sub queries, the first one deals with the public data, the second one deals with the sensitive data. Each sub query is processed on the server storing the corresponding data. Finally, the data obtained by the computation of the sub query on public data is sent to the secure server to be mixed with the result of the computation on sensitive data. For security reasons, the final result is built on the secure server. This architecture resolves the security problems, because all the computations dealing with sensitive data are done by the secure server, but brings performance problems (few RAM, asymmetric cost of read/write operations. . . ). These problems will be solved by different strategies of query optimization
42
Tardif, Florent. "Practical considerations on cryptanalytic time-memory trade-offs." Thesis, Rennes 1, 2019. http://www.theses.fr/2019REN1S118.
Abstract:
Un compromis temps-mémoire cryptanalytique est une technique qui vise à réduire le temps nécessaire pour effectuer certaines attaques cryptographiques telles que l'inversion d'une fonction à sens unique. Une telle inversion intervient dans une des principales applications des compromis temps-mémoire : le cassage de mots de passe. La technique requiert un très lourd pré-calcul qui génère des tables utilisables pour accélérer la recherche exhaustive de l'attaque. L'attaque par compromis temps-mémoire est d'autant plus rapide qu'il y a de mémoire allouée à l'algorithme. Cependant, en pratique, la mémoire est souvent un facteur limitant. Nous évaluons l'impact d'un problème nécessitant une grande mémoire sur la technique des compromis temps-mémoire, notamment en se plaçant dans le contexte où une mémoire externe lente est utilisée à la place d'une mémoire rapide limitée (RAM). Nous établissons qu'une telle approche est applicable dans des cas pratiques, qui sont identifiés. Nous proposons ensuite une nouvelle construction de compromis temps-mémoire qui repose sur des fonctions de hachage minimales parfaites, et dont le stockage est moindre que sur les techniques de compression de tables existantes. Finalement, nous proposons une comparaison entre les améliorations existantes, possiblement combinées, et notre nouvelle techniqueA cryptanalytic time-memory trade-off (TMTO) is a technique that aims to reduce the time needed to perform a set of cryptanalysis attacks, such as inverting a one-way function. Such an inversion constitutes one of the main applications of TMTOs, which is password cracking. The technique relies on a large-scale pre-computation which outputs tables that allow to significantly speed up the attack's exhaustive search. The more memory is used by a TMTO, the faster the attack can be. In practice, the amount of memory available is often the limiting factor, so numerous approaches have been proposed to fit large tables in a restricted amount of memory. In this thesis, we focus on the rainbow tables variant, the most widely spread version of time-memory trade-offs. When the considered cryptographic problem is overwhelmingly sized, using an external memory is eventually needed. We analyse the relevance of using an external memory instead of RAM, and we state that it is fully suited for practical cases, which are identified. We then introduce a new technique, based on minimal perfect hash functions, whose storage complexity is better than any previous optimisation. Finally, we analyse and compare existing TMTO approaches as well as their combinations, along with our newly introduced MPHF rainbow technique. We are then able to provide a set of practical recommendations on how to configure the implementation of a TMTO in an optimal way
43
Ton, That Dai Hai. "Gestion efficace et partage sécurisé des traces de mobilité." Thesis, Université Paris-Saclay (ComUE), 2016. http://www.theses.fr/2016SACLV003/document.
Abstract:
Aujourd'hui, les progrès dans le développement d'appareils mobiles et des capteurs embarqués ont permis un essor sans précédent de services à l'utilisateur. Dans le même temps, la plupart des appareils mobiles génèrent, enregistrent et de communiquent une grande quantité de données personnelles de manière continue. La gestion sécurisée des données personnelles dans les appareils mobiles reste un défi aujourd’hui, que ce soit vis-à-vis des contraintes inhérentes à ces appareils, ou par rapport à l’accès et au partage sûrs et sécurisés de ces informations. Cette thèse adresse ces défis et se focalise sur les traces de localisation. En particulier, s’appuyant sur un serveur de données relationnel embarqué dans des appareils mobiles sécurisés, cette thèse offre une extension de ce serveur à la gestion des données spatio-temporelles (types et operateurs). Et surtout, elle propose une méthode d'indexation spatio-temporelle (TRIFL) efficace et adaptée au modèle de stockage en mémoire flash. Par ailleurs, afin de protéger les traces de localisation personnelles de l'utilisateur, une architecture distribuée et un protocole de collecte participative préservant les données de localisation ont été proposés dans PAMPAS. Cette architecture se base sur des dispositifs hautement sécurisés pour le calcul distribué des agrégats spatio-temporels sur les données privées collectéesNowadays, the advances in the development of mobile devices, as well as embedded sensors have permitted an unprecedented number of services to the user. At the same time, most mobile devices generate, store and communicate a large amount of personal information continuously. While managing personal information on the mobile devices is still a big challenge, sharing and accessing these information in a safe and secure way is always an open and hot topic. Personal mobile devices may have various form factors such as mobile phones, smart devices, stick computers, secure tokens or etc. It could be used to record, sense, store data of user's context or environment surrounding him. The most common contextual information is user's location. Personal data generated and stored on these devices is valuable for many applications or services to user, but it is sensitive and needs to be protected in order to ensure the individual privacy. In particular, most mobile applications have access to accurate and real-time location information, raising serious privacy concerns for their users.In this dissertation, we dedicate the two parts to manage the location traces, i.e. the spatio-temporal data on mobile devices. In particular, we offer an extension of spatio-temporal data types and operators for embedded environments. These data types reconcile the features of spatio-temporal data with the embedded requirements by offering an optimal data presentation called Spatio-temporal object (STOB) dedicated for embedded devices. More importantly, in order to optimize the query processing, we also propose an efficient indexing technique for spatio-temporal data called TRIFL designed for flash storage. TRIFL stands for TRajectory Index for Flash memory. It exploits unique properties of trajectory insertion, and optimizes the data structure for the behavior of flash and the buffer cache. These ideas allow TRIFL to archive much better performance in both Flash and magnetic storage compared to its competitors.Additionally, we also investigate the protect user's sensitive information in the remaining part of this thesis by offering a privacy-aware protocol for participatory sensing applications called PAMPAS. PAMPAS relies on secure hardware solutions and proposes a user-centric privacy-aware protocol that fully protects personal data while taking advantage of distributed computing. For this to be done, we also propose a partitioning algorithm an aggregate algorithm in PAMPAS. This combination drastically reduces the overall costs making it possible to run the protocol in near real-time at a large scale of participants, without any personal information leakage
44
Kauffmann-Tourkestansky, Xavier. "Analyses sécuritaires de code de carte à puce sous attaques physiques simulées." Phd thesis, Université d'Orléans, 2012. http://tel.archives-ouvertes.fr/tel-00771273.
Abstract:
Cette thèse s'intéresse aux effets des attaques par fautes physiques sur le code d'un système embarqué en particulier la carte à puce. De telles attaques peuvent compromettre la sécurité du système en donnant accès à des informations confidentielles, en compromettant l'intégrité de données sensibles ou en perturbant le fonctionnement pendant l'exécution. Dans cette thèse, nous décrivons des propriétés de sécurité permettant d'exprimer les garanties du système et établissons un modèle d'attaque de haut niveau définissant les capacités d'un attaquant à modifier le système. Ces propriétés et ce modèle nous servent à vérifier la sécurité du code par analyse statique ou test dynamique, combinés avec l'injection d'attaques, simulant les conséquences logicielles des fautes physiques. Deux méthodologies sont ainsi développées afin de vérifier le comportement fonctionnel du code sous attaques, tester le fonctionnement des sécurités implémentées et identifier de nouvelles attaques. Ces méthodologies ont été mises en oeuvre dans un cadre industriel afin de faciliter le travail du développeur chargé de sécuriser un code de carte à puce.
45
Duclos, Mathilde. "Méthodes pour la vérification des protocoles cryptographiques dans le modèle calculatoire." Thesis, Université Grenoble Alpes (ComUE), 2016. http://www.theses.fr/2016GREAM002/document.
Abstract:
Les échanges des informations confidentielles ou critiques dans un environnement public, et donc potentiellement hostile, nécessitent l'emploi de techniques cryptographiques (protocoles et primitives). Malheureusement, l'expérience montre qu'une mauvaise conception, ou une expression peu claire des propriétés et hypothèses de sécurité attendues conduisent à des attaques, et qu'il faut parfois des années avant que celles-ci soient découvertes et corrigées. D'où l'adoption croissante de la sécurité prouvable, où on donne une définition rigoureuse des objectifs de sécurité et des démonstrations mathématiques que ceux-ci sont remplis. Par ailleurs, la complexité et la diversité des systèmes cryptographiques croît également. Il est donc largement admis qu'il n'est plus viable d'écrire ou vérifier manuellement des démonstrations cryptographiques (Bellare& Rogaway 2004, Shoup 2004, Halevi 2005) et qu'il faut développer des méthodes de vérification des systèmes cryptographiques assistées par ordinateur. L'objectif de cette thèse est d'effectuer des progrès significatifs dans cette direction. Plus précisement on s'interesse à la preuve formelle de protocoles cryptographiques. Vérifier des protocoles cryptographiques requiert le développement d'un cadre théorique qui doit permettre: - une modélisation précise des protocoles cryptographiques et des propriétés de sécurité qu'on veut prouver dans le modèle calculatoire. - mise en place de stratégies d'automatisation de preuves. - prise en compte des modèles plus réalistes pour l'adversaire (canaux cachés, ressources de calcul). A la fin de la thèse on a obtenu un cadre formel et un ensemble de méthodes logicielles capable d'aider à la vérification des protocoles cryptographiquesCritical and private information are exchanged on public environment. To protect it from dishonest users, we use cryptographic tools. Unfortunately, bad conception, poorly written security properties and required security hypothesis lead to attacks, and it may take years before one discover the attack and fix the security schemes involved. In this context, provable security provides formal definitions for security objectives and implied mathematical proofs that these objectives are fullfilled. On another hand, complexity and variety of cryptographic systems are increasing, and proofs by hand are too complicated to write and to verify (Bellare& Rogaway 2004, Shoup 2004, Halevi 2005). Thus, we need computer-assisted verification methods for cryptographic systems. The aim of this thesis is to progress in this direction. More precisely we want significant progress over formal proofs on cryptographic protocols. To verify cryptographic protocols we need to develop a theoritical framework providing: - a precise modelisation for cryptographic protocols and security properties we want to prove in the computationnal model, - designing tactics to automate proofs, - taking into account realistic models for adversary (side-channels...). By the end of the thesis we have enhanced a theoretical framework and computing tools helping verifying cryptographic protocols
46
Venelli, Alexandre. "Contribution à la sécurite physique des cryptosystèmes embarqués." Thesis, Aix-Marseille 2, 2011. http://www.theses.fr/2011AIX22005/document.
Abstract:
Ces travaux de thèse se concentrent sur l'étude des attaques par canaux cachés et les implications sur les mesures à prendre pour un concepteur de circuits sécurisés. Nous nous intéressons d'abord aux différentes attaques par canaux cachés en proposant une amélioration pour un type d'attaque générique particulièrement intéressante : l'attaque par analyse d'information mutuelle. Nous étudions l'effet des différentes techniques d'estimation d'entropie sur les résultats de l'attaque. Nous proposons l'utilisation de fonctions B-splines comme estimateurs étant donné qu'elles sont bien adaptées à notre scénario d'attaques par canaux cachés. Nous étudions aussi l'impact que peut avoir ce type d'attaques sur un cryptosystème symétrique connu, l'Advanced Encryption Standard (AES), en proposant une contre-mesure basée sur la structure algébrique de l'AES. L'opération principale de la majorité des systèmes ECC est la multiplication scalaire qui consiste à additionner un certain nombre de fois un point de courbe elliptique avec lui-même. Dans une deuxième partie, nous nous intéressons à la sécurisation de cette opération. Nous proposons un algorithme de multiplication scalaire à la fois efficace et résistant face aux principales attaques par canaux cachés. Nous étudions enfin les couplages, une construction mathématique basée sur les courbes elliptiques, qui possède des propriétés intéressantes pour la création de nouveaux protocoles cryptographiques. Nous évaluons finalement la résistance aux attaques par canaux cachés de ces constructionsThis thesis focuses on the study of side-channel attacks as well as their consequences on the secure implementation of cryptographic algorithms. We first analyze different side-channel attacks and we propose an improvement of a particularly interesting generic attack: the mutual information analysis. We study the effect of state of the art entropy estimation techniques on the results of the attack. We propose the use of B-spline funtions as estimators as they are well suited to the side-channel attack scenario. We also investigate the consequences of this kind of attack on a well known symmetric cryptosystem, the Advanced Encryption Standard (AES), and we propose a countermeasure based on the algebraic structure of AES. The main operation of ECC is the scalar multiplication that consists of adding an elliptic curve point to itself a certain number of times. In the second part, we investigate how to secure this operation. We propose a scalar multiplication algorithm that is both efficient and secure against main side-channel attacks. We then study pairings, a mathematical construction based on elliptic curves. Pairings have many interesting properties that allow the creation of new cryptographic protocols. We finally evaluate the side-channel resistance of pairings
47
Andouard, Philippe. "Outils d'aide à la recherche de vulnérabilités dans l'implantation d'applications embarquées sur carte à puce." Thesis, Bordeaux 1, 2009. http://www.theses.fr/2009BOR13958/document.
Abstract:
Les travaux présentés dans cette thèse ont pour objectif de faciliter les évaluations sécuritaires des logiciels embarqués dans les cartes à puce. En premier lieu, nous avons mis au point un environnement logiciel dédié à l'analyse de la résistance d'implémentations d'algorithmes cryptographiques face à des attaques par analyse de la consommation de courant. Cet environnement doit être vu comme un outil pour rechercher des fuites d'information dans une implémentation en vue d'évaluer la faisabilité d'une attaque sur le produit réel. En second lieu, nous nous sommes intéressé à l'analyse de programmes écrits en langage d'assemblage AVR dans le but de vérifier s'ils sont vulnérables aux \textsl{timing attacks}. Nous avons donc développé un outil qui consiste à décrire des chemins du flot de contrôle d'un programme grâce à des expressions régulières qui seront par la suite interprétées par notre outil afin de donner leur temps exact d'exécution (en terme de cycles d'horloge). Enfin, nous avons étudié comment faciliter la compréhension de programmes écrits en langage C dans le but de vérifier si des politiques de sécurité sont correctement implémentées. D'une part, nous fournissons des assistants de navigation qui au travers d'informations concernant les variables et procédures rencontrées, facilitent la compréhension du programme. D'autre part, nous avons au point une manière de vérifier les politiques de sécurité sans modélisation préalable (e.g. avec un automate à états finis) au moyen de requêtes exprimées dans la logique CTLThe work presented in this thesis aims at easing the evaluation process of smartcards embedded software. On one hand, we set up a software environment dedicated to analyze the implementation resistance of cryptographic to power analysis attacks. This environment must be seen as a tool that facilitates a real attack by giving a way to find information leakages in an implementation. On the other hand, we focused on analyzing program written in AVR assembly language in order to check whether they are vulnerable to timing attacks. To achieve this goal we have developed a tool that makes possible the description of a path in the control flow of the program thanks to regular expressions. Those regular expressions will be interpreted by our tool in order to give the exact execution timing (expressed in clock cycles). Finally, we studied how to ease the global comprehension of a program written in C language in order to check whether security policies are well implemented. First, we provide graphical navigation assisants that helps to understand the progam being analyzed by giving information on variables and procedures. Then, we provide a way to check the security policies through the use of requests expressed with the CTL logic. This approach does not need prior modelisation of the program
48
Barki, Amira. "Mécanismes cryptographiques conciliant authentification et respect de la vie privée dans le contexte du M2M." Thesis, Compiègne, 2016. http://www.theses.fr/2016COMP2337.
Abstract:
Les applications Machine-to-Machine (M2M) fournissent plus de confort aux utilisateurs et permettent une utilisation optimale des ressources. Toutefois, ces applications ne présentent pas que des avantages. Ces dernières peuvent engendrer des problèmes de sécurité, voire porter atteinte à la vie privée de leurs utilisateurs. Dans cette thèse, nous nous intéressons à la sécurité des applications M2M, et plus précisément à l'authentification et la préservation de la vie privée d'utilisateurs d'équipements M2M dotés d'une carte SIM. Dans une première partie, nous proposons cinq nouvelles primitives cryptographiques, à savoir un schéma de signature partiellement aveugle, deux schémas de codes d'authentification de messages, ainsi que deux schémas d'attestations anonymes. Ces nouvelles primitives sont plus efficaces, voire fournissent des fonctionnalités nouvelles par rapport aux schémas de l'état de l'art et sont adaptées aux environnements limités en ressources telles que les cartes SIMs. En nous appuyant sur ces primitives, nous construisons de nouveaux protocoles préservant la vie privée des utilisateurs. Plus précisément, nous introduisons un nouveau système de paiement anonyme efficace. Nous proposons également un protocole d’authentification et d’identification anonyme pour la nouvelle génération de cartes SIMs connue sous le nom d'Embedded SIM. Par ailleurs, nous construisons un système d'accréditations anonymes. Enfin, nous spécifions un système de vote électronique efficace rendant inutile toute forme de coercition à l'encontre d'un électeur. La sécurité de toutes nos contributions est prouvée dans le modèle de l'oracle aléatoire sous des hypothèses classiquesMachine to Machine (M2M) applications enable a better management of resources and provide users With greater cornfort. Unfortunately, they also entail serious security and privacy concerns. ln this thesis, we focus on M2M security, and particularly on the authentication and privacy issues of M2M applications involving a SIM card. ln the first part, we design five new cryptographic primitives and formally prove that they meet the expected security requirements. More precisely, they consist of a partially blind signature scheme, a sequential aggregate Message Authentication Codes (MAC) scheme, an algebraic MAC scheme and two pre-Direct Anonymous Attestation (pre-DAA) schemes. Some of the proposed schemes aim to achieve a particular property that was not provided by previous constructions whereas others intend to improve the efficiency of state-of-the-art schemes. Our five schemes do not require the userls device to compute pairings. Thus, they are suitable for resource constrained environments such as SIM cards. ln a second part, we rely on these primitives to propose new privacy-preserving protocols. More specifically, we design an efficient private eCash system. We also propose a protocol enabling anonymous authentication and identification of embedded SIMs (eSlMs). Furthermore, we rely on our algebraic MAC scheme to build a practical Keyed-Verification Anonymous Credentials (KVAC) system. Finally, based on our sequential aggregate MAC scheme, we introduce a remote electronic voting system that is coercion-resistant and practical for real polls. The security of our protocols is formally proven in the Random Oracle Model (ROM) under classical computational assumptions
49
Dehbaoui, Amine. "Analyse Sécuritaire des Émanations Électromagnétiques des Circuits Intégrés." Thesis, Montpellier 2, 2011. http://www.theses.fr/2011MON20020.
Abstract:
Le développement de la société de l'information et de la monnaie virtuelle, a soulevé de nouveaux problèmes aux communautés de la sécurité et du circuit intégré, faisant devenir la cryptologie un outil incontournable permettant de répondre aux exigences sécuritaires telles que l'identification, l'authentification ou la confidentialité. L'intégration des primitives cryptographiques dans différents dispositifs électroniques est largement répandue aujourd'hui dans le domaine des communications, des services financiers, des services gouvernementaux ou de la PayTV. Au premier rang de ces dispositifs, figure la carte à puce. D'après un rapport publié en août 2010, IMS Research prévoit que le marché de la carte à puce atteindra les 5.8 milliards d'unités vendues en fin d'année. La grande majorité est utilisée dans les télécommunications (carte SIM) et les services bancaires. La carte à puce incorpore un circuit intégré qui peut être, soit un processeur dédié aux calculs cryptographiques, soit seulement de la mémoire non-volatile ou les deux. Ces circuits intégrés manipulent et contiennent donc des secrets comme les clefs secrètes ou privées utilisées par les algorithmes de cryptographie symétriques ou asymétriques. Ces clefs doivent donc, rester absolument confidentielles et intègres afin de garantir la chaîne de sécurité. Par conséquent la robustesse des cartes à puces aux attaques cryptographiques est cruciale. En effet, les attaques sur les circuits intégrés sont aujourd'hui très performantes. Elles peuvent être classées selon trois grandes familles : invasives, semi-invasives et non-invasives. 1- Les attaques invasives sont des attaques menées en général par des experts et requièrent du matériel spécifique. 2- Les attaques semi-invasives, famille d'attaques récemment introduite par l'équipe de Ross Anderson, dont le principe est de décapsuler le package contenant le circuit, afin de se positionner le plus proche possible de la surface, sans pour autant en détériorer les fonctionnalités. 3- Les attaques non-invasives ne nécessitent aucune préparation préalable du dispositif soumis aux attaques. Elles consistent à espionner les phénomènes physiques engendrés par la manipulation des données et notamment les clefs secrètes. Les attaques non-invasives peuvent être considérées comme les plus dangereuses, dans la mesure où ce type d'attaque peut être réalisé sans contact avec le circuit. En effet, pendant l'utilisation d'appareils électroniques, les circuits qui les composent sont soumis à des variations de courant et de tension. Ces variations génèrent des ondes électromagnétiques qui se propagent dans le voisinage du circuit. Ces émanations présentent une corrélation avec des informations censées être stockées dans la puce de façon sécurisée (exemple: la clef secrète d'une carte bancaire utilisée pour l'authentification). Plusieurs attaques dites par canaux auxiliaires, et basées sur ces fuites électromagnétiques ont été publiées par la communauté scientifique ces dernières années. Cette thèse a pour objectifs: (a) comprendre les différentes sources des émanations électromagnétiques des circuits intégrés, et de proposer un flot d'attaque électromagnétique localisée et en champ proche afin de tester la robustesse d'un circuit cryptographique contre les attaques et analyses utilisant le canal électromagnétique, et (b) proposer des contre-mesures afin de contrecarrer ces attaques par analyse de champ électromagnétique. Afin d'atteindre ces objectifs, nous présentons, dans un premier temps, une technique efficace nommée WGMSI (Weighted Global Magnitude Squared Incoherence) pour localiser les positions, au-dessus du circuit cryptographique, qui génèrent les émanations électromagnétiques les plus dépendantes des données secrètes. Dans un deuxième temps la WGMSI est utilisée aussi pour améliorer la stabilité et la convergence des différentes attaques électromagnétiques proposées dans la littérature. La suite de la thèse décrit les différentes contre-mesures aux attaques par canaux auxiliaires. En effet, face à ces techniques d'attaques évoluées, il est primordial, de rendre les fonctions cryptographiques implantées dans les circuits intégrés pour la sécurité (confidentialité, authentification, intégrité ... ), inattaquables en un temps raisonnable et ceci même en manipulant des sous-clefs dans des chiffrements par blocs. Pour cela, on se focalisera principalement aux contre-mesures basées sur des logiques différentielles et dynamiques. Ces contre-mesures sont dites par conception, puisqu'elles se situent au niveau des portes logiques qui sont considérées comme les éléments de base pour la conception d'un circuit intégré. Ceci permet une certaine indépendance des algorithmes cryptographiques vis à vis de l'architecture ou de la technologie considérées. Parmi les différentes logiques différentielles et dynamiques, on s'intéressera plus spécifiquement à la logique STTL (Secure Triple Track logic) qui peut être considérée comme une amélioration de la logique double rail, dans la mesure où un troisième rail est ajouté afin de contrecarrer la faiblesse principale de la logique double rail, à savoir l'évaluation anticipée. Enfin, nous présenterons un flot d'implémentation sur FPGA de la logique STTL prouvée robuste aux attaques par analyse de courant, et nous implémenterons un prototype de DES STTL afin de tester sa robustesse aux attaques électromagnétiques localisées en champ procheThe integration of cryptographic primitives in different electronic devices is widely used today incommunications, financial services, government services or PayTV.Foremost among these devices include the smart card. According to a report published in August 2010, IMS Research forecasts that the smart card market will reach 5.8 billion units sold in this year. The vast majority is used in telecommunications (SIM) and banking.The smart card incorporates an integrated circuit which can be a dedicated processor for cryptographic calculations. Therefore, these integrated circuits contain secrets such as secret or private keys used by the symmetric or asymmetric cryptographic algorithms. These keys must remain absolutely confidential to ensure the safety chain.Therefore the robustness of smart cards against attacks is crucial. These attacks can be classifiedinto three main categories: invasive, semi-invasive and non-invasive.Non-invasive attacks can be considered the most dangerous, since this kind of attack can be achieved without any contact with the circuit.Indeed, while using electronic circuits that compose them are subjected to variations in current and voltage. These variations generate an electromagnetic radiation propagating in the vicinity of the circuit.These radiations are correlated with secret information (eg a secret key used for authentication). Several attacks based on these leakages were published by the scientific community.This thesis aims to: (a) understand the different sources of electromagnetic emanations of integrated circuits, and propose a localized near field attack to test the robustness of a cryptographic circuit and (b) propose counter-measures to these attacks
50
Ruhault, Sylvain. "Security analysis for pseudo-random number generators." Thesis, Paris, Ecole normale supérieure, 2015. http://www.theses.fr/2015ENSU0014/document.
Abstract:
La génération d’aléa joue un rôle fondamental en cryptographie et en sécurité. Des nombres aléatoires sont nécessaires pour la production de clés cryptographiques ou de vecteurs d’initialisation et permettent également d’assurer que des protocoles d’échange de clé atteignent un niveau de sécurité satisfaisant. Dans la pratique, les bits aléatoires sont générés par un processus de génération de nombre dit pseudo-aléatoire, et dans ce cas, la sécurité finale du système dépend de manière cruciale de la qualité des bits produits par le générateur. Malgré cela, les générateurs utilisés en pratique ne disposent pas ou peu d’analyse de sécurité permettant aux utilisateurs de connaître exactement leur niveau de fiabilité. Nous fournissons dans cette thèse des modèles de sécurité pour cette analyse et nous proposons des constructions prouvées sûres et efficaces qui répondront à des besoins de sécurité forts. Nous proposons notamment une nouvelle notion de robustesse et nous étendons cette propriété afin d’adresser les attaques sur la mémoire et les attaques par canaux cachés. Sur le plan pratique, nous effectuons une analyse de sécurité des générateurs utilisés dans la pratique, fournis de manière native dans les systèmes d’exploitation (/dev/random sur Linux) et dans les librairies cryptographiques (OpenSSL ou Java SecureRandom) et nous montrons que ces générateurs contiennent des vulnérabilités potentiellesIn cryptography, randomness plays an important role in multiple applications. It is required in fundamental tasks such as key generation and initialization vectors generation or in key exchange. The security of these cryptographic algorithms and protocols relies on a source of unbiased and uniform distributed random bits. Cryptography practitioners usually assume that parties have access to perfect randomness. However, quite often this assumption is not realizable in practice and random bits are generated by a Pseudo-Random Number Generator. When this is done, the security of the scheme depends of course in a crucial way on the quality of the (pseudo-)randomness generated. However, only few generators used in practice have been analyzed and therefore practitioners and end users cannot easily assess their real security level. We provide in this thesis security models for the assessment of pseudo-random number generators and we propose secure constructions. In particular, we propose a new definition of robustness and we extend it to capture memory attacks and side-channel attacks. On a practical side, we provide a security assessment of generators used in practice, embedded in system kernel (Linux /dev/random) and cryptographic libraries (OpenSSL and Java SecureRandom), and we prove that these generators contain potential vulnerabilities