Thèse de doctorat : Informatique : Nancy 1 : 2001. / Thèse : 2001NAN10123. Titre provenant de l'écran-titre.

Reproduction de : Thèse de doctorat : Systèmes informatiques : Toulouse, INPT : 2006. / Titre provenant de l'écran-titre. Bibliogr. 117 réf.

Thèse (M.Sc.)--Université Laval, 2008. / Titre de l'écran-titre (visionné le 25 mars 2009). Bibliogr.

Thèse (M.Sc.)--Université Laval, 2005. / Bibliogr.: f. [65]-66. Publié aussi en version électronique.

Les avancées technologiques des programmes de simulation et des ordinateurs commerciaux rendent la simulation en temps réel de procédés complexes plus accessible au public. La simulation en temps réel nous permet de ressentir les vraies dynamiques d'un modèle physique qui pourrait être trop difficile ou trop coûteux à réaliser en réalité. Le concept présenté, dans ce mémoire, porte sur l'utilisation de la simulation en temps réel pour réaliser des laboratoires virtuels interactifs et versatiles. En génie électrique, on pourrait prendre comme exemple les laboratoires de machines électriques où il est difficile en salle de classe de démontrer les dynamiques et les envergures des machines rencontrées dans l'industrie. Le laboratoire virtuel de ce cours serait une représentation complète de la table physique dans l'environnement de simulation, à la différence que l'on pourrait modifier les machines à volonté pour avoir par exemple des machines plus proches de la réalité industrielle. Dans un premier temps, les objectifs et contraintes des laboratoires d'enseignement sont présentés. On en déduira les objectifs que doivent remplir les laboratoires virtuels en temps réel. Ensuite, on introduira la conception de la structure que doit respecter le modèle de simulation pour permettre la réalisation d'un laboratoire "bac à sable". Une réflexion doit être apportée pour que le modèle permette à l'utilisateur de réaliser le maximum d'expériences différentes tout en restant intuitif. Des composants permettant d'atteindre les objectifs déterminés ont été développés. Ils ont été créés pour permettre leur modification durant la simulation, apportant ainsi une plus grande versatilité une fois la simulation créée. Enfin, l'étendue des possibilités que proposent les laboratoires virtuels en temps réels sera présentée. Des expériences seront réalisées sur deux laboratoires créés dans le cadre de ce mémoire. Le premier traite du cours d'électrotechnique fondamental, où divers essais sur les transformateurs et les charges passives peuvent être réalisés. Le deuxième porte sur un réseau d'usine où le démarrage des machines de grande puissance et leurs interactions sont présentés. / Technological advances in simulation programs and commercial computers make real-time simulation of complex processes more accessible to the general public. Real-time simulation allows us to experience the true dynamics of a physical model that might be too difficult or too expensive to realize in reality. The concept presented in this memoire focuses on the use of real-time simulation to create interactive and versatile virtual laboratories. In electrical engineering, we could take, as an example, the electrical machine laboratories where it is difficult in the classroom to demonstrate the dynamics and scale of machines encountered in the industry. The virtual lab in this course would be a complete representation of the physical workbench with in the simulation environment. With the difference that the machines could be modified at will, for example, to be closer to the reality of the industry. First, the objectives and constraints of the teaching laboratories are presented, from wich we will deduce the objectives that must be fulfilled by real-time virtual laboratories. Then, we will introduce the design of the structure that the simulation model must respect to allow the realization of a "sandbox" type laboratory. The model must allow to realize a maximum of different experiments while remaining intuitive. Components allowing to reach the determined objectives have been developed. They were created to allow their modification during the simulation, thus bringing a greater versatility once the simulation is created. Finally, the extent of the possibilities offered by real-time virtual laboratories will be presented. Experiments will be performed on two labs created for this memoire. The first deals with the fundamental electrical engineering course, where various tests on transformers and passive loads can be performed. The second deals with a factory grid where the starting of large machines and their interactions are presented.

Les avancées technologiques des programmes de simulation et des ordinateurs commerciaux rendent la simulation en temps réel de procédés complexes plus accessible au public. La simulation en temps réel nous permet de ressentir les vraies dynamiques d'un modèle physique qui pourrait être trop difficile ou trop coûteux à réaliser en réalité. Le concept présenté, dans ce mémoire, porte sur l'utilisation de la simulation en temps réel pour réaliser des laboratoires virtuels interactifs et versatiles. En génie électrique, on pourrait prendre comme exemple les laboratoires de machines électriques où il est difficile en salle de classe de démontrer les dynamiques et les envergures des machines rencontrées dans l'industrie. Le laboratoire virtuel de ce cours serait une représentation complète de la table physique dans l'environnement de simulation, à la différence que l'on pourrait modifier les machines à volonté pour avoir par exemple des machines plus proches de la réalité industrielle. Dans un premier temps, les objectifs et contraintes des laboratoires d'enseignement sont présentés. On en déduira les objectifs que doivent remplir les laboratoires virtuels en temps réel. Ensuite, on introduira la conception de la structure que doit respecter le modèle de simulation pour permettre la réalisation d'un laboratoire "bac à sable". Une réflexion doit être apportée pour que le modèle permette à l'utilisateur de réaliser le maximum d'expériences différentes tout en restant intuitif. Des composants permettant d'atteindre les objectifs déterminés ont été développés. Ils ont été créés pour permettre leur modification durant la simulation, apportant ainsi une plus grande versatilité une fois la simulation créée. Enfin, l'étendue des possibilités que proposent les laboratoires virtuels en temps réels sera présentée. Des expériences seront réalisées sur deux laboratoires créés dans le cadre de ce mémoire. Le premier traite du cours d'électrotechnique fondamental, où divers essais sur les transformateurs et les charges passives peuvent être réalisés. Le deuxième porte sur un réseau d'usine où le démarrage des machines de grande puissance et leurs interactions sont présentés. / Technological advances in simulation programs and commercial computers make real-time simulation of complex processes more accessible to the general public. Real-time simulation allows us to experience the true dynamics of a physical model that might be too difficult or too expensive to realize in reality.The concept presented in this memoire focuses on the use of real-time simulation to create interactive and versatile virtual laboratories. In electrical engineering, we could take, as an example, the electrical machine laboratories where it is di cult in the classroom to demonstrate the dynamics and scale of machines encountered in the industry. The virtual lab in this course would be a complete representation of the physical workbench with in the simulation environment. With the difference that the machines could be modified at will, for example, to be closer to the reality of the industry. First, the objectives and constraints of the teaching laboratories are presented, from wich we will deduce the objectives that must be fullled by real-time virtual laboratories.Then, we will introduce the design of the structure that the simulation model must respect to allow the realization of a "sandbox" type laboratory. The model must allow to realize a maximum of different experiments while remaining intuitive.Components allowing to reach the determined objectives have been developed. They were created toallow their modification during the simulation, thus bringing a greater versatility once the simulationis created.Finally, the extent of the possibilities oered by real-time virtual laboratories will be presented. Experiments will be performed on two labs created for this memoire. The firrst deals with the fundamental electrical engineering course, where various tests on transformers and passive loads can be performed. The second deals with a factory grid where the starting of large machines and their interactions are presented.

Une jeune femme qui cherche des souliers dans les ruelles et qui mémorise les pavillons à la poupe des cargos, un libraire qui collectionne les aquariums et un chien qui se prend pour un baron. D'abord isolés, les personnages de La ruelle aux aquariums développent une amitié aussi profonde qu'étrange. Jusque-là confinés à la marge, ils se rencontrent le temps de faire pour l'autre la cartographie de leurs mondes et d'effacer la frontière séparant la réalité rêche d'une imagination salutaire. En écrivant ce roman sur un ordinateur, une question s'est imposée: ±Qu'implique au juste l'utilisation de cet outil pour l'écrivain?¿. S'ouvrait alors une réflexion sur le romancier qui, composant une oeuvre à paraître sous forme imprimée, entretient une relation nouvelle avec son support d'écriture. Puisqu'il est question d'ordinateur, de brouillon et d'imprimé, la première section rappelle d'abord les principales transformations qu'ont subies les supports d'écriture et le brouillon à travers le temps du point de vue des informaticiens, des généticiens du texte et des historiens du livre. Avec l'écran comme vecteur d'une nouvelle relation entre le romancier et son texte, c'est ensuite la nature du ±brouillon numérique¿ qui apparaît. Mais ce brouillon, largement influencé par l'±image¿ iconique (Eco), comporte une ±friabilité¿ doublée d'une illusion contradictoire: à l'état de chantier, il prend souvent les allures d'un texte fini. C'est là le côté ±charlatan¿ du numérique. Pour capter cette ±image¿, la médiologie de Régis Debray a, dans un troisième temps, servi d'interface. Grâce au concept de médiasphère, le lien entre l'innovation technique et le roman est analysé dans une perspective diachronique, traçant du coup les contours de la période de transition dans laquelle nous nous trouvons. Appliquées à notre objet, les caractéristiques de cette période font émerger une nouvelle posture de l'écrivain à laquelle s'accrochent des ±rôles¿ transformés (romancier-lecteur, éditeur et imprimeur) dont l'impact est discuté. Enfin, la friabilité du brouillon est interrogée en regard de sa sauvegarde et de son archivage, le brouillon numérique destiné à l'impression impliquant plusieurs sauvegardes et un archivage qui peuvent poser problème.

Certains protocoles cryptographiques ont été développés spécifiquement pour assurer quelques propriétés de sécurité dans nos réseaux de communication. Dans le but de s'assurer qu'un protocole remplit ses propriétés de sécurité, des vérifications probabilistes y sont donc entreprises afin de confirmer s'il présente des failles lorsqu'on prend en compte leur comportement probabiliste. Nous avons voulu entreprendre une méthode probabiliste, mais aussi non-déterministe, de modélisation de protocoles afin de confirmer si cette méthode peut remplacer d'autres qui ont déjà été utilisées pour vérifier des failles sur des protocoles cryptographiques. Cela nous a motivé à envisager comme objectif de nos recherches scientifiques, des analyses quantitatives des possibilités de faille sur des protocoles cryptographiques. / Certain cryptographic protocols were specifically developed to provide some security properties in our networks of communication. For the purpose of assuring that a protocol fulfils its security properties, probabilistic model checkings are undertaken to confirm if it introduces a fault when its probabilistic behavior is considered. We wanted to use a probabilistic method (and also non-deterministic) of protocols modeling to confirm if this method may substitute others that were already used for checking faults in cryptographic protocols. It leads us to consider the objective of our scientific researches as: quantitative analysis of faults in cryptographic protocols.

Titre de l'écran-titre (visionné le 28 février 2024) / Avec l'avènement de la technologie de la chaîne de blocs, un nouveau type de contrat appelé contrat intelligent a émergé. Les contrats intelligents sont des programmes informatiques permettant de formaliser des accords contractuels complexes tout en assurant automatiquement le respect de ces accords sans l'aide d'intermédiaires de confiance. Aujourd'hui, ils gèrent des millions de dollars en jetons numériques et effectuent des tâches quotidiennes de processus métier. Compte tenu des énormes enjeux financiers, les pirates informatiques sont plus que jamais motivés à exploiter tout bogue dans les contrats intelligents ou l'infrastructure sous-jacente. Une grande prudence est donc requise avant le déploiement des contrats intelligents, d'autant plus qu'ils deviennent immuables (*pas de possibilité de les modifier*) une fois déployés sur la chaîne de blocs. Écrire des contrats intelligents sécurisés et fiables est une tâche ardue et les méthodes existantes de sécurisation des contrats intelligents reposent largement sur l'expérience du programmeur, laissant ainsi place à des erreurs de logique et d'inattention. Dans cette thèse, nous proposons une approche novatrice basée sur la réécriture de programmes pour renforcer la sécurité des contrats intelligents. Plus précisément, étant donné un contrat intelligent *S* et une politique de sécurité *ϕ*, nous dérivons un nouveau contrat intelligent *S'* à partir de *S* et de *ϕ* de telle sorte que *S′* satisfait la politique de sécurité *ϕ* et reste correct par rapport à *S*. Le contrat *S′* (*c'est-à-dire le contrat sécurisé*) est celui qui sera en fin de compte déployé sur la chaîne de blocs. L'approche présentée utilise l'algèbre SBPA$^\textup{*}_\textup{0,1}$ qui est une variante de BPA$^\textup{*}_\textup{0,1}$ (*Basic Process Algebra*) étendue avec des variables, des environnements et des conditions pour formaliser et résoudre le problème. Le problème de trouver la version sécuritaire *S′* à partir de *S* et de *ϕ* se transforme en un problème de résolution d'un système d'équations linéaires pour lequel nous savons déjà comment extraire la solution dans un temps polynomial. Cette recherche contribue à combler le fossé dans la sécurisation des contrats intelligents et ouvre la voie à une adoption plus large de cette technologie révolutionnaire. / With the advent of blockchain technology, a new type of contract called smart contract has emerged. Smart contracts are computer programs to formalize complex contractual agreements while automatically ensuring compliance with these agreements without the help of trusted intermediaries. Today, they manage millions of dollars in digital tokens and perform daily business process tasks. Given the huge financial stakes, hackers are more motivated than ever to exploit any bugs in smart contracts or the underlying infrastructure. Great caution is therefore required before deploying smart contracts, especially since they become immutable (*no possibility to modify them*) once deployed on the blockchain. Writing secure and reliable smart contracts is a daunting task and existing methods of securing smart contracts rely heavily on the experience of the programmer, leaving room for errors of logic and carelessness. In this thesis, we propose an innovative approach based on program rewriting to strengthen the security of smart contracts. Specifically, given a smart contract *S* and a security policy *ϕ*, we derive a new smart contract *S′* from *S* and *ϕ* such that *S′* satisfies the security policy *ϕ* and remains correct with respect to *S*. The *S′* contract (*i.e. the secure contract*) is the one that will ultimately be deployed on the blockchain. The presented approach uses the algebra SBPA$^\textup{*}_\textup{0,1}$ which is a variant of BPA$^\textup{*}_\textup{0,1}$ (*Basic Process Algebra*) extended with variables, environments and conditions to formalize and solve the problem. The problem of finding the secure version *S′* from *S* and *ϕ* turns into a problem of solving a system of linear equations for which we already know how to extract the solution in polynomial time. This research helps bridge the gap in securing smart contracts and paves the way for wider adoption of this game-changing technology.

Tableau d’honneur de la Faculté des études supérieures et postdoctorales, 2004-2005 / Dans les deux dernières décennies, l’Internet a apporté une nouvelle dimension aux communications. Il est maintenant possible de communiquer avec n’importe qui, n’importe où, n’importe quand et ce, en quelques secondes. Alors que certains systèmes de communication distribués, comme le courriel, le chat, . . . , sont plutôt informels et ne nécessitent aucune sécurité, d’autres comme l’échange d’informations militaires ou encore médicales, le commerce électronique, . . . , sont très formels et nécessitent de très hauts niveaux de sécurité. Pour atteindre les objectifs de sécurité voulus, les protocoles cryptographiques sont souvent utilisés. Cependant, la création et l’analyse de ces protocoles sont très difficiles. Certains protocoles ont été montrés incorrects plusieurs années après leur conception. Nous savons maintenant que les méthodes formelles sont le seul espoir pour avoir des protocoles parfaitement corrects. Ce travail est une contribution dans le domaine de l’analyse des protocoles cryptographiques de la façon suivante: • Une classification des méthodes formelles utilisées pour l’analyse des protocoles cryptographiques. • L’utilisation des systèmes d’inférence pour la mod´elisation des protocoles cryptographiques. • La définition d’une classe de systèmes d’inférence qui ont une theorie décidable. • La proposition d’une procédure de décision pour une grande classe de protocoles cryptographiques / In the last two decades, Internet brought a new dimension to communications. It is now possible to communicate with anyone, anywhere at anytime in few seconds. While some distributed communications, like e-mail, chat, . . . , are rather informal and require no security at all, others, like military or medical information exchange, electronic-commerce, . . . , are highly formal and require a quite strong security. To achieve security goals in distributed communications, it is common to use cryptographic protocols. However, the informal design and analysis of such protocols are error-prone. Some protocols were shown to be deficient many years after their conception. It is now well known that formal methods are the only hope of designing completely secure cryptographic protocols. This thesis is a contribution in the field of cryptographic protocols analysis in the following way: • A classification of the formal methods used in cryptographic protocols analysis. • The use of inference systems to model cryptographic protocols. • The definition of a class of theory-decidable inference systems. • The proposition of a decision procedure for a wide class of cryptographic protocols.