Thèse diffusée initialement dans le cadre d'un projet pilote des Presses de l'Université de Montréal/Centre d'édition numérique UdeM (1997-2008) avec l'autorisation de l'auteur.

Cette thèse s'intéresse en premier lieu à l'analyse des effetsfonctionnels des erreurs dans laconfiguration de FPGAs à base de SRAM. Ces erreurs peuvent provenir deperturbations naturelles(rayonnements, particules) ou d'attaques volontaires, par exemple avecun laser. La famille Virtex IIde Xilinx est utilisée comme premier cas pratique d'expérimentation,puis une comparaison est réaliséeavec la famille AT40K de chez ATMEL. Ceci a permis de mieux comprendrel'impact réel dedifférentes sources de perturbations, et les motifs d'erreur devantréellement être pris en compte pouraméliorer la robustesse d'un circuit implanté sur ce type detechnologie. Cette étude a nécessité ledéveloppement d'outils de conception spécifiques, permettantd'automatiser les analyses. Uneméthodologie innovante est proposée pour l'évaluation de lasensibilité de la mémoire de configurationaux SEUs : une classification des bits de configuration est établie enfonction des effets produits parleur inversion sur le fonctionnement normal de l'application. Cecipermet de déterminer les zones lesplus critiques, autorisant le développement de stratégies deprotection sélectives et à faible coût.

L'inclusion de requête est un problème bien étudié sur plusieurs décennies de recherche. En règle générale, il est défini comme le problème de déterminer si le résultat d'une requête est inclus dans le résultat d'une autre requête pour tout ensemble de données. Elle a des applications importantes dans l'optimisation des requêtes et la vérification de bases de connaissances. L'objectif principal de cette thèse est de fournir des procédures solides et com- plètes pour déterminer l'inclusion des requêtes SPARQL en vertu d'exprimés en axiomes logiques de description. De plus, nous mettons en œuvre ces procédures à l'appui des résultats théoriques par l'expérimentation. À ce jour, test d'inclusion de requête a été effectuée à l'aide de différentes techniques: homomorphisme de graphes, bases de données canoniques, les tech- niques de la théorie des automates et par une réduction au problème de la va- lidité de la logique. Dans cette thèse, nous utilisons la derniere technique pour tester l'inclusion des requêtes SPARQL utilisant une logique expressive appelée μ-calcul. Pour ce faire, les graphes RDF sont codés comme des systèmes de transitions, et les requêtes et les axiomes du schéma sont codés comme des formules de μ-calcul. Ainsi, l'inclusion de requêtes peut être réduit á test de validité de formule logique. L'objectif de cette thèse est d'identifier les divers fragments de SPARQL (et PSPARQL) et les langages de description logique de schéma pour lequelle l'inculsion est décidable. En outre, afin de fournir théoriquement et expériment- alement éprouvées procédures de vérifier l'inclusion de ces fragments décid- ables. Pas durer au moins mais, cette thèse propose un point de repère pour les solveurs d'inclusion. Ce benchmark est utilisé pour tester et comparer l'état actuel des solveurs d'inclusion.

Le chapitre 2 présente la première partie importante de nos travaux : l'approche pour la détection que nous proposons. Nous avons tout d'abord expliqué les caractéristiques des attaques contre les données de calcul et en quoi ces dernières se distinguent des autres types d'attaque. Ceci nous a notamment permis de montrer que pour perpétuer une intrusion, un utilisateur malveillant va chercher à cibler un ensemble bien précis de données de calcul. À l'aide de la logique de Hoare, nous avons ensuite expliqué que le code source des applications peut contenir des informations qui peuvent être utilisées pour détecter ce type bien précis d'attaque. Nous avons détaillé cela sur un exemple d'exploitation de vulnérabilité. Puis, nous avons présenté notre modèle de détection. Nous l'avons tout d'abord présenté empiriquement sur un cas réel d'attaques contre les données de calcul. Pour cela, nous avons détaillé la vulnérabilité utilisée dans notre exemple ainsi que les différents scénarios d'attaque et comment des invariants portant sur certaines variables permettent de détecter ces attaques. Enfin, nous avons présenté formellement notre modèle de détection. Celui-ci correspond à l'ensemble des domaines de variation des variables qui influencent l'exécution des appels de fonction. Ces domaines de variation sont calculés juste avant les appels de fonction et uniquement pour les variables qui sont atteignables à ces endroits du code source. Nous avons ensuite présenté une méthode pour construire un tel modèle. Premièrement, nous proposons d'utiliser le graphe de dépendance du programme pour déterminer pour chaque appel de fonction l'ensemble des variables qui influencent son exécution. Deuxièmement, nous proposons d'utiliser l'interprétation abstraite pour calculer pour chacun de ces ensembles de variables leur domaine de variation. Pour finir, nous présentons une implémentation de notre approche que nous avons réalisée pour les programmes écrits en langage C. Nous détaillons d'abord la phase de construction du modèle qui repose sur un outil d'analyse statique existant, Frama-C. Nous détaillons ensuite la phase d'instrumentation, celle-ci ayant pour contrainte de ne pas modifier le processus original de compilation. Le chapitre 3 présente la seconde partie importante de nos travaux : l'approche pour l'évaluation que nous proposons. Nous commençons par aborder la problématique de la simulation des erreurs engendrées par les attaques contre les données de calcul. Pour cela, nous présentons d'abord le modèle de faute que nous proposons pour simuler ce type bien particulier d'attaques. Nous étudions les caractéristiques qui doivent être simulées, quel sera leur impact sur le programme et dans quel cas ces dernières peuvent être détectées. Nous expliquons ensuite comment nous proposons de construire notre modèle de simulation. La principale problématique ici est de savoir comment déterminer l'ensemble des cibles potentielles. Il s'agit du même ensemble de variables que pour la détection. Nous proposons donc à nouveau de nous reposer sur le graphe de dépendance du programme et d'embarquer les mécanismes d'injection au sein des applications. Nous expliquons ensuite comment notre modèle de faute peut être utilisé pour l'évaluation d'un système de détection d'intrusion. Nous posons comme objectif que le résultat obtenu doit être une sur-approximation du taux de faux négatifs réel. Cela implique que nous voulons placer le système de détection d'intrusion à évaluer dans la situation la moins favorable possible. Pour respecter cette contrainte, nous montrons que notre modèle de faute doit être utilisé pour simuler une intrusion qui ne nécessite qu'une seule exploitation de la vulnérabilité, que la vulnérabilité donne accès à l'ensemble de l'espace mémoire du processus et que l'exploitation ne vise qu'une seule variable. Nous présentons enfin les modifications que nous avons apportées à notre outil afin qu'il instrumente aussi les programmes pour l'injection et comment les mécanismes d'injection ainsi ajoutés doivent être utilisés. Le chapitre 4 présente la dernière partie de nos travaux : l'évaluation de notre système de détection d'intrusion, notamment à l'aide de notre modèle de simulation d'attaque. Nous commençons par présenter la plateforme de tests que nous avons développée autour de nos mécanismes d'injection. Il s'agit d'une plateforme qui automatise la réalisation de tests ainsi que l'analyse des résultats obtenus. Nous abordons tout d'abord les problématiques d'écriture des scénarios d'exécution et de collecte des informations. Les scénarios doivent permettre de couvrir suffisamment le code des programmes utilisés pour les tests. Nous avons choisi de mesurer ce taux de couverture en fonction des appels de fonction. Les informations collectées sont utilisées pour produire deux résultats : une sur-approximation du taux réel de faux négatifs et une évaluation du taux de détection pour les injections ayant provoqué une déviation comportementale. Pour finir, nous présentons les résultats de l'évaluation de notre système de détection d'intrusion. Nous commençons par donner les performances de l'analyse. On note que la durée d'analyse peut être très grande, notamment en fonction de la taille du code à analyser, mais qu'en fonction de la sémantique du code, deux programmes de taille similaire peuvent présenter des durées d'analyse complètement différentes. Puis, nous donnons le niveau de surcharge à l'exécution. On note que la surcharge induite par nos mécanismes de détection est très faible, toujours inférieure à 1%. Nous continuons avec les performances de la détection. Nous pouvons voir que les résultats de la détection varient grandement d'un programme à l'autre, malgré un taux d'instrumentation similaire. Ce qui change, c'est le nombre d'invariants vérifiés. On voit ici la limite de notre approche : si la sémantique du code original ne permet pas de calculer suffisamment d'invariants, l'efficacité de notre approche sera alors limitée. De plus, la propagation de l'erreur n'apporte que peu d'aide à notre modèle de détection. Dans tous les cas, nous avons pu vérifier que notre approche ne génère bien pas de faux positif.

Dans cette thèse, nous analysons les problèmes liés à la représentation finie des nombres réels et nous contrôlons la déviation induite par cette approximation. Nous nous intéressons particulièrement à deux problèmes. Le premier est l'étude de l'influence de la représentation finie sur les protocoles de confidentialité différentielle. Nous présentons une méthode pour étudier les perturbations d'une distribution de probabilité causées par la représentation finie des nombres. Nous montrons qu'une implémentation directe des protocoles théoriques pour garantir la confidentialité différentielle n'est pas fiable, tandis qu'après l'ajout de correctifs, la propriété est conservée en précision finie avec une faible perte de confidentialité. Notre deuxième contribution est une méthode pour étudier les programmes qui ne peuvent pas être analysés par composition à cause de branchements conditionnels au comportement trop erratique. Cette méthode, basée sur la théorie des systèmes de réécriture, permet de partir de la preuve de l'algorithme en précision exacte pour fournir la preuve que le programme en précision finie ne déviera pas trop.

Aujourd'hui, les contenus et les applications Web sont devenus la principale interface pour effectuer toutes sortes de tâches de la vie quotidienne comme déclarer et payer les impôts, réserver des billets d'avion ou de train, planifier des vacances, effectuer des achats, gérer les comptes bancaires, etc. En conséquence, il devient de plus en plus important d'étudier leurs fondements, d'améliorer leurs capacités, de faciliter leur conception, de vérifier leur fonctionnement, de les optimiser automatiquement et les rendre plus souples et adaptables aux usages et aux différentes plateformes. Dans ce document, nous décrivons d'abord mes activités professionnelles, concernant les années 1998 à 2012. La première partie de ce document contient un résumé de mes activités de recherche, d'encadrement, d'enseignement et charges administrative et collective, ainsi qu'un résumé de mes principaux résultats scientifiques. Dans le reste du document, nous introduisons une logique de raisonnement sur les arbres finis, une procédure de décision correcte et complète pour vérifier la satisfaisabilité d'une formule de la logique ainsi que d'une mise en œuvre efficace en pratique. La logique est une variante du mu-calcul adaptée aux arbres finis et équipée avec des modalités arrières et des nominaux. Ensuite, nous considérons le problème de l'évolution des schémas XML. Dans le contexte en constante évolution du Web, les schémas XML changent continuellement afin de faire face à l'évolution naturelle des entités qu'ils décrivent. Les modifications de schémas peuvent avoir des conséquences importantes dans la mesure où les documents existants peuvent devenir invalides et la programmes les manipulant incorrectes. Nous proposons un cadre unificateur pour déterminer les effets de l'évolution des schémas XML à la fois sur la validité des documents et des requêtes contenues dans ces programmes. Dans la dernière partie du document, nous considérons une algèbre de type équipée de la récursivité, du produit cartésien, des fonctions, de l'intersection, de l'union, et du complément ainsi que des variables de type et une quantification universelle implicite sur ces variables. Nous considérons la relation de sous-typage récemment définie par Castagna et Xu sur des expressions de cette algèbre de type et montrons que le sous-typage peut être décidé avec une complexité EXPTIME et implémenté efficacement en pratique clôturant ainsi à une question ouverte dans la littérature.

Ce mémoire présente les résultats de calculs analytiques de prédiction du comportement de dispositifs de retenue de niveau PL-2 armé d'armature en polymères renforcés de fibres de verre (PRFV) soumis aux essais de chargement quasi statique horizontal. L'un des modèles analytiques à l'étude est le calcul de la charge ultime que peut reprendre un dispositif de retenue en fonction des dimensions de la fissure au niveau de la connexion. Le deuxième modèle analytique à l'étude est le calcul de prédiction de la relation charge-déflexion en tête de muret. La collaboration entre le Ministère des Transports du Québec (MTQ), le Ministère des Transports de l'Alberta et l'Université de Sherbrooke a permis d'effectuer des essais quasi statiques sur plusieurs configurations durant les dernières années. Les configurations de dispositifs provenant du MTQ sont des barrières de type 210 et 311 dont les murets et les dalles sont entièrement armés de barres en PRFV. Les configurations des dispositifs de l'Alberta sont quant à eux des dispositifs de type S-1642 et S-1650 dont les murets sont armés de barres en PRFV et les dalles sont armées de barres d'acier enduit d'époxy. Grâce à cette banque de données, il est possible d'effectuer l'étude des modèles sur différentes configurations et ainsi déterminer certaines de leurs limites. De plus, une modélisation par éléments finis de la configuration de dispositif de retenue de type 311 (PL-2) a été effectuée. Le dispositif a été modélisé en trois dimensions avec le logiciel ADINA. De ce modèle, une comparaison avec les données expérimentales a été effectuée afin de le valider. De plus, une étude paramétrique a été effectuée sur l'influence des résistances du béton de la dalle et du muret et du module d'élasticité des barres en polymères renforcés de fibres (PRF). En effet, des bétons de 35 MPa et 50 MPa ont été utilisés afin de représenter trois cas de combinaison de résistance en compression des bétons. Finalement, trois grades de modules élastiques ont été utilisés sur le dispositif ayant un béton de 35 MPa au niveau de la dalle et un béton de 50 MPa au niveau du muret (combinaison la plus courante) afin d'étudier l'effet du module élastique des barres.

L'objectif de cette thèse est de caractériser le comportement confiné en cisaillement du béton sous chargement statique et dynamique. La méthode expérimentale reprend le concept de l'essai 'Punch Through Shear' qui consiste dans un premier temps à soumettre une éprouvette de béton à un chargement radial puis à appliquer au cours d'une deuxième étape un chargement axial qui permet de cisailler la partie centrale de l'échantillon.Deux méthodes ont été utilisées pour appliquer la contrainte de confinement à l'éprouvette avant de la soumettre à un chargement de cisaillement. La première méthode consiste à appliquer une pression hydrostatique via un fluide de confinement. Ces essais sont réalisés avec la presse Giga. La deuxième méthode consiste à utiliser une cellule métallique pré-déformée à l'aide d'une presse hydraulique. Durant le déchargement de la cellule, des contraintes de confinement sont transmises à l'éprouvette de béton. Cette cellule est instrumentée avec des jauges de déformation qui permettent de mesurer le niveau de confinement appliqué au béton.Les éprouvettes de béton confinées avec la cellule sont soumises à deux types de chargement : l'un statique avec une presse hydraulique normale et l'autre dynamique avec un système aux barres de Hopkinson. Cela permet d'étudier le comportement du béton en cisaillement confiné sur une large gamme de vitesse de déformation.Les résultats des campagnes d'essais montrent que la contrainte de cisaillement du béton augmente avec la pression de confinement. D'autre part, des échantillons saturés d'eau et d'autres séchés à l'étuve sont testés afin de vérifier l'influence de la teneur d'eau sur la résistance au cisaillement. Une résistance au cisaillement des échantillons de béton R30A7 sec supérieure à celle des échantillons saturés est observée sur la plage de déformation considérée. Une influence modeste de la vitesse de déformation en comparaison de ce qui est observé sous chargement en traction dynamique a été remarquée. De plus, un béton haute performance a été testé pour étudier l'influence de la composition du béton sur sa résistance au cisaillement. Il a été observé que la résistance au cisaillement du béton haute performance dépasse fortement celle du béton ordinaire. Les résultats obtenus sont comparés à ceux de la littérature, pour lesquelles des méthodes expérimentales différentes avaient été utilisées. / This PhD thesis focuses on studying the confined behavior of concrete under shear loading in static and dynamic conditions. An experimental method based on the Punch-Through Shear (PTS) test is used in order to investigate shear behavior in mode II conditions. The concept of this test is to first subject the specimen to a confining pressure and then an axial loading is applied to punch through the central portion of the core.In order to introduce confinement to the concrete sample prior to testing it under shear, two methods have been used. The first one is an active confinement applied by means of a high capacity triaxial press Giga. The second method consists in confining the sample with a pre-stressed metallic cell instrumented with hoop strain gages in order to evaluate the confinement acting in the ligament of the concrete sample.Samples confined with the pre-stressed cell are subjected to two types of loading; static and dynamic. The static tests are carried out by means of a normal hydraulic press while dynamic shear testing are performed using a modified Split Hopkinson Bar setup which allows to determine the shear response of concrete over a wide range of strain-rates.The results of test campaigns show that the shear strength of the concrete increases significantly with an increase of confining pressure. Furthermore, dry and saturated concrete samples have been tested in order to study the influence of saturation ratio on the shear behavior of concrete. The results show a higher shear strength with dry samples than in wet ones. Moreover, a small influence (compared to what was observed in dynamic tension) of the strain rate was observed. A high performance concrete was also studied to investigate the influence of concrete composition on its shear strength. It was observed that its shear strength strongly exceeds that of the ordinary concrete. The obtained results are compared with data from literature obtained with different experimental methods.

No description available.

La disponibilité de gros volumes de données structurées selon le modèle Resource Description Framework (RDF) est en constante augmentation. Cette situation implique un intérêt scientifique et un besoin important de rechercher de nouvelles méthodes d’analyse et de compilation de requêtes pour tirer le meilleur parti de l’extraction de données RDF. SPARQL est le plus utilisé et le mieux supporté des langages de requêtes sur des données RDF. En parallèle des langages de requêtes, les langages de définition de schéma d’expression de contraintes sur des jeux de données RDF ont également évolués. Les Shape Expressions (ShEx) sont de plus en plus utilisées pour valider des données RDF et pour indiquer les motifs de graphes attendus. Les schémas sont importants pour les tâches d’analyse statique telles que l’optimisation ou l’injection de requêtes. Notre intention est d’examiner les moyens et méthodologies d’analyse statique et d’optimisation de requêtes associés à des contraintes de schéma.Notre contribution se divise en deux grandes parties. Dans la première, nous considérons le problème de l’injection de requêtes SPARQL en présence de contraintes ShEx. Nous proposons une procédure rigoureuse et complète pour le problème de l’injection de requêtes avec ShEx, en prenant en charge plusieurs fragments de SPARQL. Plus particulièrement, notre procédure gère les patterns de requêtes OPTIONAL, qui s’avèrent former un important fonctionnalité à étudier avec les schémas. Nous fournissons ensuite les limites de complexité de notre problème en considération des fragments gérés. Nous proposons également une méthode alternative pour l’injection de requêtes SPARQL avec ShEx. Celle-ci réduit le problème à une satisfiabilité de Logique de Premier Ordre, qui permet de considérer une extension du fragment SPARQL traité par la première méthode. Il s’agit de la première étude traitant l’injection de requêtes SPARQL en présence de contraintes ShEx.Dans la seconde partie de nos contributions, nous proposons une méthode d’analyse pour optimiser l’évaluation de requêtes SPARQL groupées, sur des graphes RDF, en tirant avantage des contraintes ShEx. Notre optimisation s’appuie sur le calcul et l’assignation de rangs aux triple patterns d’une requête, permettant de déterminer leur ordre d’exécution. La présence de jointures intermédiaires entre ces patterns est la raison pour laquelle l’ordonnancement est important pour gagner en efficicacité. Nous définissons un ensemble de schémas ShEx bien- formulés, qui possède d’intéressantes caractéristiques pour l’optimisation de requêtes SPARQL. Nous développons ensuite notre méthode d’optimisation par l’exploitation d’informations extraites d’un schéma ShEx. Enfin, nous rendons compte des résultats des évaluations effectuées, montrant les avantages de l’application de notre optimisation face à l’état de l’art des systèmes d’évaluation de requêtes. / Data structured in the Resource Description Framework (RDF) are increasingly available in large volumes. This leads to a major need and research interest in novel methods for query analysis and compilation for making the most of RDF data extraction. SPARQL is the widely used and well supported standard query language for RDF data. In parallel to query language evolutions, schema languages for expressing constraints on RDF datasets also evolve. Shape Expressions (ShEx) are increasingly used to validate RDF data, and to communicate expected graph patterns. Schemas in general are important for static analysis tasks such as query optimisation and containment. Our purpose is to investigate the means and methodologies for SPARQL query static analysis and optimisation in the presence of ShEx schema constraints.Our contribution is mainly divided into two parts. In the first part we consider the problem of SPARQL query containment in the presence of ShEx constraints. We propose a sound and complete procedure for the problem of containment with ShEx, considering several SPARQL fragments. Particularly our procedure considers OPTIONAL query patterns, that turns out to be an important feature to be studied with schemas. We provide complexity bounds for the containment problem with respect to the language fragments considered. We also propose alternative method for SPARQL query containment with ShEx by reduction into First Order Logic satisfiability, which allows for considering SPARQL fragment extension in comparison to the first method. This is the first work addressing SPARQL query containment in the presence of ShEx constraints.In the second part of our contribution we propose an analysis method to optimise the evaluation of conjunctive SPARQL queries, on RDF graphs, by taking advantage of ShEx constraints. The optimisation is based on computing and assigning ranks to query triple patterns, dictating their order of execution. The presence of intermediate joins between the query triple patterns is the reason why ordering is important in increasing efficiency. We define a set of well-formed ShEx schemas, that possess interesting characteristics for SPARQL query optimisation. We then develop our optimisation method by exploiting information extracted from a ShEx schema. We finally report on evaluation results performed showing the advantages of applying our optimisation on the top of an existing state-of-the-art query evaluation system.