Dans les deux dernières décennies, le logiciel libre a pris un essor considérable. Des distributions qui au début comptaient une centaine de paquets, en ont maintenant des dizaines de milliers, tous de provenance très différente. Ceci engendre des problèmes pour la gestion de qualité. Les outils et procédures ne sont plus adaptés à la taille et la complexité des distributions d'aujourd'hui. Dans cette thèse, nous commençons par présenter une modélisation mathématique des points communs entre les différents types de distribution (Debian et RPM); notamment le concept des paquets et des relations qui existent entre eux: les dépendances et les conflits. Cette modélisation est en partie formalisé avec l'assistant de preuves Coq. Cette modélisation sera ensuite utilisée pour proposer des relations 'sémantiques', qui sont plus adaptés que les relations existantes pour repérer et corriger des erreurs dans les distributions. Nous présentons aussi des algorithmes pour calculer ces relations d'une façon efficace, et nous utiliserons Coq pour prouver formellement les théorèmes les plus importantes utilisées par ces algorithmes. Finalement, nous avons validé les algorithmes sur des distributions existantes. Nous présenterons une analyse de la structure des distributions qui est le résultat de cette validation, ainsi qu'une discussion de la phénomène du "petit monde" en rapport avec les distributions.

Le thème principal de cette recherche est d'étudier et développer des techniques pour la modélisation des systèmes où la sécurité est critique. Cette thèse est focalisé sur l'étape de la spécification du domaine où de tels systèmes vont fonctionner, et de sa validation. La contribution de cette thèse est double. D'abord, nous modélisons le domaine des transports terrestres, un bon candidat pour cette étude en raison de sa nature critique vis-à-vis de la sécurité, dans le cadre formel de B événementiel et proposent quelques directives pour cette activité. Ensuite, nous présentons une approche, basée sur les techniques de l'animation et des transformations, pour la validation par étapes des spécifications formelles.

Au-delà de la formidable évolution en termes de complexité du circuit électronique en soi, son adoption et sa diffusion ont connu, au fil des dernières années, une explosion dans un très grand nombre de domaines distincts. Un système sur puce peut incorporer une combinaison de composants aux fonctionnalités très différentes. S'assurer du bon fonctionnement de chaque composant, et du système complet, est une tâche primordiale et épineuse. Dans ce contexte, l'Assertion-Based Verification (ABV) a considérablement gagné en popularité ces dernières années : il s'agit d'une démarche de vérification où des propriétés logico-temporelles, exprimées dans des langages tels que PSL ou SVA, spécifient le comportement attendu du design. Alors que la plupart des solutions d'ABV existantes se limitent au niveau transfert de registres (RTL), la contribution décrite dans cette thèse s'efforce de résoudre un certain nombre de limitations et vise ainsi une solution mature pour le niveau transactionnel (TLM) de SystemC. Une technique efficace de construction de moniteurs de surveillance à partir de propriétés PSL est proposée : cette technique, inspirée d'une approche originale existante pour le niveau RTL, est ici adaptée à SystemC TLM. Une méthode spécifique de surveillance des actions de communication à haut niveau d'abstraction est également détaillée. Les possibilités offertes par la technique présentée sont significativement étendues en proposant, pour les propriétés écrites en langage PSL, à la fois un support formel et une mise en oeuvre pratique pour des variables auxiliaires globales et locales, qui constituent un élément essentiel lors des spécifications à haut niveau d'abstraction. Tous ces concepts sont également implémentés dans un outil prototype. Afin d'illustrer l'intérêt de la solution proposée, diverses expérimentations sont effectuées avec des designs aux dimensions et complexités différentes. Les résultats obtenus permettent de souligner le fait que la méthode de vérification dynamique suggérée reste applicable pour des designs de taille réaliste.

Nous présentons un ensemble de travaux sur l'intégration de méthodes formelles et l'analyse multifacette de systèmes logiciels. %deuxième partie Partant de l'idée que les différentes facettes d'un système doivent être étudiées et développées avec les formalismes et outils appropriés, nous avons exploré, suite à d'autres chercheurs, des pistes pour l'intégration de méthodes formelles utilisées pour spécifier, analyser ou développer des parties des systèmes. La nécessité de l'intégration est relative au besoin de l'interaction entre différentes parties d'un même système ou bien à l'appréhension globale des propriétés du système. Nous explicitons les principaux problèmes de l'intégration de méthodes formelles : l'hétérogénéité syntaxique, l'hétérogénétité sémantique et la variété des systèmes logiques de raisonnement. Nous proposons alors la notion de compatibilité relative à ces trois niveaux pour assurer l'intégration de méthodes. L'idée principale est celle de l'interopérabilité sur une base sémantique (base d'intégration) ) sans laquelle aucun raisonnement n'est possible entre des parties assemblées d'un système. Les raisonnements formels sont alors effectués par plongement (embedding) des spécifications dans des logiques appropriées. Ce premier cadre est généralisé à des domaines de compatibilité plus larges que les bases d'intégration, et qui permettent de s'affranchir des langages et de travailler au niveau des paradigmes sous-jacents aux langages ; on obtient ainsi un cadre pour une intégration générique. Nous avons montré comment les formalismes intégrés existants tels que LOTOS, CSP-B, Circus rentrent dans ce cadre et nous avons mis en oeuvre ces idées pour de nouvelles intégrations par exemple B et les réseaux de Pétri. Dans une autre partie des travaux, nous présentons des extensions proposées autour de la méthode B, notamment la composition parallèle asynchrone de systèmes abstraits B à la manière de la composition parallèle dans les algèbres de processus. Notre proposition permet de combiner dans un même projet de développement formel la démarche descendante de la méthode B par une approche ascendante. Nous présentons ensuite une méthode de construction systématique de spécifications B pour des systèmes multi-processus à architecture dynamique. Ces travaux généralisent les précédents sur la composition de systèmes abstraits en définissant un opérateur de fusion de sous-systèmes qui est plus général que les opérateurs de composition parallèle. Une partie des travaux est consacrée à l'analyse multifacette de système ; notre proposition consiste à assurer la compatibilité des analyses des différentes facettes en partant non pas de modèles indépendants mais de modèles spécifiques dérivés à partir d'un modèle de référence qui permet d'assurer la cohésion globale de l'analyse. Cette approche est poursuivie par des expérimentations sur la combinaison de prouveurs et d'évaluateurs de modèles (model-checkers). Nous avons exploré d'autres voies pour l'analyse multifacette : élaborer une algèbre de spécifications multiparadigmes, ou différents aspects, relatifs aux facettes envisagées, peuvent être introduits dans une même unité de spécification. Les unités de spécification sont ensuite composées à l'aide des opérateurs de l'algèbre. Le lien est fait entre cette approche et celle de l'intégration de méthodes par plongement dans des logiques formelles. Une plateforme expérimentale est développée conjointement à ces travaux et relie les deux approches : elle permettra à terme de traduire, moyennant la compatibilité sémantique, différents formalismes d'entrées dans des formalismes cibles en passant par un modèle de référence ou pivot qui lui même est une spécification multiparadigme.

Actuellement, les applications interactives sont utilisées dans de nombreux domaines (guichets automatiques, tours de contrôle...), par des publics très différents (enfants, experts, handicapés...) et par un nombre important d'utilisateurs (interfaces de téléphones portables...) ou au contraire très spécifiques (logiciels conçus spécifiquement pour une entreprise). Elles sont de ce fait très diverses. De par la multiplicité des paramètres à prendre en compte, la conception et le développement des applications interactives sont devenus très coûteux. Afin de réduire ces coûts, des recherches sont actuellement menées sur le processus de conception. Cette thèse s'inscrit dans ces travaux. L'un des axes étudiés pour réduire le coût de production des applications interactives est la détection des erreurs le plus en amont possible pendant le processus de conception. Nous proposons de faciliter la vérification et la validation de la dynamique des applications (plus spécifiquement dénommée dialogue) tout au long de la conception, en fonction des spécifications recueillies auprès des futurs utilisateurs, exprimés sous forme de modèles de tâches. Les modèles de dialogue et les modèles de tâches représentent deux points de vue différents et complémentaires pour une même application. Nous proposons une approche de vérification de cohérence entre ces deux modèles tout au long du cycle de vie de l'application. Pour cela, nous avons défini des règles de cohérence entre les modèles que nous vérifions formellement en utilisant une méta-modélisation des formalismes que nous avons choisis après évaluation de leur utilisation pour une conception centrée-utilisateur.

<p>Les travaux présentés portent sur l'étude de méthodes de vérification paramétrée des systèmes temps réels. La motivation pour ces recherches est de proposer des méthodes formelles à appliquer sur des systèmes dont les spécifications ne sont pas encore complètes. Des paramètres sont donc introduits dans les modèles utilisés afin de donner des degrés de liberté à la modélisation. Le but est alors de guider la conception du système en déterminant des valeurs satisfaisantes pour les paramètres.</p> <p>Nous nous sommes focalisé sur les paramètres temporels qui sont en général parmi les plus complexes à définir. Nous avons ainsi défini le modèle des réseaux de Petri à chronomètres paramétrés.</p> <p>Dans une première approche, nous étendons les méthodes d'analyse classiquement utilisées dans les réseaux de Petri temporels. L'espace d'états du modèle paramétré est ainsi représenté par le graphe des classes d'états paramétrées. Cela nous permet de proposer des semi-algorithmes de model-checking paramétré avec lesquels nous vérifions des formules de logique TCTL paramétrées.</p> <p>Dans une seconde approche, nous étudions les méthodes qui préservent le parallélisme des réseaux de Petri. L'intérêt est de limiter l'explosion combinatoire qui apparaît lors de l'analyse de systèmes distribués, en particulier avec des modèles paramétrés. Nous proposons pour cela une méthode de dépliage temporel paramétré. Ce dépliage est a priori infini, mais nous proposons de l'utiliser pour résoudre un problème de supervision. La construction du dépliage est alors guidée par des observations finies, et nous extrayons les explications de ces observations, ainsi que les contraintes sur les paramètres qu'elles induisent.</p>

Malgré les progrès importants effectués en matière de conception de logiciels et l'existence de méthodes de développement éprouvées, il faut reconnaître que les défaillances de systèmes causées par des logiciels restent fréquentes. Il arrive même que ces défaillances concernent des logiciels critiques et provoquent des dommages significatifs. Considérant l'importance des intérêts en jeu, et le fait que la garantie de logiciel "zéro défaut" est hors d'atteinte, il est donc important de pouvoir déterminer en cas de dommages causés par des logiciels les responsabilités des différentes parties. Pour établir ces responsabilités, un certain nombre de conditions doivent être réunies: (1) on doit pouvoir disposer d'éléments de preuve fiables, (2) les comportements attendus des composants doivent avoir été définis préalablement et (3) les parties doivent avoir précisé leurs intentions en matière de répartition des responsabilités. Dans cette thèse, nous apportons des éléments de réponse à ces questions en proposant un cadre formel pour spécifier et établir les responsabilités en cas de dysfonctionnement d'un logiciel. Ce cadre formel peut être utilisé par les parties dans la phase de rédaction du contrat et pour concevoir l'architecture de logs du système. Notre première contribution est une méthode permettant d'intégrer les définitions formelles de responsabilité et d'éléments de preuves dans le contrat juridique. Les éléments de preuves sont fournis par une architecture de logs dite ''acceptable'' qui dépend des types de griefs considérés par les parties. La seconde contribution importante est la définition d'une procédure incrémentale, qui est mise en oeuvre dans l'outil LAPRO, pour l'analyse incrémentale de logs distribués.

Cette thèse est consacrée au problème de la vérification automatique des protocoles cryptographiques d'un point de vue logique et calculatoire.<br />Dans une première partie, nous abordons la sécurité des protocoles dans le cadre logique (formel). Nous montrons comment spécifier différentes propriétés de sécurité des protocoles (secret, authentification, <br />résistance aux attaques par dictionnaire) au moyen d'un langage de processus et comment les analyser de manière automatique pour un nombre borné de sessions.<br />La seconde partie traite de la justification cryptographique des modèles logiques. Nous nous intéressons ici à la notion d'équivalence statique, appliquée en particulier au chiffrement et aux données vulnérables aux attaques par dictionnaire (par ex. des mots de passe). Dans ce cadre, nous montrons que sous certaines conditions simples, toute preuve logique d'équivalence statique implique d'indistinguibilité cryptographique des données modélisées.

Le travail de la thèse porte sur la problématique de l'évolution des exigences et son analyse d'impact sur la sécurité. Au cours du développement des systèmes, les parties prenantes demandent l'application des évolutions, afin d'améliorer leurs fonctionnalités. L'occurrence d'une évolution affecte plusieurs aspects comme: la sécurité, le coût du développement et les délais. Lorsque le développement concerne un système complexe où le nombre des exigences est de l'ordre de dizaines de milliers, alors les demandes des évolutions rendent l'analyse d'impact du changement de plus en plus difficile. Malheureusement, la problématique de l'évolution des exigences n'est pas encore complètement résolue en milieu industriel. Notre étude est située dans le contexte d'ingénierie système et ingénierie des exigences, en intégrant des modèles formels et outils supports associés pour la vérification des propriétés de sécurité. La méthodologie est basée sur la norme industrielle de l'EIA-632 et sur le format VOLERE d'ingénierie des exigences en intégrant un modèle de traçabilité. De cette démarche ingénierie système, on a développé une méthodologie associée et un système d'information du processus de changement/évolution des exigences. Enfin, ce travail présente la méthodologie de la recherche d'impact lors de la demande de changement, et les outils qui supportent la méthodologie de la recherche d'impact, en se basant sur la méthode formelle (RAISE), qui nous permet d'analyser l'impact de l'évolution sur la sécurité.

L'analyse statique a pour but de vérifier qu'un programme a le comportement souhaité c.à.d. satisfait des propriétés de sûreté. Toutefois, inférer les propriétés vérifiées par un programme est un problème difficile : le théorème de Rice énonce que toute propriété non triviale d'un langage de programmation Turing-complet est indécidable. Afin de contourner cette difficulté, les analyses statiques effectuent des approximations des comportements possibles du programme. La théorie de l'interprétation abstraite permet de donner un cadre formel à ces approximations. Cette théorie, introduite par Cousot & Cousot propose un cadre d'approximation basé sur la notion de treillis, de connexion de Galois et de calculs de points fixes par itération. Ce cadre permet de définir la qualité des approximations effectuées et notamment la notion de meilleure approximation. À l'opposé, les notions quantitatives n'apparaissent pas naturellement dans ce cadre. Nous nous sommes donc posés la question de l'inférence, par analyse statique, de propriétés s'exprimant de manière quantitative (telles que l'utilisation de la mémoire ou le temps d'exécution).