Architecture de sécurité décentralisée basée sur l'identification cryptographique.

  • By: Julien Laganier
  • Number: PhD2006-01
  • Date: March 2006
  • Abstract:

    This thesis studies the problem of securing large scale and dynamic communication, execution and storage infrastructures. The majority of existing security solutions relies on the existence of a global public key infrastructure. The deployment of such a global infrastructure is problematic at technical, administrative and political levels. In order to relieve solutions from this constraint, we propose a decentralized security approach based on cryptographic identifiers (CBID, CGA, HBA and HIP) and delegation (SPKI certificates). We show that this security approach fits better to the intrinsical decentralized nature of the large scale, shared and open systems like Internet or grid computing. To validate the approach, we instantiate it into several security solutions for existing protocols using the IP security (IPsec) and host identity (HIP) protocols. In particular, security solutions for the IPv6 (Internet Protocol version 6) network layer and its ND (Neighbor Discovery) component, as well as for virtualization of the execution, communication and storage infrastructure of grid computing (Supernet, HIPernet and Internet Backplane Protocol) are presented and analysed.
  • Abstract (in french):

    L'objectif de ce travail de thèse est d'étudier le problème de la sécurisation des infrastructures distribuées de communication, d'exécution ou de stockage, dynamiques et à très large échelle. La majorité des solutions de sécurité reposent sur l'existence d'infrastructures de clefs publiques globales, dont le déploiement soulève de nombreux problèmes, tant techniques qu'administratifs et politiques. Afin d'échapper à cette contrainte, nous proposons une approche de sécurité décentralisée basée sur l'identification cryptographique (CBID, CGA, HBA et HIP) et la délégation (certificats SPKI). Nous montrons qu'une telle approche de sécurité est plus adaptée à la nature intrinsèquement décentralisée de systèmes de grandes tailles, ouverts et partagés, tels que l'Internet ou les grilles de calculs. Pour valider cette approche, nous l'avons instanciée en nous appuyant sur les protocoles de sécurité pour IP (IPsec), et d'identification des hôtes (HIP - Host Identity Protocol). Nous montrons ainsi comment sont sécurisés différents protocoles réseaux. En particulier, des solutions de sécurité pour la couche réseau IPv6 (Internet Protocol version 6) et pour sa composante de découverte du voisinage ND (Neighbor Discovery), ainsi que pour virtualiser l'infrastructure d'exécution, de communication et de stockage des grilles de calcul (Supernet, HIPernet, Internet Backplane Protocol) sont présentées et analysées.
  • Keywords:

    security, decentralized, distributed, identification, cryptography, network, internet, infrastructure.
  • Keywords (in french):

    sécurité, décentralisé, distribué, identification, cryptographie, réseau, internet, infrastructure.
  • Availability: Electronic copy only.
  • Size: 127p
  • Format:compressed postscript
  • Get it

FLIP : Une bibliothèque virgule flottante pour processeurs entiers.

  • By: Saurabh-Kumar RAINA
  • Number: PhD2006-02
  • Date: September 2006
  • Abstract:

    Embedded systems are now ubiquitous in a wide range of diverse application domains. Because of cost and energy reasons most embedded systems rely on integer or fixed-point processors. Such systems confront with a problem while supporting the multimedia applications which depend on floating-point arithmetic due to high demands for accuracy. A straightaway solution might be to use a dedicated floating-point unit but it comes at the cost of extra silicon area and increased power consumption. The solutions existing in software consist of introducing some scaling operations in the target program, which becomes complicated due to wide range of floating-point numbers, or porting the programs meant for general-purpose processors to integer or fixed-point cores which is quite a complex task. In those cases, an efficient solution may be to use a fast floating-point emulation layer over the integer or fixed-point units. This thesis addresses the design and implementation issues involved in providing this software layer to support floating-point arithmetic on the ST200 family of VLIW integer processors from STMicroelectronics. This work discusses the possibilities of adequation and adaptation of specific algorithms to ST200 processors. It shows that the performance of a software implementation can be significantly improved through a sound understanding of a particular architecture, careful selection of an algorithm and a fine tuning of an implementation. FLIP, developed in a collaborative project funded by Région Rhône-Alpes and STMicroelectronics, supports basic floating-point operations (+, -, *, /, x0.5), additional operations (x2, x*y +- z, 1/x, 1/(x0.5)) with a fast implementation of division and square root and elementary functions (exp(x), log_2(x), sin(x), cos(x)). FLIP has achieved better performances in comparison to the original library which has already been optimized by STMicroelectronics. For complex operations like division and square root, FLIP is at least three times faster. A rewarding achievement for FLIP is that it has replaced the original library in the industrial compiler R4.1 for ST200 processors.
  • Abstract (in french):

    Aujourd'hui, les systèmes embarqués sont omniprésents dans de nombreuses applications. À cause de la vitesse et de la consommation d'énergie la plupart des processeurs dans les systèmes embarqués ont seulement des ressources matérielles de calcul entier (ou virgule fixe). Un grand nombre des applications en calcul scientifique et en traitement du signal utilisent l'arithmétique virgule flottante pour des raisons de précision. Donc, pour faire du calcul numérique sur les nombres flottants, soit on utilise des processeurs avec une couche flottante matérielle qui consomme beaucoup d'énergie, soit on fait une émulation logicielle de la couche flottante pour les processeurs entiers. Le travail de cette thèse concerne la conception et l'implantation de couches logicielles pour l'arithmétique virgule flottante sur les processeurs de la famille ST200 de STMicroelectronics. Le but de cette thèse, réalisée dans le cadre d'une collaboration avec STMicroelectronics et financée par la Région Rhône-Alpes, est de concevoir une bibliothèque pour les processeurs de la famille ST200. Ce travail présente les possibilités d'adéquation et d'adaptation des algorithmes spécifiques à ces processeurs. Il montre qu'une amélioration considérable de la performance peut être obtenue grâce à une bonne connaissance de l'architecture cible, un choix judicieux de l'algorithme à utiliser et un réglage minutieux de l'implantation. La bibliothèque FLIP est la concrétisation logicielle de cette thématique. Elle implante les cinq opérations de base (+, -, *, /, x0.5) en respectant la norme IEEE-754, des opérations supplémentaires comme x2, x*y +- z, 1/x, 1/(x0.5) avec une implantation rapide de la division et de la racine carrée, et quelques fonctions élémentaires (sin(x), cos(x), log_2(x), 2^x). FLIP a été comparée à la bibliothèque initiale déjà optimisée par STMicroelectronics; pour chaque opération FLIP a obtenu de meilleurs performances. Des gains d'au moins 40 % pour deux applications industrielles ont permis à FLIP de remplacer la bibliothèque initiale de STMicroelectronics dans la version R4.1 des compilateurs pour ST200.
  • Keywords:

    floating-point arithmetic, integer processors, floating-point addition, multiplication, division, square root, fused multiply-and-add, elementary functions.
  • Keywords (in french):

    arithmétique flottante, processeurs entiers, addition, multiplication, division et racine carrée, multiplication addition fusionnées, fonctions élémentaires.
  • Availability: Electronic copy only.
  • Size: 157p
  • Format:Portable Document Format
  • Get it

Rotations discrètes et automates cellulaires.

  • By: Bertrand NOUVEL
  • Number: PhD2006-03
  • Date: September 2006
  • Abstract:

    In a discrete space, such as the set of integer-coordinate points, the modelization of isotropy may lead to noticeable theoretical difficulties. At this time, we do not know any gerometric theory on $\ZZ^n$ that would be suitable to describe the isotropy the same way it is perceived by Euclidean geometry. With respect to this problematic, our aim is to describe some algorithms that would give to the discrete rotations some properties that would be similar to the properties of the Euclidean rotation. Also, we expect these algorithm to work using integer arithmetic only.
    We start by proving the non-existence of transitive discrete rotation on $\ZZ^2$. This motivates the introduction of an encoding of the discrete rotation. We can establish the existence of connections in-between these configurations, bidimensional dynamical systems, and cellular automatas. A local analysis of the discrete rotations is then initiated. This research comprises the intersection of discrete geometry and symbolic dynamic. The pertinence of the encoding the rotations is justified by the existence of planar tranduscer that are able to compute one configuration according the other one by performing the encoded rotation.
    In order to describe the configurations in the framework of dynamical system we extend usual symbolical dynamic contepts to dimension 2. For the discretized rotations, the associated symbolic dynamic is conjugated with a set of two orthogonal translations on a bidimensional torus. Out analysis will hilight the fact that the configurations can be computed as a superposition of low-complexity configurations. Our work is also evocating some planar generalizations of sturmian words that have been studied, among others, by Valerie Berthé and Laurent Vuillon. Similar results exist for the 3-shear rotations.
    The analysis of discrete rotations by the symbolic dynamic system theory then leads to various results : quasiperiodicity of all configurations, possibility to compute the frequency associated to each symbol, caracterisation of bijective discretized rotation... This last result is also a the converse of a \'Eric Andrès et Marie-Andrée Jacob Theorem on discrete rotations.
    We have also studied the the discontinuities angles. We specify the angles for which they occur, as well as the nature of the transformation that happens.
    Combinating the remarks that are relative to the way discrete rotations proceed, we have described two algorithms : the first algorithm computes a rotation without doing any floating point arithmetic, nor computing any sine nor cosine; the order of complexity of this algorithm is optimal. The second algorithm is an implementation of the $3$-shear rotation on cellular automatas. Other possibilities to construct algorithms for rotations are enclosed within our dissertation.
    Moreover, we also have some interest in the quest for planar substitutions that are able to generate the rotation configurations. For quadratic angles, we have shown the rotations configurations are actually a weaving of interlaced autosimilar configurations. Also, we have introduced the scheme of an approach based on Rauzy graphs to infer planar subsitutions. By combination of these two approaches, we have hilighted the essential elements that are required to prove the autosimilarity of the configuration $C_{\pi/4}$.
    The potential applications of this research deal with the implementation of rotation algorithm within graphic processors. It also contributes to the study of the algorithmic methods for the physical modelization of isotropic phenemena in discrete spaces.
  • Abstract (in french):

    Dans un espace discret, comme l'ensemble des points à coordonnées entières, la modélisation de l'isotropie pose des difficultés théoriques notables. \`A ce jour, aucune théorie géométrique sur $\ZZ^n$ n'est apte à rendre compte de l'isotropie telle qu'elle est décrite par la géométrie euclidienne. Dans l'optique de contribuer à cette problématique, nous nous intéressons à la conception d'algorithmes capables de donner aux rotations discrètes des propriétés proches de celles de la rotation euclidienne. Ces algorithmes doivent de plus fonctionner à base d'arithmétique entière.
    Après avoir montré la non-existence de rotation discrète transitive sur $\ZZ^n$, nous introduisons un codage de rotations discrètes que nous relions à la fois à la dynamique symbolique et aux automates cellulaires. Il s'agit alors de mener une étude locale des rotations discrètes. Cette étude se situe au carrefour entre géométrie discrète et systèmes dynamiques symboliques. La pertinence des configurations obtenues est justifiée par l'existence de transducteurs planaires capables d'effectuer des rotations à partir des configurations.
    Ensuite, afin de réinterpréter ces configurations dans le cadre de la théorie des systèmes dynamiques, nous étendons des notions classiques de cette théorie à la dimension 2. Pour la rotation discrétisée, la dynamique symbolique associée est conjuguée avec un jeu de deux translations orthogonales sur un tore bidimensionnel. Après analyse, nous constatons que les configurations obtenues sont des superpositions de configurations de faible complexité. Cela évoque alors les généralisations planaires des mots sturmiens étudiées entre autres par Valérie Berthé et Laurent Vuillon. Des résultats analogues sont aussi obtenus pour les rotations $3$-transvections.
    L'analyse les rotations discrètes par le biais de systèmes dynamiques a permis de nombreux résultats : mise en évidence de la quasipériodicité des configurations, calcul de la fréquence des symboles, caractérisation des rotations discrétisées bijectives, ce qui est aussi la réciproque du théorème d'\'Eric Andrès et Marie-Andrée Jacob.
    Nous avons aussi étudié les discontinuités du processus de rotation. Ces discontinuités ont lieu pour des angles issus d'un sous-ensemble des angles quadratiques (i.e. les angles charnières).
    En combinant ces remarques, nous aboutissons à deux algorithmes. Le premier algorithme réalise des rotations sans faire aucun calcul à virgule flottante et sans calculer aucun sinus ni aucun cosinus. Il fonctionne de manière incrémentale et en ordre de complexité optimal. Le second algorithme est une implémentation de la rotation $3$-transvections sur automates cellulaires. D'autres pistes pour la conception d'algorithmes sont mentionnées dans la thèse.
    En outre, nous nous intéressons aussi aux méthodes substitutives qui engendrent les configurations de rotations. Pour les angles quadratiques, nous montrons que les configurations de rotations sont des entrelacements de configurations autosimilaires; et nous présentons le schéma d'une approche basée sur les graphes de Rauzy pour l'inférence de substitutions planaires. En combinant ces deux approches, nous mettons en avant les éléments essentiels de la démonstration de l'autosimilarité de $C_{\pi/4}$.
    Les applications potentielles de cette thèse concernent à terme l'implémentation d'algorithmes de rotations pour processeurs graphiques. Elle contribue aussi à l'étude des méthodes algorithmiques pour la modélisation physique en milieu discret de phénomènes isotropes.
  • Keywords:

    digital geometry, isotropy, rotations, cellular automatas, generalized substitutions, Rauzy graphs.
  • Keywords (in french):

    géométrie discrète, isotropie, rotations, automates cellulaires, substitutions généralisées, graphes de Rauzy.
  • Availability: Electronic copy only.
  • Size: 231p
  • Format:Portable Document Format
  • Get it

Automatic Deployment for Application Service Provider Environments.

  • By: Pushpinder Kaur Chouhan
  • Number: PhD2006-04
  • Date: September 2006
  • Abstract:

    The main objective of the thesis is to improve the performance of a NES environment so as to use these environments efficiently. Here efficiency means the maximum number of completed requests that can be treated in a time step by these environments. The very first problem which comes to picture is related to the applications scheduling on the selected servers. We have proposed algorithms for the scheduling of the sequential tasks on an NES environment. Experimentally we proved that the deadline scheduling with priority along with fallback mechanism can increase the overall number of tasks executed by the NES. Another important factor that influence the efficiency of the NES environments is the mapping style of the environment's components on the available resources. The questions such as ``which resources should be used?'', ``how many resources should be used?'' and ``should the fastest and connected resource be used for middleware or as a computational resource?'' remained unanswered. In this thesis we gave the solutions to these questions. We have shown theoretically that the optimal deployment on cluster is a Complete Spanning d-ary (CSD) tree. Considering heterogeneous resources we presented a deployment heuristic, as finding the best deployment among heterogeneous resources is amounts to find the best broadcast tree on a general graph, which is known to be NP-complete. Finally, we gave a mathematical model that can analyze an existing deployment and can improve the performance of the deployment by finding and then removing the bottlenecks. This is an heuristic approach for improving deployments of NES environments that has been defined by other means. Deployment planning algorithms and heuristic presented in thesis are validated by implementing them to deploy a hierarchical middleware DIET, on different sites of Grid’5000, a set of distributed computational resources in France.
  • Abstract (in french):

    L'objectif principal de cette thèse vise l'amélioration de l'utilisation des NES afin d'employer ces environnements de façon efficace. Le premier problème illustrant l'utilisation des NES est lié aux applications utilisant des serveurs dédiés. Nous avons montré expérimentalement l'impact positif en terme de charge globale d'un ordonnanceur combinant échéances d'exécution et un mécanisme de priorité. Cette première étude sur l'ordonnancement nous a conduit à nous intéresser à un autre facteur important lié à l'efficacité des NES, le déploiement des composants de l'environnement sur les ressources disponibles. Dans le cadre de NES hiérarchique nous avons notamment démontré que le déploiement optimal dans un cadre homogène est un Complete Spanning d-ary arbre. Dans le cas de ressources hétérogènes, le problème étant NP-complet, nous fournissons des heuristiques visant à fournir le meilleur arbre de diffusion des requêtes. Nous proposons un modèle mathématique afin d'analyser un déploiement existant et d'améliorer ce dernier par détection des goulots d'étranglement. Les algorithmes et heuristiques présentés dans cette thèse ont été validés expérimentalement en utilisant l'intergiciel DIET sur la plate-forme Grid'5000.
  • Keywords:

    Deployment, Network Enabled Server, Application Service Provider, Grid Computing, Grid Middleware.
  • Availability: Not available.
  • Size: 161p
  • Format:Portable Document Format

Ordonnancement et réplication de données bioinformatiques dans un contexte de grille de calcul.

  • By: Antoine VERNOIS
  • Number: PhD2006-05
  • Date: October 2006
  • Abstract:

    In this thesis, we focus on the specific context of a set of bioinformatic applications. Those applications have the particularity to use wellknown read-only databanks and a computation cost linear with the size of data. The other point is that the use of application and data is always the same. Within this context, we have developped an algorithm (Scheduling and Replication Algorithm, SRA) that combines data management and scheduling using steady-state approach. Using a model of the platform, the number of requests as well as their distribution, the number and size of databanks, we define a linear program to satisfy ball the constraints at every level of the platform in steady-state. The solution of this linear program will give us a placement for the databanks on the servers as well as providing, for each kind of job, the server on which they should be executed. With the OptorSim grid simulator, that we have merely improved, we have show good result when storage space or network bandwidth between grid nodes are critical resources. Then, we have design a set of heuristics that aims to adapt the scheduling and data placement when data use changes. These heuristics have also been tested with our version of OptorSim. The conclusion of these simulations is that, in most cases, our algorithm is able to keep an almost optimal use of computation resources even if usage scheme used for initial data placement are very different of the request that are really submitted. Finally, we have implemented a prototype of our static solution inside the DIET grid middleware. This prototype has been deployed on the Grid'5000 platform. The run of experiments in these real conditions has validated results of our simulations.
  • Abstract (in french):

    Au cours de cette thèse, nous nous sommes placés dans le contexte bien > particulier d'une catégorie d'applications bioinformatiques dont les > caractéristiques sont d'utiliser des banques de données de références en > lecture seule et d'avoir un coût en temps de calcul affine en la taille des > données. Une autre caractéristique concernant l'utilisation de ces > applications est que leur schéma d'utilisation reste constant dans le > temps. Dans ce cadre, nous avons défini un algorithme basé sur un programme > linéaire permettant de calculer un ordonnancement et un placement statique > des données optimisant le rendement d'une plate-forme de type grille de > calcul. Grâce au simulateur Optorsim que nous avons largement modifié, nous > avons montré les bons résultats de notre algorithme lorsque l'espace de > stockage sur les noeuds de calcul ou le débit du réseau connectant les > différents sites sont des points critiques. > Nous avons ensuite établi un ensemble d'heuristiques dont le but est de > palier à d'éventuels changements dans les schémas d'utilisation des banques > de données. Là encore, nous avons utilisé Optorsim pour montrer et > comprendre l'impact de ces différentes heuristiques. Il en découle que dans > la plupart des cas, nous sommes en mesure de conserver une utilisation > presque optimale de la plate-forme, même lorsque les requêtes qui arrivent > sont très différentes du schéma d'utilisation utilisé pour le placement > initial. Enfin, nous avons réalisé un prototype du système basé sur > l'ordonnancement et le placement statique au sein de l'intergiciel de > grille DIET. Ce prototype, déployé sur un ensemble de noeuds de la > plate-forme Grid 5000, nous a permis de montrer l'efficacité de notre > méthode dans un environnement réel.
    Keywords:

    Scheduling, data management, grid computing, steady state.
  • Keywords (in french):

    Ordonnancement, gestion de > données, grille de calcul, régime permanent.
  • Availability: Electronic copy only.
  • Size: 127p
  • Format:Portable Document Format
  • Get it

Communications collectives et ordonnancement en régime permanent sur plates-formes hétérogènes.

  • By: Loris MARCHAL
  • Number: PhD2006-06
  • Date: October 2006
  • Abstract:

    The results presented in this document concern scheduling for large-scale heterogeneous platforms. We mainly focus on collective communications taking place during the execution of distributed applications: broadcast, scatter or reduction of data for instance. We study the steady-state operation of these communications and we aim at maximizing the throughput of a series of similar communications. The goal is also to obtain an asymptotically optimal schedule for makespan minimization. We present a general framework to study these communications, which we use to assess that the complexity of the problem is polynomial for most of the collective communications. For a particular model of communication, the bidirectional one-port model, we propose a practical method for solving the problem, which is applied to the broadcast, scatter and reduce operations. This method allows us to build an optimal solution by the resolution of a linear program of size polynomial in rational numbers. However, we prove that the optimization problem remains NP-hard for some communication schemes, like the multicast. These results are illustrated by simulations and real experiments conducted on the Grid5000 platform. Then, we extend our study of the steady-state operation to the scheduling of Grid applications. We first study how to execute multiple applications with centralized and decentralized schedulers on tree-shaped master-slave platforms. We also propose a new realistic model for hierarchical grid platforms, which we use to schedule divisible applications.
  • Keywords:

    Parallel algorithms, scheduling, heterogeneity, steady-state, collective communications, combinatorial optimization.
  • Abstract (in french):

    Les travaux présentés dans cette thèse concernent l'ordonnancement pour les plates-formes hétérogènes à grande échelle. Nous nous intéressons principalement aux opérations de communications collectives qui interviennent lors de l'exécution d'applications distribuées: diffusion de données, distribution de données, réduction, etc. Nous étudions ces problèmes dans le cadre de leur régime permanent, en optimisant le débit d'une série d'opérations de communications, en vue d'obtenir un ordonnancement asymptotiquement optimal du point de vue du temps d'exécution total. Nous présentons un cadre général pour l'étude de ces opérations, qui nous permet d'établir que la complexité du problème est polynomiale pour la plupart des opérations de communications collectives. Pour un modèle de communication particulier, le modèle un-port bidirectionnel, nous proposons une méthode de résolution pratique que nous appliquons à la diffusion, la distribution et la réduction. Elle permet de trouver une solution optimale en utilisant un programme linéaire de taille polynomiale en nombre rationnels. Nous montrons cependant que certains problèmes de communication demeurent NP-complets pour l'optimisation du régime permanent, comme la diffusion partielle (multicast) et le calcul de prefixes parallèles. Ces résultats sont illustrés à l'aide de simulations et d'expérimentations sur la grille Grid5000. Par la suite, nous avons orienté notre étude du régime permanent vers l'ordonnancement d'applications sur la grille. Nous avons proposé des ordonnanceurs centralisés et décentralisés pour des applications consistant en un ou plusieurs ensembles de tâches indépendantes sur une plate-forme maître-esclaves organisée en arbre. Nous avons également proposé une modélisation réaliste de grilles de calcul, que nous avons utilisé pour concevoir des stratégies d'ordonnancement pour des applications divisibles.
    Keywords (in french):

    Algorithmique parallèle, ordonnancement, hétérogénéité, régime permanent, communications collectives, optimisation combinatoire.
  • Availability: Electronic copy only.
  • Size: 231p
  • Format:Portable Document Format
  • Get it

De l'arithmétique d'intervalles à la certification de programmes.

  • By: Guillaume MELQUIOND
  • Number: PhD2006-07
  • Date: October 2006
  • Abstract:

    Computer numbers are usually limited, both in range and in precision. As a consequence, a careful certification has to be performed for applications that compute with these sets of numbers. Unfortunately, performing such a certification by hand is error-prone. Formal methods can ensure that the certification is correct, but making use of them is usually long and tedious, even for experts.
    This thesis aims at improving the availability of these methods to developers by automatizing their implementation. The key concepts are the use of interval arithmetic, a database of theorems on computer arithmetics, and a system for rewriting expressions in order to compute tight bounds on rounding errors.
    This approach has led to the development of the Gappa tool. It is designed to verify the numeric properties of programs relying on floating-point or fixed-point arithmetic. When verifying these properties, the tool also generates formal proofs of their correctness. These proofs can later be mechanically checked by the Coq proof assistant. Gappa has been successfully used for certifying some functions of the CRlibm, CGAL, and FLIP libraries, among others.
  • Abstract (in french):

    Parce que les nombres manipulés en machine ont généralement un domaine et une précision limités, il est nécessaire de certifier soigneusement que les applications les utilisant se comportent correctement. Réaliser une telle certification à la main est cependant un travail propice à de nombreuses erreurs. Les méthodes formelles permettent de garantir l'absence de ces erreurs, mais le processus de certification est alors long, fastidieux et généralement réservé à des spécialistes.
    Le travail effectué au cours de cette thèse vise à rendre ces méthodes accessibles en automatisant leur application. L'approche adoptée s'appuie sur une arithmétique d'intervalles accompagnée d'une base de théorèmes sur les propriétés des arithmétiques approchées et d'un mécanisme de réécriture d'expressions permettant le calcul de bornes fines sur les erreurs d'arrondi.
    Ce travail s'est concrétisé par le développement de l'outil Gappa d'aide à la certification. Il permet de vérifier les propriétés de codes numériques qui utilisent de l'arithmétique à virgule fixe ou à virgule flottante. Cette vérification s'accompagne de la génération d'une preuve formelle de ces propriétés utilisable par l'assistant de preuves Coq. Gappa a été utilisé avec succès pour certifier la correction de fonctions dans les bibliothèques CRlibm, CGAL et FLIP par exemple.
  • Keywords:

    program certification, floating-point arithmetic, fixed-point arithmetic, interval arithmetic, formal methods, Coq proof assistant.
  • Keywords (in french):

    certification de programmes, arithmétique à virgule flottante, arithmétique à virgule fixe, arithmétique d'intervalles, méthodes formelles, assistant de preuve Coq.
  • Availability: Electronic copy only.
  • Size: 231p
  • Format:Portable Document Format
  • Get it

Automates cellulaires : temps réel et voisinages.

  • By: Victor POUPET
  • Number: PhD2006-08
  • Date: December 2006
  • Abstract:

    In this thesis we have worked on the impact of the choice of a neighborhood on the algorithmic abilities of cellular automata. We have specifically studied the lower complexity classes such as the real time (that corresponds to the shortest time necessary for a cellular automaton to read all the letters of the input word) and the real time plus a constant. It is indeed known that neighborhoods are equivalent in linear time and it is therefore necessary to consider shorter times.
    We have obtained neighborhood equivalence results with respect to the real time (neighborhood classes such that cellular automata working on any of those neighborhoods can recognize the same languages in real time) and linear or constant speed-up theorems for many classes of neighborhoods.
  • Abstract (in french):

    Dans cette thèse nous nous sommes intéressés à l'importance du choix du voisinage sur les capacités algorithmiques des automates cellulaires. Nous avons travaillé en dimension quelconque en nous concentrant sur les classes de complexité correspondant au temps réel (plus petit temps nécessaire pour que l'automate ait lu le mot en entrée) et temps réel plus une constante. En effet il est connu que les voisinages sont équivalents en temps linéaire et il est donc nécessaire de considérer des temps inférieurs.
    Nous avons obtenu plusieurs résultats d'équivalences de voisinages au sens du temps réel (des classes de voisinages tels que les automates fonctionnant sur ces voisinages reconnaissent les mêmes langages) et des résultats d'accélérations linéaires ou constantes selon les voisinages.
  • Keywords:

    Cellular automata, neighborhoods, language recognition, real time, convex hull, constant speed-up, linear speed-up.
  • Keywords (in french):

    Automates cellulaires, voisinages, reconnaissance de langages, dimension quelconque, temps réel, enveloppe convexe, accélération constante, accélération linéaire.
  • Availability: Electronic copy only.
  • Size: 158p
  • Format:Portable Document Format
  • Get it

Analyses statistiques des communications sur puce.

  • By: Antoine SCHERRER
  • Number: PhD2006-09
  • Date: December 2006
  • Abstract:

    This PhD is composed of two main parts. The first one focuses on Internet traffic modelling. From the analysis of many traffic traces, we have proposed a parsimonious model (Gamma-Farima) adapted to aggregated throughput traces and valid for wide range of aggregation levels. In order to produce synthetic traffic from this model, we have also studied the generation of sample path of non-gaussian and long memory stochastic processes. We have then used the Gamma-Farima model in order to build an anomaly detection method. To this end we have introduced a multiresolution model that can differentiate a regular traffic from a malicious one (including a DDoS attack). This method was evaluated both on real traces and simulations. Finally, we have studied the production of long range dependent traffic in a network simulator (NS-2). The second part of this PhD deals with the analysis and synthesis of on-chip traffic, i.e. the traffic occurring in a system on chip. In such systems, the introduction of networks on chip (NoC) has brought the interconnection system on top of the design flow. In order to prototype these NoC rapidly, fast simulations need to be done, and replacing the components by traffic generators is a good way to achieve this purpose. So, we have set up and developed a complete and flexible on-chip traffic generation environment that is able to replay a previously recorded trace, to generate a random load on the network, to produce a stochastic traffic fitted to a reference trace and to take into account traffic phases. Indeed most of the traffic traces we have obtained were non-stationary, we therefore need to split them into reasonably stationary parts in order to perform a meaningful stochastic fit. We have performed many experiments in the SocLib simulation environment that demonstrate that i) our traffic generation procedure is correct, ii) our segmentation algorithm provides promising results and iii) multiphase stochastic traffic generation is a good tradeoff between replay and simple random traffic generation. Finally, we have investigated the presence of long memory in the trace as well as the impact of long memory on the NoC performance.
  • Abstract (in french):

    Cette thèse est composée de deux parties. La première explore la problématique de la modélisation de trafic Internet. Nous avons proposé, à partir de l'étude de nombreuses traces, un modèle basé sur des processus stochastiques non-gaussiens à longue mémoire (Gamma-Farima) permettant de modéliser de manière pertinente les traces de débit agrégé, et ce pour une large gamme de niveau d'agrégation. Afin de pouvoir générer du trafic synthétique, nous avons proposé une méthode de synthèse de tels processus. Nous avons ensuite, à partir du modèle Gamma-Farima, proposé un modèle multirésolution permettant de différencier un trafic régulier, d'un trafic contenant une attaque (de type déni de service distribuée). Ceci nous a permis de proposer une méthode de détection d'anomalie que nous avons évalué sur des traces réelles et en simulation. Enfin nous avons étudié expérimentalement le problème de la production de trafic à longue mémoire dans un simulateur de réseaux (NS-2). La deuxième partie traite la problématique de la génération de trafic au sein des systèmes sur puce (SoC). Dans ce domaine, l'arrivée de véritable réseaux sur puce place la conception de l'interconnexion au premier plan, et pour accélérer les simulations, il convient de remplacer les composants par des générateurs de trafic. Nous avons mis en place un environnement complet de génération de trafic sur puce permettant de rejouer une trace, de produire une charge aléatoire sur le réseau, de produire un trafic stochastique ajusté sur une trace de référence et de tenir compte des phases dans le trafic. Nous avons effectué de nombreuses simulations dans l'environnement de simulation de SoC académique SocLib qui nous ont permis de valider notre approche de la génération de trafic, d'évaluer notre algorithme de segmentation ainsi que la génération de trafic stochastique multiphase que nous avons introduite. Nous avons aussi exploré la présence de longue mémoire dans le trafic des processeurs sur puce, ainsi que l'impact de cette caractéristique sur les performances du réseau sur puce.
  • Keywords:

    Stochastic processes, traffic modelling, traffic synthesis, Internet traffic, systems-on-chip, networks-on-chip, long-range dependence, self-similarity.
  • Keywords (in french):

    Processus stochastiques, modélisation de trafic, synthèse de trafic, trafic Internet, systèmes sur puce, réseaux sur puce, trafic sur puce, longue mémoire, autosimilarité.
  • Availability: Electronic copy only.
  • Size: 204p
  • Format:Portable Document Format
  • Get it