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

Magazine
Marque
MISC
Numéro
64
Mois de parution
novembre 2012
Spécialité(s)


Résumé

Vous vous préoccupez sans doute de la sécurité de votre ordinateur ou de votre mobile, en évitant par exemple de récupérer le dernier virus à la mode. Mais qu'en est-il de votre voiture ? Avez-vous déjà pensé à activer des options « cachées » ou à changer le logiciel de contrôle du moteur pour le rendre plus puissant ? Les constructeurs veulent bien entendu éviter cela à tout prix, pour des raisons de sécurité routière, mais aussi pour ne pas mettre en danger leur modèle économique (options payantes qu'un utilisateur pourrait arriver à activer...). Cet article met en évidence les travaux faits pour la sécurisation des architectures automobiles. Il se focalise plus particulièrement sur la façon dont les preuves de sécurité peuvent être effectuées sur ces architectures, et notamment sur les protocoles de communication entre les calculateurs véhiculaires.


Body

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.

 

hsm-full

 

Figure 1 : Architecture d'une puce (ECU chip) comprenant un processeur applicatif (sur la droite : application code) et le module de sécurité HSM (sur la gauche). Le HSM comporte des accélérateurs matériels pour des fonctions cryptographiques, de la mémoire pour stocker les calculs en cours et le matériel cryptographique, et enfin un processeur pour piloter les différents accélérateurs.

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.

 

evitacar

 

Figure 2 : Les modules de sécurité HSM sont ajoutés à tout calculateur embarqué. Selon la nature du calculateur, une version simplifiée du HSM peut être implantée afin de réduire le coût de l'architecture.

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 :

1. ECU1 -> ECUKM:M1:={M:={{SesK}PSK1,gn,ts1},MAC(M, PSK1)}

2. ECUKM -> ECUN : M2:={M:={{SesK}PSKN,gn,ts2}, MAC(M, PSKN)}

3. ECUN -> ECUKM : M3:={M:={ACK, ts3}, MAC(M, PSKN)}

4. ECUKM -> ECU1 : M4:={M:={ACK, ts4}, MAC(M, PSK1)}

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.

(* Modélisation proVerif du protocole de distribution de clés *)

(* Données *)

data true /0.

data ack/0.

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.

(* Déclaration d'un canal de communication public *)

free c.

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.

(* Fonctions cryptographiques *)

fun encrypt /2.

reduc decrypt(encrypt(x, k),k)=x.

fun MAC/2.

fun verifyMAC / 3 .

equation verifyMAC(m,MAC(m, k), k)=true.free c.

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.

(* Modélisation de ECU1 *)

let processECU1 =

 (∗ Sending of M1 ∗)

 new ts1;

 new SesK; new groupNumber ;

 let m=(encrypt(SesK,psk1), groupNumber, ts1) in

 let m1=(m, MAC(m ,psk1)) in

  out(c, m1);  

 (∗ Receiving of M4 ∗)

 in(c, m4);

 let (ack4, ts4, mac4)=m4 in

 let res4 = verifyMAC((ack4, ts4), mac4, psk1) in

 if ack4 = ack then

  if res4 = true then

   event ECU1_Done ( ) ;

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

(* Modélisation de ECUKM *)

let processECUKM =

 (∗ Receiving of M1 ∗)

 in(c, m1);

 let (encrypt1, gn1, ts1, mac1) = m1 in

 let res1 = verifyMAC((encrypt1, gn1, ts1), mac1, psk1) in

 if res1 = true then

  let seskKM = decrypt(encrypt1 , psk1) in

  (∗Sending of M2 ∗)

  new ts2;

  let m = (encrypt(seskKM, pskn), gn1, ts2) in

  let m2 = (m, MAC(m, pskn)) in

  out(c, m2);

  (∗ Receiving of M3∗)

  in(c, m3); let (ack3, ts3, mac3) = m3 in

  let res3 = verifyMAC((ack3, ts3), mac3, pskn) in

  if res3 = true then

   if ack3 = ack then

   (∗ Sending of M4∗)

   new ts4;

   let m = (ack, ts4) in

   let m4 = (m, MAC(m, psk1)) in

   out(c, m4);

   event KM_Done ( ) .

( Modélisation de ECUN *)

let processECUN =

 (∗ Receiving of M2 ∗)

 in(c, m2);

 let (encrypt2, gn2, ts2, mac2) = m2 in

 let res2 = verifyMAC((encrypt2, gn2, ts2), mac2, pskn) in

 if res2 = true then

 let seskECUN = decrypt(encrypt2 , pskn) in

 (∗ Sending M3 ∗)

 new ts3;

 let m = (ack, ts3) in

 let m3 = (m, MAC(m, pskn)) in

 out(c, m3);

 event ECUN_Done ( ) .

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 « ! » ).

(* Lancement de sessions du protocle *)

process new psk1 ;

new pskn ; ((!processECU1) | (!processKM) | (!processECUN))

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:

event ECU1_Done ( ) ;

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 :

(* Accessibilité de ECU1_Done *)

query ev : ECU1_Done()

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 :

(* Confidentialité de SesK*)

query attacker: SesK

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 :

...

 event beginM1( ts1 );

 out(c, m1);

...

Et au niveau de KM :

...

 in(c, m1);

 let (encrypt1, gn1, ts1, mac1) = m1 in

 let res1 = verifyMAC((encrypt1, gn1, ts1), mac1, psk1) in

 if res1 = true then

  let seskKM = decrypt(encrypt1 , psk1) in

  event endM1( ts1 );

...

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.

(* Authenticité du message M1 *)

query evinj :endM1(x)==>ev:beginM1(x).

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 :

% proverif -in pi my_proverif_specification

...

The event ECU1_Done() is executed .

A trace has been found .

RESULT not ev:ECU1_Done() is false

...

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 :

...

Starting query not attacker :SesK_41[!1 = v_174]

RESULT not attacker :SesK_41[!1 = v_174] is true .

...

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

...

RESULT evinj :endM1(x_58) ==> evinj :beginM1(x_58) is false .

RESULT (but ev:endM1(x_635) ==> ev:beginM1(x_635) is true .)

...

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).

 

archi2

 

Figure 3 : Architecture du protocole modélisée avec l'outil UML TTool. Les propriétés de sécurité sont exprimées sur le même diagramme, en haut à gauche de ce dernier.

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.

 

sm1

 

Figure 4 : Extrait du comportement de l'entité ECU1 décrit sous la forme d'une machine à états UML. Le diagramme met en évidence des émissions de messages, des réceptions de messages, des manipulations de structures de données et de variables, et des tests.

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.

 

result

 

Figure 5 : Résultats de la vérification de propriétés de sécurité directement depuis l'outil TTool. L'utilisateur n'a aucunement besoin de connaître le langage pi-calculus ou la façon d'effectuer une preuve de sécurité avec ProVerif.

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

 



Article rédigé par

Par le(s) même(s) auteur(s)

Sécurité des véhicules connectés et/ou autonomes

Magazine
Marque
MISC
Numéro
87
Mois de parution
septembre 2016
Spécialité(s)
Résumé

L'antivirus de votre véhicule est-il bien à jour ? Son pare-feu est-il bien configuré ? Si cela est pour l'instant de l'ordre de la science-fiction, l'on commence à voir apparaître des attaques sophistiquées sur les systèmes embarqués des véhicules. Cet article présente les architectures actuelles, les attaques qu'elles peuvent subir, et les solutions de sécurité actuelles. Il explique aussi en quoi ces solutions devront évoluer pour sécuriser aussi les véhicules communicants et/ou autonomes.

Ventilation contrôlée par des framboises

Magazine
Marque
Hackable
Numéro
11
Mois de parution
mars 2016
Spécialité(s)
Résumé

La ventilation d'une maison est indispensable pour son assainissement. L'article propose un moyen à bas coût pour ventiler automatiquement et efficacement une habitation, tout en laissant à l'utilisateur la possibilité de piloter manuellement sa ventilation depuis Internet.

Les derniers articles Premiums

Les derniers articles Premium

Sécurisez vos applications web : comment Symfony vous protège des menaces courantes

Magazine
Marque
Contenu Premium
Spécialité(s)
Résumé

Les frameworks tels que Symfony ont bouleversé le développement web en apportant une structure solide et des outils performants. Malgré ces qualités, nous pouvons découvrir d’innombrables vulnérabilités. Cet article met le doigt sur les failles de sécurité les plus fréquentes qui affectent même les environnements les plus robustes. De l’injection de requêtes à distance à l’exécution de scripts malveillants, découvrez comment ces failles peuvent mettre en péril vos applications et, surtout, comment vous en prémunir.

Bash des temps modernes

Magazine
Marque
Contenu Premium
Spécialité(s)
Résumé

Les scripts Shell, et Bash spécifiquement, demeurent un standard, de facto, de notre industrie. Ils forment un composant primordial de toute distribution Linux, mais c’est aussi un outil de prédilection pour implémenter de nombreuses tâches d’automatisation, en particulier dans le « Cloud », par eux-mêmes ou conjointement à des solutions telles que Ansible. Pour toutes ces raisons et bien d’autres encore, savoir les concevoir de manière robuste et idempotente est crucial.

Présentation de Kafka Connect

Magazine
Marque
Contenu Premium
Spécialité(s)
Résumé

Un cluster Apache Kafka est déjà, à lui seul, une puissante infrastructure pour faire de l’event streaming… Et si nous pouvions, d’un coup de baguette magique, lui permettre de consommer des informations issues de systèmes de données plus traditionnels, tels que les bases de données ? C’est là qu’intervient Kafka Connect, un autre composant de l’écosystème du projet.

Le combo gagnant de la virtualisation : QEMU et KVM

Magazine
Marque
Contenu Premium
Spécialité(s)
Résumé

C’est un fait : la virtualisation est partout ! Que ce soit pour la flexibilité des systèmes ou bien leur sécurité, l’adoption de la virtualisation augmente dans toutes les organisations depuis des années. Dans cet article, nous allons nous focaliser sur deux technologies : QEMU et KVM. En combinant les deux, il est possible de créer des environnements de virtualisation très robustes.

Les listes de lecture

11 article(s) - ajoutée le 01/07/2020
Clé de voûte d'une infrastructure Windows, Active Directory est l'une des cibles les plus appréciées des attaquants. Les articles regroupés dans cette liste vous permettront de découvrir l'état de la menace, les attaques et, bien sûr, les contre-mesures.
8 article(s) - ajoutée le 13/10/2020
Découvrez les méthodologies d'analyse de la sécurité des terminaux mobiles au travers d'exemples concrets sur Android et iOS.
10 article(s) - ajoutée le 13/10/2020
Vous retrouverez ici un ensemble d'articles sur les usages contemporains de la cryptographie (whitebox, courbes elliptiques, embarqué, post-quantique), qu'il s'agisse de rechercher des vulnérabilités ou simplement comprendre les fondamentaux du domaine.
Voir les 67 listes de lecture

Abonnez-vous maintenant

et profitez de tous les contenus en illimité

Je découvre les offres

Déjà abonné ? Connectez-vous