Les systèmes de communication à distance entre les individus ont évolué significativement au cours des dernières années, de concert avec les innovations technologiques caractérisant notre société. Afin de réaliser une communication réaliste et intuitive, le système doit être capable de stimuler les sens qui sont habituellement impliqués dans l’interaction entre deux personnes, tels que l’ouïe, la vision et le toucher. Le téléphone a représenté une innovation importante dans les communications en permettant enfin de pouvoir parler avec son interlocuteur directement, sans devoir employer un signal codé comme le code Morse. Cette communication a été améliorée en introduisant les appels vidéo, lesquels permettent non seulement d’entendre l’interlocuteur mais aussi de le voir. Plusieurs recherches ont cependant démontré que le sens du toucher joue également un rôle très important dans les interactions entre individus. Une technologie relativement récente, connue comme technologie haptique, aborde le problème de la transmission du sens du toucher à distance, dans le but de mettre en oeuvre une communication complète et encore plus réaliste. Cette technologie a également d’autres applications tout aussi importantes. À titre d’exemple, l’haptique est utilisée dans le domaine de la réadaptation et de l’apprentissage guidé de personnes ayant des déficiences motrices. Cette thèse porte sur le développement de la technologie haptique pour la communication à distance entre deux individus. L’objectif final est la réalisation d’un système permettant aux deux utilisateurs de se serrer la main à distance. Afin d’atteindre cet objectif, nous devons aborder deux problèmes différents, tels que la conception d’une interface capable de reproduire le mouvement désiré et l’implémentation d’une loi de commande garantissant le comportement correct de cette interface. Toujours dans le cadre de l’interaction à distance par le biais d’un dispositif haptique, une interface pour l’apprentissage de l’écriture manuelle est également présentée. Cette application permet de démontrer, entre autres, l’importance d’un signal haptique dans l’interaction humain-humain et son influence sur les utilisateurs. / Remote communication systems have significantly improved in the course of the recent years, in concert with technological innovations of our society. In order to realize a realistic and intuitive communication, the system must activate the part of the sensory system that is normally stimulated in an interaction between two people, i.e., the auditory system, the visual system and the haptic perception system, which concerns touch. The telephone represented an innovating communication system. It allowed to directly talk to the interlocutor without any need for a coded signal such as the Morse code. Remote communications have been further improved with the introduction of the video calls, which allow people not only to talk to but also to see each other. Several researches proved that the sense of touch plays a crucial role in social interactions. Haptic technology, which is relatively recent, approaches the problems related to the perception and the transmission of touch. One objective is to render remote communications even more complete and realistic. Haptic technology is also used in other important applications such as, for instance, rehabilitation and guided learning process of people with movement impairments. This thesis concerns the development of the haptic technology devoted to the implementation of remote communication systems. The final objective is to realize a teleoperation system which allows two users to remotely shake hands. In order to achieve this objective, two main issues must be faced : the design of a haptic interface capable of reproducing the required movement and the implementation of a control law which guarantees the proper response of such an interface. In the framework of a remote interaction via a haptic device, an interface for the training and assessment of handwriting capabilities is also presented. The latter application demonstrates the importance of haptic signals in a remote human-human interaction and its influence on the users.

Est-il possible de démontrer un théorème prouvant que l’accès aux données confidentielles d’un utilisateur d’un service Web (tel que GMail) nécessite la connaissance de son mot de passe, en supposant certaines hypothèses sur ce qu’un attaquant est incapable de faire (par exemple, casser des primitives cryptographiques ou accéder directement aux bases de données de Google), sans toutefois le restreindre au point d’exclure des attaques possibles en pratique?Il existe plusieurs facteurs spécifiques aux protocoles du Web qui rendent impossible une application directe des méthodes et outils existants issus du domaine de l’analyse des protocoles cryptographiques.Tout d’abord, les capacités d’un attaquant sur le Web vont largement au-delà de la simple manipulation des messages échangés entre le client et le serveur sur le réseau. Par exemple, il est tout à fait possible (et même fréquent en pratique) que l’utilisateur ait dans son navigateur un onglet contenant un site contrôlé par l’adversaire pendant qu’il se connecte à sa messagerie (par exemple, via une bannière publicitaire) ; cet onglet est, comme n’importe quel autre site, capable de provoquer l’envoi de requêtes arbitraires vers le serveur de GMail, bien que la politique d’isolation des pages du navigateur empêche la lecture directe de la réponse à ces requêtes. De plus, la procédure pour se connecter à GMail implique un empilement complexe de protocoles : tout d’abord, un canal chiffré, et dont le serveur est authentifié, est établi avec le protocole TLS ; puis, une session HTTP est créée en utilisant un cookie ; enfin, le navigateur exécute le code JavaScript retourné par le client, qui se charge de demander son mot de passe à l’utilisateur.Enfin, même en imaginant que la conception de ce système soit sûre, il suffit d’une erreur minime de programmation (par exemple, une simple instruction goto mal placée) pour que la sécurité de l’ensemble de l’édifice s’effondre.Le but de cette thèse est de bâtir un ensemble d’outils et de librairies permettant de programmer et d’analyser formellement de manière compositionelle la sécurité d’applicationsWeb confrontées à un modère plausible des capacités actuelles d’un attaquant sur le Web. Dans cette optique, nous étudions la conception des divers protocoles utilisés à chaque niveau de l’infrastructure du Web (TLS, X.509, HTTP, HTML, JavaScript) et évaluons leurs compositions respectives. Nous nous intéressons aussi aux implémentations existantes et en créons de nouvelles que nous prouvons correctes afin de servir de référence lors de comparaisons. Nos travaux mettent au jour un grand nombre de vulnérabilités aussi bien dans les protocoles que dans leurs implémentations, ainsi que dans les navigateurs, serveurs, et sites internet ; plusieurs de ces failles ont été reconnues d’importance critiques. Enfin, ces découvertes ont eu une influence sur les versions actuelles et futures du protocole TLS. / As ever more private user data gets stored on the Web, ensuring proper protection of this data (in particular when it transits through untrusted networks, or when it is accessed by the user from her browser) becomes increasingly critical. However, in order to formally prove that, for instance, email from GMail can only be accessed by knowing the user’s password, assuming some reasonable set of assumptions about what an attacker cannot do (e.g. he cannot break AES encryption), one must precisely understand the security properties of many complex protocols and standards (including DNS, TLS, X.509, HTTP, HTML,JavaScript), and more importantly, the composite security goals of the complete Web stack.In addition to this compositional security challenge, onemust account for the powerful additional attacker capabilities that are specific to the Web, besides the usual tampering of network messages. For instance, a user may browse a malicious pages while keeping an active GMail session in a tab; this page is allowed to trigger arbitrary, implicitly authenticated requests to GMail using JavaScript (even though the isolation policy of the browser may prevent it from reading the response). An attacker may also inject himself into honest page (for instance, as a malicious advertising script, or exploiting a data sanitization flaw), get the user to click bad links, or try to impersonate other pages.Besides the attacker, the protocols and applications are themselves a lot more complex than typical examples from the protocol analysis literature. Logging into GMail already requires multiple TLS sessions and HTTP requests between (at least) three principals, representing dozens of atomic messages. Hence, ad hoc models and hand written proofs do not scale to the complexity of Web protocols, mandating the use of advanced verification automation and modeling tools.Lastly, even assuming that the design of GMail is indeed secure against such an attacker, any single programming bug may completely undermine the security of the whole system. Therefore, in addition to modeling protocols based on their specification, it is necessary to evaluate implementations in order to achieve practical security.The goal of this thesis is to develop new tools and methods that can serve as the foundation towards an extensive compositional Web security analysis framework that could be used to implement and formally verify applications against a reasonably extensive model of attacker capabilities on the Web. To this end, we investigate the design of Web protocols at various levels (TLS, HTTP, HTML, JavaScript) and evaluate their composition using a broad range of formal methods, including symbolic protocol models, type systems, model extraction, and type-based program verification. We also analyze current implementations and develop some new verified versions to run tests against. We uncover a broad range of vulnerabilities in protocols and their implementations, and propose countermeasures that we formally verify, some of which have been implemented in browsers and by various websites. For instance, the Triple Handshake attack we discovered required a protocol fix (RFC 7627), and influenced the design of the new version 1.3 of the TLS protocol.