Le test structurel est généralement limité aux test unitaires et basé sur une définition claire de la couverture du code. En particulier, le critère tous-les-chemins, qui requiert au moins un cas de test par chemin faisable, est reconnu comme offrant un haut niveau de confiance dans les test effectués. Ce document traite des difficultés de l'utilisation de ce type de test sur des fonctions composées d'appels à d'autres fonctions. Pour limiter l'explosion combinatoire du nombre de chemins résultant d'un traitement "inlining", nous choisissons d'abstraire les fonctions appelées par leurs spécifications. Nous incluons les informations fonctionnelles des fonctions appelées aux informations structurelles de la fonction appelante données sous forme de graphe de flot de contrôle. Cette représentation fonctionnelle et structurelle peut être vue comme une extension du CFG classique ce qui nous permet de définir de nouveaux critères de couverture assurant le maintien de la couverture complète de la fonction appelante tout en limitant au maximum le nombre de cas de test nécessaires.

Ce travail analyse les problèmes posés par l'administration des systèmes répartis. Il dégage un ensemble de services de base permettant la construction d'un ensemble complet de services d'administration. Il définit donc un noyau d'administration constitué d'un service étendue de gestion de la configuration, remplissant à la fois la spécification de la configuration, la gestion des modifications, et la gestion de l'audit. La spécification de la configuration permet de fournir une description de haut niveau des ressources du système. Cette spécification est décrite grâce à une extension du langage C++. L'extension est réalisée grâce à une bibliothèque de classes et un préprocesseur permettant la spécification des relations entre les différentes entités et celle des notifications qui pourront être émises pour signaler un changement de l'état d'une ressource. Nous proposons un protocole original de gestion des modifications de la configuration. Il permet au système d'accepter les changements structurels (retrait, ajout, connexion et déconnexion). L'algorithme proposé permet au système d'évoluer d'une configuration vers une autre sans mettre en cause la cohérence des applications qui s'exécutent sur le système, et ceci avec un coût très bas en terme de ralentissement observé

Cette thèse présente une extension du compilateur CompCert permettant de fournir des garanties formelles de préservation sémantique à des programmes auxquels CompCert n'en donne pas. CompCert est un compilateur pour le langage C vers différentes architectures qui fournit, en plus d'un exécutable compilé, des garanties formelles concernant le comportement du programme assembleur généré. En particulier, tout programme C ayant une sémantique définie selon le standard C est compilé en un programme assembleur équivalent, c'est-à-dire qui a la même sémantique. En revanche, ce théorème n'assure aucune garantie lorsque le programme source n'a pas de sémantique définie : on parle en C de comportement indéfini. Toutefois, des programmes C issus de réels projets largement utilisés contiennent des comportements indéfinis. Cette thèse détaille dans un premier temps un certain nombre d'exemples de programmes C qui déclenchent des comportements indéfinis. Nous argumentons que ces programmes devraient tout de même bénéficier du théorème de préservation sémantique de CompCert, d'abord parce qu'ils apparaissent dans de vrais projets et parce que leur utilisation des comportements indéfinis semble légitime. Dans ce but, nous proposons d'abord un modèle mémoire pour CompCert qui définit l'arithmétique arbitraire de pointeurs et la manipulation de données non initialisées, à l'aide d'un formalisme de valeurs symboliques qui capturent la sémantique d'opérations non définies dans le standard. Nous adaptons l'intégralité du modèle mémoire de CompCert avec ces valeurs symboliques, puis nous adaptons les sémantiques formelles de chacun des langages intermédiaires de CompCert. Nous montrons que ces sémantiques symboliques sont un raffinement des sémantiques existantes dans CompCert, et nous montrons par ailleurs que ces sémantiques capturent effectivement le comportement des programmes sus-cités. Enfin, afin d'obtenir des garanties similaires à celles que CompCert fournit, nous devons adapter les preuves de préservation sémantique à notre nouveau modèle. Pour ce faire, nous généralisons d'importantes techniques de preuves comme les injections mémoire, ce qui nous permet de transporter les preuves de CompCert sur nos nouvelles sémantiques. Nous obtenons ainsi un théorème de préservation sémantique qui traite plus de programmes C. / This thesis presents an extension of the CompCert compiler that aims at providing formal guarantees about the compilation of more programs than CompCert does. The CompCert compiler compiles C code into assembly code for various architectures and provides formal guarantees about the behaviour of the compiled assembly program. It states that whenever the C program has a defined semantics, the generated assembly program behaves similarly. However, the theorem does not provide any guarantee when the source program has undefined semantics, or, in C parlance, when it exhibits undefined behaviour, even though those behaviours actually happen in real-world code. This thesis exhibits a number of C idioms, that occur in real-life code and whose behaviour is undefined according to the C standard. Because they happen in real programs, our goal is to enhance the CompCert verified compiler so that it also provides formal guarantees for those programs. To that end, we propose a memory model for CompCert that makes pointer arithmetic and uninitialised data manipulation defined, introducing a notion of symbolic values that capture the meaning of otherwise undefined idioms. We adapt the whole memory model of CompCert with this new formalism and adapt the semantics of all the intermediate languages. We prove that our enhanced semantics subsumes that of CompCert. Moreover, we show that these symbolic semantics capture the behaviour of the previously undefined C idioms. The proof of semantic preservation from CompCert needs to be reworked to cope with our model. We therefore generalize important proof techniques such as memory injections, which enable us to port the whole proof of CompCert to our new memory model, therefore providing formal guarantees for more programs.

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 CTL. / The 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.

Le problème général de la preuve de propriétés de programmes impératifs est indécidable. Pour deslangages de programmation et de propriétés plus restrictifs, des sous-problèmes décidables sontconnus. En pratique, grâce à des heuristiques, les outils de preuve de programmes automatisent despreuves qui sortent du cadre théorique de ces sous-problèmes décidables connus. Nous illustronscette réussite pratique en construisant un catalogue de preuves, pour des programmes et despropriétés de nature similaire et de complexité croissante. Ces programmes sont principalementdes générateurs de cartes combinatoires.Ainsi, ce travail contribue aux domaines de recherche de la combinatoire énumérative et dugénie logiciel. Nous distribuons une bibliothèque C de générateurs exhaustifs bornés de tableauxstructurés, formellement spécifiés en ACSL et vérifiés avec le greffon WP de la plateforme d’analyseFrama-C. Nous proposons également une méthodologie de test qui facilite la preuve interactive enCoq, une étude formelle des cartes originale, et de nouveaux résultats en combinatoire énumérative. / The general problem of proving properties of imperative programs is undecidable. Some subproblems– restricting the languages of programs and properties – are known to be decidable. Inpractice, thanks to heuristics, program proving tools sometimes automate proofs for programs andproperties living outside of the theoretical framework of known decidability results. We illustrate thisfact by building a catalog of proofs, for similar programs and properties of increasing complexity. Mostof these programs are combinatorial map generators.Thus, this work contributes to the research fields of enumerative combinatorics and softwareengineering. We distribute a C library of bounded exhaustive generators of structured arrays, formallyspecified in ACSL and verified with the WP plugin of the Frama-C analysis platform. We also proposea testing-based methodology to assist interactive proof in Coq, an original formal study of maps, andnew results in enumerative combinatorics.