Vers des véhicules (enfin) plus sécurisés

1. Introduction

Si certains secteurs des systèmes embarqués se sont intéressés tôt dans la mise au point de mécanismes de sécurité embarqué (par exemple, le domaine des terminaux mobiles), d’autres au contraire n’en ont pas fait leur cheval de bataille, privilégiant avant tout la sûreté de fonctionnement à la sécurité. Par exemple, le domaine de l’automobile n’est pas particulièrement féru de sécurité. Certaines attaques ont ainsi été menées facilement pour accéder aux principales fonctions des automobiles, en se connectant assez simplement sur le bus principal de la voiture. Il suffit aussi d’un peu chercher sur Internet pour trouver des correctifs logiciels qui permettent d’activer de nouvelles options de son véhicule, d’augmenter la puissance du moteur : une partie de ces modifications permet d'atteindre des fonctionnalités qui sont normalement facturées par le constructeur ou par le concessionnaire automobile. Ainsi, il est possible d'acheter un modèle de véhicule peu puissant, puis de modifier son véhicule pour le rendre aussi puissant qu'une version plus haut de gamme.

Nous venons de le voir, la sécurité peut avoir un impact sur l’économie d’un secteur. Dans l’avenir, cela aura aussi un impact fort sur la sûreté des automobilistes. En effet, les constructeurs ont décidé d’améliorer la sûreté grâce à des communications entre les véhicules, et entre les véhicules et les infrastructures routières (panneaux, péages, etc.). Un exemple : le véhicule précédant le votre détecte un obstacle sur la route et vous le signale afin que vous puissiez réaliser un freinage d’urgence. Si ces technologies peuvent sans doute diminuer le nombre d’accidents et la gravité des blessures, elles soulèvent de nouvelles questions de sécurité afin de prévenir des attaques sur ces systèmes. Par exemple, on pourrait imaginer une personne mal intentionnée émettant de faux messages d’obstacles afin de provoquer des freinages d’urgence inutiles, ou au contraire, des attaques rendant inopérant le système de freinage.

La commission européenne a décidé de financer plusieurs projets de recherche liés à la sécurisation des systèmes embarqués de l’automobile. Par exemple, le projet SEVECOM s’intéresse à la sécurisation des communications entre véhicules. Le projet EVITA [2] se focalise pour sa part sur la sécurisation des calculateurs embarqués. Comment sécuriser de tels calculateurs ? Comment prouver que cette sécurisation est effective ? Ces deux questions sont abordées par la suite.

2. Contexte : les systèmes embarqués de l'automobile

Un système embarqué véhiculaire est d’une nature assez hétérogène. Il comprend une petite centaine de calculateurs dont certains sont limités à quelques fonctions basiques de relevé de capteurs, alors que d’autres beaucoup plus complexes gèrent par exemple l’affichage du panneau de bord, ou gèrent le fonctionnement du moteur. Chaque calculateur - appelé ECU pour Electronic Control Unit - comporte en règle générale un microprocesseur (par exemple, un PowerPc), un bus interne, une mémoire, des capteurs reliés sur le bus interne, et une interface vers un bus externe. Ce bus externe est soit le bus principal du véhicule, soit un bus d’un sous-domaine du bus principal. Les bus sont généralement de type CAN ou FlexRay.

Du point de vue logiciel, selon la complexité des ECU, des simples séquenceurs de tâches peuvent être utilisés, ou alors des systèmes d’exploitation plus complets, comme Linux. Aussi, l’utilisation de l’intergiciel AUTOSAR [1] se démocratise.

3. Une méthodologie de conception de systèmes sécurisés

La plupart des systèmes embarqués ne sont pas sécurisés dans leur première version. Ce qui ne veut pas dire qu’une qualité appliquée sur le logiciel embarqué n’aura pas comme effet de réduire les éventuelles failles, mais généralement, la sécurité ne fait pas partie des spécifications de base du système. Par contre, lorsque des failles de sécurité sont découvertes sur les produits, des versions plus sécurisées des systèmes sont produites dans un deuxième temps.

Dans notre cas, les systèmes embarqués automobiles ont clairement été produits dans un premier temps sans prendre en compte les critères de sécurité. La méthodologie que nous avons appliquée comprend trois grandes étapes :

1. Une phase d’analyse du système. Cette dernière intègre une définition des cas d’utilisation (les applications à sécuriser), une recherche exhaustive des attaques possibles et l’évaluation du risque de ces attaques, et enfin la définition des exigences du système.

2. Une phase d’architecture système, qui consiste à définir l’environnement matériel et logiciel du système. Cela comporte, dans le cadre d’un système sécurisé, la définition du matériel cryptographique (les clés : leur taille, leur contenu, leur localisation initiale), les protocoles cryptographiques. Il convient aussi d’évaluer cette architecture pour avoir une bonne idée des performances et notamment si les ajouts liés à la sécurité peuvent compromettre les latences maximales liées à la sûreté de fonctionnement. Par exemple, l’exécution d’une primitive cryptographique ne doit pas avoir trop d’impact sur la latence au freinage. Enfin, il convient de vérifier que l’architecture proposée répond bien aux exigences de sécurité identifiées à l’étape précédente. Ainsi, une phase de vérification formelle est souhaitable, notamment pour les aspects les plus critiques du système : par exemple l’échange des clés cryptographiques.

3. Une phase de prototypage/démonstration, dans laquelle on implémente un sous-ensemble jugé pertinent du système, et que l’on soumet à des tests de sécurité (fuzzing, etc.). Ces tests de sécurité sont effectués au regard des attaques possibles identifiées en phase d’analyse.

4. Une architecture sécurisée

De façon simplifiée, le projet EVITA a pris comme hypothèse que les attaques matérielles ne sont pas possibles. Ainsi, les attaques qui consistent à obtenir du matériel cryptographiques (clés, messages chiffrés) par analyse de consommation d’énergie ou de rayonnements divers ne sont pas considérées. Par contre, les attaques sur les bus (probing) sont possibles. Cela fait d’ailleurs partie des attaques courantes dans les automobiles d’aujourd’hui.

Pour sécuriser les communications entre processeur et mémoire, il a été décidé d’implanter les deux sur la même puce (System-on-Chip), et d’ajouter sur ces puces des clés cryptographiques « en dur ». Pour toutes les communications externes à cette puce, les messages critiques du système sont chiffrés, authentifiés de façon unique, et rendus intègres. Pour assurer que les clés ne peuvent pas être découvertes avec des attaques brutes forces, elles sont mises à jour toutes les deux heures avec un protocole de distribution de clés. Ces clés sont distribuées par groupe d’intérêt pour certains messages. Aussi, afin de s’assurer un certain isolement entre les différents domaines, des pare-feu sont mis en place entre les domaines, avec des politiques d’accès qui sont mises à jour en fonction des conditions d’utilisation du véhicule. Enfin, un audit d’éventuelles attaques (retransmissions par exemple, accès erronés sur les pare-feu, etc.) est réalisé, permettant de se mettre dans un mode dégradé en cas de détection d’attaques.

Dernier point mais non des moindres : le fait de chiffrer de nombreux messages oblige bien entendu à augmenter la puissance des processeurs, notamment pour l’implémentation des algorithmes cryptographiques asymétriques. La solution retenue dans le projet EVITA consiste à ajouter à la puce processeur-mémoire des accélérateurs matériels pour les algorithmes cryptographiques sélectionnés. Cet accélérateur est nommé « HSM » (Hardware Security Module), et est présenté en figure 1.

 

 

Cependant, avoir autant d'accélérateurs dans chaque calculateur a un coût important, qui multiplié par le nombre de calculateurs et le nombre de véhicules vendus par un constructeur représente un montant total non négligeable. Pour cette raison, il a été défini trois types de HSM : low, medium, et full. Ainsi, si un calculateur effectue peu de calculs, dédiés à de simples capteurs, on pourra envisager d'implanter une version allégée. La figure suivante présente l'architecture typique du HSM dans sa version complète. Les versions allégées ne comprennent qu'un sous-ensemble des différents blocs cryptographiques. La figure 2 met en évidence la répartition des différentes versions du HSM dans l'architecture embarquée d'un véhicule.

 

 

L’architecture de sécurité est complétée avec un ensemble de protocoles cryptographiques assurant les fonctions de « base » entre les différents calculateurs : distribution des clés, mises à jour des firmwares dans les calculateurs, échange de messages chiffrés et authentifiés, etc. L’ensemble de l’architecture est décrit dans [11] et [10].

5. Preuve de sécurité

Une fois l’architecture de sécurité définie, il est recommandé de prouver que ses mécanismes résistent bien aux attaques pré-identifiées en phase d’analyse. Les parties critiques de l’architecture de sécurité sont bien entendu les protocoles cryptographiques réalisés de façon ad hoc, et destinés aux échanges de messages entre ECU. En effet, si les calculs et communications effectués au sein d'un calculateur sont par hypothèse sécurisés, les communications externes, c'est-à-dire entre calculateurs, entre véhicules, ou entre le véhicule et un garage peuvent être écoutées facilement par un attaquant. Un des protocoles cryptographiques est particulièrement critique pour la sécurité : le protocole de distribution de clés. C’est donc celui-là que nous allons étudier ensemble.

5.1. Protocole de distribution de clés

Du terme mathématique - cryptographique habituel, ce protocole se décrit ainsi :

Brièvement, l’ECU1 désire envoyer une nouvelle clé SesK à un groupe de calculateurs (ECUN). Dans le premier message M1, ECU1 envoie au gestionnaire de clés (ECUKM, KM = Key Master) la clé SesK, ainsi que le numéro de groupe gn et un identifiant unique ts1. Le message est chiffré avec une clé connue uniquement de ECU1 et ECUKM (PSK1). Le message M1 comporte aussi un MAC : MAC(M, PSK1). Le gestionnaire de clés vérifie l’authenticité et l’intégrité du message, et envoie la clé SesK aux différents membres du groupe : dans notre cas, nous avons utilisé un seul membre, appelé ECUN (Message M2). Ce membre, une fois la clé SesK correctement reçue, émet un acknowledge vers le gestionnaire de groupe (Message M3). Une fois que ce dernier a reçu un acknowledge de tous les membres du groupe, il émet un acknowledge vers ECU1 (Message M4).

Nous allons montrer comment vérifier deux propriétés de sécurité relatives à ce protocole :

- la confidentialité de la clé SesK ;

- l’authenticité des messages M1, M2, M3 et M4.

5.2. L'outil ProVerif

Pour effectuer la preuve de ces deux propriétés, nous avons utilisé un outil appelé ProVerif [5] [4]. L’idée est de décrire le protocole dans une algèbre de processus appelée pi-calculus, puis d’utiliser le moteur de preuves automatique de ProVerif. Ces preuves sont réalisées avec un attaquant tel que décrit par Dolev et Yao [6]. Ainsi, un attaquant peut écouter toutes les communications réalisées sur des canaux de communication publics. Cette écoute lui permet d’enrichir son savoir. Elle lui permet aussi, à partir de son savoir, de pouvoir analyser les messages reçus (les décrypter), puis en construire de nouveaux avant d’émettre ces derniers sur les canaux publics.

Une spécification ProVerif comprend une description des primitives cryptographiques utilisées pour construire les messages, une description des canaux de communication et du savoir des entités du protocole, une description du protocole, et enfin une description des propriétés à prouver sur le protocole. ProVerif permet la description de propriétés de confidentialité et d’authenticité. Pour chaque propriété, le moteur répond par true ou false : dans ce dernier cas, il essaie de donner une trace amenant à la violation de la propriété de sécurité, c’est-à-dire la séquence d’actions que doit réaliser l’attaquant pour effectuer l’attaque. En fait, le moteur peut aussi répondre par « je ne sais pas prouver cette propriété », dans le cas où le moteur de preuves ne peut parvenir à analyser le système décrit en pi-calculus au regard de la propriété à prouver

5.3. Modélisation du protocole en langage pi-calculus

Étudions pas à pas comment modéliser le protocole en pi-calculus. La spécification comporte deux grandes parties : l’en-tête et le comportement. L’en-tête permet de déclarer les primitives cryptographiques, les canaux de communication, et les variables globales. Le comportement permet de décrire les différentes étapes du protocole.

Commençons par l’en-tête. Nous déclarons tout d’abord les différentes variables et données globales. Notons qu’en pi-calculus, les variables n’ont pas de valeur ni de type. Nous définissons deux données : true, ack.

On déclare ensuite un canal de communication public c qui servira pour les échanges de données entre ECU. Les échanges internes aux ECU sont par construction sécurisés puisque l’on considère que les échanges sur les bus on-chip ne peuvent être écoutés.

Dans un deuxième temps, nous déclarons les primitives cryptographiques dont le protocole se sert : la crypto symétrique et le calcul de MAC. La fonction encrypt prend deux arguments, et la fonction decrypt permet de retrouver la valeur x lorsque la même valeur k est fournie à encrypt et decrypt. Pour le calcul du MAC, le même principe a été utilisé, sauf que la fonction ne peut pas être inversée : une fonction de vérification du MAC permet de dire si un calcul de MAC depuis un message et une clé est égal à une valeur fournie.

La description du comportement du protocole se fait en deux étapes : la description du comportement global et la description de chaque entité. Le comportement global est comme suit. Le processus processECU1 crée un timestamp unique, une nouvelle clé, et un nouveau numéro de groupe. Le message M1 est construit puis émis sur le canal public out(c, m1). La prochaine étape consiste à attendre un message en retour du gestionnaire de clé : in(c, m4). Le message est analysé progressivement pour vérifier qu’il contient bien un acknowledge, et que le MAC du message est conforme à ce qu’il devrait être.

Les processus correspondant au gestionnaire de clés et à une ECU du groupe sont construits d’une façon assez similaire.

Enfin, il reste à donner deux indications au système : deux clés ont été créées avant le démarrage du système (psk1, pskn). Les processus processECU1, processKM et processECUN sont lancés en parallèle (symbole « | ») un nombre infini de fois (symbole « ! » ).

5.4. Preuve de sécurité avec ProVerif

La modélisation du protocole est réalisée. Mais il reste à exprimer les propriétés de sécurité que nous désirons vérifier formellement, puis effectuer leur vérification.

5.4.1. Expression des propriétés

Une première étape consiste à examiner si le protocole peut s’exécuter correctement, c’est-à-dire si les trois entités protocolaires peuvent arriver à la fin de l'exécution. En effet, faire des preuves d’authenticité ou de confidentialité sur un protocole qui ne peut réaliser aucun envoi de message ne sert pas à grande chose. Pour faire cette preuve, nous ajoutons à la fin de chaque processun événement (event). Par exemple, à la fin de processECU1:

et dans l’en-tête du fichier, on ajoute une « query » qui permet d’examiner une propriété exprimée dans la suite de la query. Par exemple, l’événement ECU1_Done est t-il accessible (i.e., peut-être exécuté) ou non :

Cela a bien entendu été fait pour les trois processus.

Pour prouver le respect ou non de la confidentialité de la clé partagée, une simple query est ajoutée en en-tête :

L’expression de l’authenticité est plus difficile. De façon simple, un message est considéré comme authentique s’il a bien été forgé auparavant par la « bonne » personne. Pour modéliser un tel schéma, on utilise les événements ProVerif : on ajoute un événement à l’envoi d’un message, et un événement à la réception du message : pour un événement de réception, il doit exister exactement un et un seul (injection) événement d’envoi. Comme nous avons modélisé des sessions multiples dans notre protocole, il faut en plus identifier ces événements à un identifiant unique : le timestamp. Ce qui donne, par exemple, pour le message M1 : au niveau du processus ECU1 :

Et au niveau de KM :

Au niveau de la query de l’authenticité, nous exprimons l’injection entre l’événement de réception et l’événement d’envoi.

Les propriétés d'authenticité des messages M2, M3 et M4 peuvent être modélisées d'une façon similaire.

5.4.2. Réalisation des preuves de propriétés

Réalisons à présent la preuve. Il suffit pour cela d’installer l’outil ProVerif puis de lancer l’outil en lui fournissant en entrée notre spécification. Nous montrons ici le résultat obtenu pour les trois types de propriétés étudiées :

- Les propriétés d’accessibilités des événements de fin d’exécution des entités sont vérifiées :

Cette trace nous indique que ProVerif a trouvé un moyen d’accéder à l’événement ECU1_Done, ce qui prouve son accessibilité.

- La propriété de confidentialité de la clé cryptographique est également vérifiée :

- Les propriétés d’authenticité sont partiellement vérifiées. Par exemple, pour le message M1, le résultat est le suivant :

Ce résultat nous indique qu’un message M1 reçu par KM a forcément été forgé par ECU1 dans le passé (la deuxième ligne du résultat). Mais cette relation n’est pas injective (première ligne du résultat), c’est-à-dire qu’il est possible à un attaquant de ré-émettre un message ancien (attaque par rejeu). En fait, nous n’avons pas modélisé un point important de notre système : l’estampillage temporel des messages, ainsi qu’une horloge synchronisée entre entités du système, ce qui permet d’éviter le rejeu.

L’ensemble des résultats de preuve peut être consulté dans [7].

5.5. Preuves de sécurité depuis UML : l'approche AVATAR

Les preuves présentées dans la section précédente ont comme inconvénient essentiel qu’elles nécessitent l’apprentissage d’un langage spécifique, qui ne peut facilement être intégré dans des processus industriels d’ingénierie système. Ces derniers reposent de plus en plus fréquemment sur des modèles réalisés avec les langages UML. Dans ce contexte, et toujours dans le cadre du projet EVITA, nous avons rendu possible le fait de décrire un protocole cryptographique au sein d’un modèle UML d’un système embarqué.

Brièvement, nous avons utilisé un environnement UML appelé AVATAR [8]. Cet environnement reprend un sous ensemble pertinent des diagrammes UML pour la modélisation des systèmes embarqués. AVATAR est implémenté par un outil open source appelé TTool [3]. Cet outil permet d’éditer les diagrammes AVATAR, et de réaliser automatiquement des preuves de sûreté de fonctionnement directement depuis les diagrammes. Par exemple, nous pouvons notamment prouver le fait qu’une tâche ne ratera jamais sa limite de temps (deadline). Ces preuves se font avec une approche presse-bouton, ce qui fait qu’un utilisateur de l’outil TTool n’a pas besoin de connaître les langages formels (i.e., mathématiquement définis) sous-jacents.

Dans le cadre du projet EVITA, nous avons enrichi ces diagrammes AVATAR avec la possibilité d’exprimer des primitives cryptographiques et des propriétés de sécurité [9]. Ainsi, depuis une icône, l’utilisateur de TTool peut demander automatiquement la vérification de ces propriétés de sécurité. TTool transcrit en fait les diagrammes AVATAR dans une spécification en pi-calculus, puis appelle automatiquement ProVerif, avant de présenter les résultats de façon synthétique.

Le diagramme de la figure 3 présente l’architecture du protocole modélisée en AVATAR avec TTool. Cette architecture comporte un bloc pour chaque entité du protocole, un bloc englobant, ainsi que les propriétés et hypothèses du système décrites dans une note (en haut à gauche du diagramme).

 

 

Le comportement de chaque bloc est décrit à l’aide d’une machine à états. La figure 4 présente un extrait de la machine à états de l’ECU1.

 

 

La vérification des propriétés de sécurité se réalise avec une approche de type presse-bouton. La figure 5 montre comment les résultats de vérification sont présentés par TTool.

 

 

Conclusion

Cet article met en évidence la sécurisation d’un système embarqué véhiculaire. La méthodologie de sécurisation présentée a été mise en œuvre dans le cadre du projet de recherche EVITA [2]. Le résultat est la définition d’une architecture sécurisée, la preuve que des nouveaux mécanismes permettent d’assurer certaines propriétés de sécurité, et une première implémentation de ce système. L’article a mis un accent tout particulier sur la preuve de protocoles cryptographiques, preuves qui reposent sur la description en pi-calculus de ces protocoles, et sur l’utilisation d’un moteur de preuves appelé ProVerif. L’approche de preuve a permis d’identifier plusieurs failles de sécurité qui ont été corrigées depuis. Aussi, les descriptions des protocoles peuvent être réalisées en UML avec l’outil TTool, puis prouvées automatiquement sans connaissance préalable sur le pi-calculus. Les technologies définies dans le projet EVITA se retrouveront d’ici quelques années dans des véhicules européens.

Remerciements

Nous remercions les différents partenaires du projet EVITA : Bosch, BMW, Continental, Escrypt, Eurecom, Fujitsu, Infineon, les instituts Fraunhofer SIT, l’institut Mines-Telecom / Telecom ParisTech, Trialog, et l’Université catholique de Louvain. Gabriel Pedroza, de Telecom ParisTech, m'a assisté dans la modélisation du protocole.

Références

[1] AUTOSAR : Automotive open system architecture. http://www.autosar.org/

[2] The EVITA european project. http://www.evita-project.org/

[3] Ludovic Apvrille. TTool. In http://ttool.telecom-paristech.fr/

[4] B. Blanchet. Automatic verification of correspondences for security protocols. Journal of Computer Security, 17(4) :363–434, July 2009

[5] Bruno Blanchet. ProVerif. In http://www.proverif.ens.fr/

[6] D. Dolev and A.C. Yao. On the security of public key protocols. IEEE trans. on Information Theory, 29 :198–208, 1983

[7] A. Fuchs, S. Gürgens, L. Apvrille, and G. Pedroza. On-Board Architecture and Protocols Verification.Technical Report Deliverable D3.4.3, EVITA Project, 2010

[8] Daniel Knorreck, Ludovic Apvrille, and Pierre De Saqui-Sannes. TEPE : A SysML language for timed- constrained property modeling and formal verification. In Proceedings of the UML&Formal Methods Workshop (UML&FM), Shanghai, China, November 2010

[9] G. Pedroza, D. Knorreck, and L. Apvrille. Avatar : A sysml environment for the formal verification of safety and security properties. In The 11th IEEE Conference on Distributed Systems and New Technologies (NOTERE’2011), Paris, France, May 2011

[10]  H. Schweppe, M. S. Idrees, Y. Roudier, B. Weyl, R. El Khayari, O. Henniger, D. Scheuermann, G. Pedroza, L. Apvrille, H. Seudié, H. Platzdasch, and M. Sall. Secure on-board protocols specification. Technical Report Deliverable D3.3, EVITA Project, 2010

[11]  H. Seudié, J. Shokrollahi, B. Weyl, A. Keil, M. Wolf, F. Zweers, T. Gendrullis, M. S. Idrees, Y. Roudier, H. Schweppe, H. Platzdasch, R. El Khayari, O. Henniger, D. Scheuermann, L. Apvrille, and G. Pedroza. Secure on-board architecture specification. Technical Report Deliverable D3.2, EVITA Project, 2010