Des preuves mathématiques pour la sécurité des objets connectés ?

1. Sécuriser les objets connectés

Les objets connectés (IoT) posent des problèmes de cybersécurité inédits par rapport aux systèmes informatiques traditionnels (serveurs et stations de travail).

Tout d’abord, d’un point de vue technique, les objets connectés sont très accessibles, à divers niveaux :

• physiquement, par leur situation dans un espace public, ou logiquement, par leur connexion sans fil en bout de réseau, ce qui en fait des points d’entrée privilégiés dans un réseau ;
• la plupart du temps sans supervision, ou pas de manière continue, ce qui peut ralentir la détection d’une attaque ;
• disponibles à l'achat, ce qui permet souvent aux hackers d'en acheter quelques exemplaires à des fins de reverse engineering ou d’expérimentation.

Cette situation contraste avec une station de travail, régulièrement supervisée et protégée dans un réseau interne, et surtout avec un serveur, a fortiori au sein d’un cloud, qui bénéficie de nombreuses couches de défense, et est très difficilement accessible aux attaquants.

Ensuite, d’un point de vue économique, la plupart des parties prenantes s’intéressent peu à la sécurité des objets connectés, car ils peuvent la considérer comme une externalité économique : ils ne supporteront pas les coûts d’une éventuelle attaque, alors qu’ils devront supporter les surcoûts liés à la sécurité. Cette attitude désinvolte nous a mené à Mirai et ses botnets, et une épouvantable réputation (voir par exemple l’excellente analyse de Bruce Schneier [1]).

Tout n’est pas noir, cependant. Certains acteurs prennent conscience des enjeux de cybersécurité, souvent ceux qui doivent garantir une sûreté de fonctionnement, par exemple dans l’industrie ou dans l’automobile.  Ces prises de conscience font souvent suite à des épisodes douloureux, comme ceux auxquels BMW et Jeep ont dû faire face.

Par ailleurs, un atout majeur de nombreux objets connectés est leur simplicité, en particulier en matière de connectivité. De nombreux objets connectés respectent trois propriétés simples :

• l’objet est utilisé dans des conditions qui sont définies ou encadrées par une seule entité, généralement le fournisseur de l’objet ou du service associé ;
• l’objet ne se connecte sur Internet qu’à un seul serveur ou service cloud, en utilisant un seul protocole ;
• l’objet initie toutes les connexions vers ce serveur, et rejette toutes les connexions provenant d’Internet.

Ces propriétés définissent des conditions très favorables. Malheureusement, elles sont très souvent ignorées, soit par négligence (oups ! J’ai laissé le port FTP ouvert avec un client derrière), soit par facilité (laissons-nous la possibilité de nous connecter par FTP avec un bon mot de passe, au cas où).

Enfin, après 20 ans de mises à jour de sécurité sur Windows, iOS ou Android, et sur nos logiciels antivirus, nous sommes habitués à un modèle de sécurité réactif et réparateur. Sur un objet connecté exposé, sans supervision, et souvent mal connecté, ce modèle est difficilement applicable. Par contre, un tel objet est souvent simple, développé par une seule entité en composant des briques simples, ce qui représente un avantage significatif. Il doit donc être possible de garantir sa sécurité dès leur conception (Security by Design), et ensuite de garantir la mise en œuvre appropriée de ces concepts de sécurité.

Il est aujourd'hui possible d'aller très loin dans cette direction, en s'appuyant sur les fonctions de sécurité offertes par les microprocesseurs et microcontrôleurs récents, et en allant jusqu'à prouver mathématiquement que le logiciel écrit respecte des propriétés essentielles de sécurité. Cet article présente comment on peut combiner ces outils pour arriver à un niveau d'assurance de sécurité très élevé, en commençant par une introduction rapide des méthodes formelles utilisées pour démontrer mathématiquement les propriétés du code.

2. Les méthodes formelles

2.1 Raisonner sur le code

Les méthodes formelles sont associées au monde de la recherche, mais elles ont de nombreux usages pratiques, dès qu’il s’agit de raisonner mathématiquement sur un programme, pour en vérifier des propriétés.

Les outils d’analyse statique, très largement utilisés, se basent sur des raisonnements formels plus ou moins complexes pour vérifier qu’un programme vérifie un ensemble de règles. Par exemple, le service verify.ly analyse des applications iOS, et s’est fait de la publicité au début de 2017 en identifiant des dizaines d’applications qui ne vérifient pas bien les certificats TLS. Le vérifieur de bytecode de Java analyse le code de chaque classe pendant son chargement pour vérifier des propriétés comme le bon typage des données et le non-débordement des structures de données de la machine virtuelle ; la machine virtuelle peut alors se reposer sur ces propriétés pour effectuer des optimisations agressives pendant l'exécution.

Ces analyseurs statiques sont limités à la vérification d’un ensemble prédéfini de règles, sur du code source ou du code binaire spécifique. À l’inverse, les outils de méthodes formelles se basent sur un modèle mathématique d’un programme, sur lequel des propriétés peuvent être définies puis prouvées. Le modèle est construit spécifiquement pour un programme, la preuve est généralement construite manuellement, puis vérifiée automatiquement. Ces méthodes sont largement utilisées pour la sécurité des systèmes critiques. Par exemple, les fonctions principales du métro sans conducteur Val ont été prouvées correctes.

Certains outils permettent en outre de générer du code à partir d’un modèle. Un processus de compilation est montré en Figure 1. Le développeur utilise un seul langage pour définir le code et les spécifications, puis utilise des outils pour générer les propriétés à prouver (obligations de preuve), le code source C prêt à compiler, mais aussi la documentation indispensable dans le cadre d’une certification.

Les méthodes formelles, la modélisation de programmes, et la preuve de programmes sont des sujets de recherche très actifs. Pour une introduction passionnante, on peut se référer aux cours de Gérard Berry au Collège de France [2].

2.2 Une technique d’assurance

Les méthodes formelles sont une technique d’assurance, comme les tests fonctionnels et les tests de pénétration. Elles sont destinées à démontrer qu’un programme fonctionne correctement. Par rapport aux techniques de test, les méthodes formelles ont deux avantages majeurs :

• L’exhaustivité des preuves. Une preuve formelle couvre tous les cas possibles, et ne souffre pas d’exception. Si on prouve qu’un programme renvoie toujours une erreur sur 1 octet ou un paquet de 15 octets, il n’y a pas d’autre possibilité.
• La richesse des propriétés. Il est possible de modéliser et de prouver des propriétés qu’il est difficile, voire impossible de tester. Par exemple, il est possible de prouver qu’un programme ne contient pas d’accès illégal à des tableaux (buffer overflow), alors que cette propriété est généralement impossible à tester.

En matière de sécurité, ces deux avantages sont significatifs. Les vulnérabilités se cachent souvent derrière des conditions très spécifiques, qui ont échappé aux testeurs ; et les propriétés les plus intéressantes, concernant par exemple la confidentialité et l’intégrité des données, sont très difficiles à tester.

Les outils de modélisation et de preuve ne sont pas à la portée de tous, et requièrent une expertise particulière pour définir des modèles et pour construire des preuves. Ces outils évoluent, et des outils récents comme Smart innovent par leurs capacités à assister le développeur à effectuer les preuves nécessaires, et à générer du code source C suffisamment efficace pour être utilisé sur des systèmes embarqués.

Dès lors, ces outils peuvent être utilisés pour générer du code pour des objets connectés, par exemple pour développer un micronoyau qui puisse être utilisé comme base de confiance dans des objets connectés.

3. Un micronoyau et des preuves

Les fournisseurs de microprocesseurs et de microcontrôleurs introduisent de plus en plus de mécanismes de sécurité matériels dans leurs composants. Ces mécanismes fournissent des services utiles (isolation, cryptographie, et bien plus), mais ils doivent être correctement exploités par les couches logicielles.

Le micronoyau ProvenCore a été développé à destination des objets connectés pour exploiter au mieux ces mécanismes matériels, sur la base de quatre principes : l’exploitation d’une racine de confiance matérielle, la minimisation de la base de confiance, une isolation forte entre programmes, et enfin un niveau d’assurance élevé, reposant sur des preuves formelles.

3.1 Enraciner la confiance dans le matériel

Les microprocesseurs basés sur l’architecture ARM bénéficient aujourd’hui de l’architecture TrustZone, qui permet de séparer les ressources du processeur entre un Monde Normal et un Monde Sûr. Cette architecture est par exemple utilisée sur les smartphones pour protéger les mécanismes d’authentification par empreintes digitales.

Comme on le voit sur la figure 2, le processeur dispose de deux environnements d’exécution, dont un Trusted Execution Environment (TEE) dans le Monde Sûr. La technologie TrustZone garantit que les programmes du Monde Normal, y compris le noyau Linux dans l’exemple ne peuvent pas accéder au TEE et aux ressources qu’il gère.

Parmi ces ressources dédiées, ces microprocesseurs disposent de plus d’une large panoplie de périphériques de sécurité. On y trouve de la mémoire à écriture unique (One-Time Programming, OTP), très utile pour suivre le cycle de vie d’un objet, une vaste panoplie de fonctions cryptographiques (accélérateurs crypto, générateurs aléatoires, clé unique matérielle, etc.), un mécanisme de démarrage sécurisé, ainsi que des mécanismes complétant la technologie TrustZone pour contrôler l’accès aux périphériques et aux mémoires externes.

Enfin, il est également possible d’assigner des périphériques au Monde Sûr, les rendant inaccessibles depuis le Monde Normal. Par exemple, une connexion réseau peut être réservée au TEE.

Le premier principe, qui est commun à tous les TEEs, consiste à baser les mécanismes logiciels de sécurité sur cette base matérielle. L’idée est que les mécanismes matériels ne peuvent pas être « vaincus » par une attaque distante purement logicielle, et requièrent une attaque physique.

3.2 Réduire au strict minimum la base de confiance

Tout système informatique a à son cœur une base de confiance (Trusted Computing Base, ou TCB). C’est typiquement le noyau d’un système d’exploitation, et plus généralement la partie du système à laquelle nous sommes obligés de faire confiance.

Par exemple, sur un système Unix classique, une application n’est généralement pas dans la TCB, car elle s’exécute en mode utilisateur, et avec une identité d’utilisateur. Certains drivers ne sont pas non plus dans la TCB, même s’ils s’exécutent sous une identité root, car ils s’exécutent en mode utilisateur. Par contre, tout logiciel qui s’exécute en mode noyau sous une identité root fait partie de la TCB.

Le second principe est de minimiser la taille de la TCB, pour diminuer d’autant la surface d’attaque disponible. L’utilisation d’un TEE va dans cette direction, puisque la base de confiance n’est alors plus le système d’exploitation du Monde Normal, mais le TEE s’exécutant dans le Monde Sûr, et ce TEE est beaucoup plus petit qu’un système d’exploitation comme Linux.

Toutefois, certains TEE sont encore trop gros. Par exemple, le système QSEE de Qualcomm a été la victime de nombreuses attaques par un hacker (voir l’encart). En particulier, Gal Beniamini a pu abuser une application de DRM disposant de droits considérables pour aller modifier le noyau du système Linux.

Une autre approche est d’utiliser un micronoyau, un système d’exploitation minimal qui ne comprend que les fonctions essentielles comme la gestion des processus et de la mémoire. Tous les drivers et services de haut niveau sont alors considérés comme des applications. La TCB d’un tel système est alors minimale, réduite au micronoyau lui-même.

3.3 Isoler les programmes sensibles contre les interférences

Certaines applications sont sensibles, car elles gèrent ou utilisent des biens susceptibles d’être ciblés par des attaques. D’autres applications sont sensibles, car elles sont susceptibles d’être détournées de leur fonction première au cours d’une attaque :

• Dans la première catégorie, on trouve par exemple une application de chiffrement de communications, qui gère des clés privées, des certificats, ainsi que des données en cours de communication. Une telle application doit être protégée contre les interférences provenant d’autres applications, qui pourraient tenter d’accéder à des secrets ou de modifier des données de référence.
• Dans la deuxième catégorie, on trouve par exemple une application de DRM qui, pour déchiffrer des contenus, dispose de permissions lui permettant de lire et écrire dans la mémoire du Monde Normal. Afin d’éviter les abus, une telle application ne doit avoir accès qu’à une partie limitée de la mémoire du Monde Normal.

Le troisième principe est donc une variante du principe de moindre privilège. Les applications sensibles dans le Monde Sûr ne doivent avoir que les permissions nécessaires à leur fonctionnement, afin de les protéger contre des interférences externes, et aussi de protéger le reste du système contre une éventuelle vulnérabilité dans l’application.

Un micronoyau peut être utilisé à des fins d’isolation, en isolant ses applications les unes des autres, et c’est ce qui est fait dans ProvenCore, avec deux règles d’isolation :

• Intégrité. Les ressources d’une application (code, registres, données), ne peuvent être modifiées par une autre application, à moins que ladite application ait explicitement donné sa permission.
• Confidentialité. Les ressources d’une application (code, registres, données) ne peuvent être modifiées par une autre application, à moins que ladite application ait explicitement donné sa permission.

Dans leur définition complète, ces règles vont encore plus loin. Par exemple, le code d’une application ne peut en fait pas être modifié, sinon par une mise à jour logicielle et un redémarrage. Cette limitation peut paraître forte, mais son impact est limité pour un logiciel embarqué. Par contre, cette règle est simple à appliquer, et elle limite considérablement les possibilités offertes à un éventuel attaquant, dans la mesure où l’injection de code est utilisée dans de nombreuses attaques.

La contrainte majeure de ces règles d’isolation est que la communication entre applications n’est possible qu’après avoir mis en place les permissions nécessaires dans les deux applications. Toutefois, comme pour le code, il est possible de définir ces permissions statiquement, ce qui permet en outre un contrôle en amont efficace.

3.4 Prouver que cette isolation est effective

La dernière étape est de se convaincre que l’implémentation du micronoyau applique effectivement cette ambitieuse politique de sécurité. L'objectif est d'atteindre les niveaux d'assurance (voir l'encadré) les plus élevés. On utilise ici une méthodologie contraignante, des tests fonctionnels, des tests de pénétration, mais aussi des preuves formelles.

Pour des propriétés fonctionnelles, il est possible d’obtenir une couverture de tests de très bonne qualité. Pour les propriétés de sécurité, les tests fonctionnels ont des limites, et ils sont complémentés par des tests de pénétration effectués par le laboratoire, ainsi que par des preuves formelles.

Par exemple, pour prouver la propriété d'intégrité ci-dessus, il faut prouver (entre autres choses) qu'aucun accès à un tableau n'est effectué en dehors des limites. Une propriété aussi simple est très difficile à tester, car les tests ne permettent pas une couverture exhaustive. Il est donc indispensable de recourir à des méthodes mathématiques pour obtenir un niveau d'assurance très élevé.

Le quatrième et dernier principe consiste donc à utiliser des modèles formels et des preuves mathématiques pour vérifier que le micronoyau applique strictement la politique de sécurité définie, et en particulier les propriétés d’isolation entre applications.

De telles preuves sont très coûteuses à produire, ce qui limite leur champ d’application à des systèmes très simples. Les micronoyaux font partie des systèmes les plus complexes sur lesquels des preuves peuvent être produites [6], et ces preuves poussent les outils à leurs limites. La manière dont ces preuves sont construites pour ProvenCore consiste en trois étapes principales [7] :

• Preuve des propriétés sur un modèle abstrait. Un modèle formel abstrait est défini en fonction des propriétés à prouver, et une preuve est produite que ces propriétés sont toujours vérifiées dans ce modèle.
• Raffinements successifs. Un modèle plus détaillé est ensuite construit, avec une preuve que le modèle abstrait est une abstraction « correcte » de ce modèle plus détaillé (et donc, que les preuves effectuées sur le modèle abstrait sont valides sur le modèle détaillé). Ce processus de raffinement est effectué plusieurs fois, pour obtenir des spécifications fonctionnelles, puis une conception détaillée.
• Génération de code. Un outil est ensuite utilisé pour générer du code en C à partir de la conception détaillée. Le code C est enfin compilé pour obtenir le code exécutable du micronoyau.

La dernière étape de génération automatique de code va même au-delà des exigences les plus élevées, en établissant un lien formel direct du modèle abstrait au code.

Cette preuve est ensuite combinée à des tests fonctionnels des tests de pénétration, pour s’assurer que le micronoyau est fonctionnellement correct, et que l’intégration avec le matériel est correctement effectuée. La combinaison de ces tests et de la preuve réduit considérablement la probabilité de trouver une vulnérabilité, probablement d’au moins un ordre de grandeur. La tâche d’éventuels attaquants est donc beaucoup plus difficile.

4. Retour sur les objets connectés

Pour comprendre en quoi un tel micronoyau peut servir à résoudre les problèmes de sécurité des objets connectés, la première étape est de s’intéresser à la résilience de ces objets, soit à leur capacité de survivre à des attaques réussies, et de les surmonter.

L’objectif essentiel est ici de s’assurer de l’intégrité et de l’authenticité du logiciel, à travers un mécanisme de démarrage sécurisé et un mécanisme de mise à jour du logiciel. En isolant ces deux mécanismes essentiels sur un environnement prouvé s'exécutant dans le Monde Sûr, il devient beaucoup plus difficile pour un attaquant de prendre le contrôle de l’objet connecté, et surtout, de conserver ce contrôle.

Pour bien comprendre l’apport de cette solution, il faut se placer dans la situation périlleuse où un attaquant a pris le contrôle du système d’exploitation du Monde Normal. Pour cela, il suffit de combiner une attaque permettant d’exécuter du code choisi avec une attaque en élévation de privilèges pour exécuter ce code en mode noyau, ce qui est courant dans les attaques sur les objets connectés.

Dans une telle situation, l’attaquant ne tardera pas à désactiver toutes les contremesures du Monde Normal. Par contre, les contremesures du Monde Sûr restent activées. Et si ces contremesures s’exécutent sur un micronoyau prouvé, les chances de reproduire les attaques effectuées sur Linux sont infimes. L’attaquant ne pourra donc pas désactiver le système de mise à jour, et le gestionnaire de l’objet connecté pourra quand il sera prêt, corriger les vulnérabilités de son logiciel et reprendre le contrôle de son objet connecté. Ici, l'attaque a lieu, mais ses conséquences et sa faculté de nuisance sont considérablement réduites.

Un avantage majeur de l'ajout de cette capacité de résilience est qu'elle est orthogonale aux fonctionnalités de l'objet connecté. L'ajout d'un micronoyau dans le Monde Sûr avec ces applications de résilience est entièrement transparent pour le développeur, et ne nécessite aucune adaptation du logiciel de l'objet connecté.

Pour aller plus loin, il est possible d'ajouter dans le Monde Sûr des services de sécurité de plus haut niveau pouvant profiter au système d’exploitation ou aux applications du Monde Normal. La cryptographie est un premier exemple. Dans de nombreux processeurs, les fonctions cryptographiques avancées ne sont accessibles que depuis le monde sûr ; les librairies cryptographiques et le stockage des clés sont donc naturellement implémentés dans le Monde Sûr. L’isolation fournie par le monde sûr permet aussi de stocker et de gérer les clés en sécurité, hors d’atteinte d’éventuels programmes malveillants dans le Monde Normal.

Les traitements cryptographiques peuvent être étendus à des protocoles de plus haut niveau, comme TLS ou OpenVPN. Dans de tels cas, où le Monde Sûr protège des communications, il est également possible d’associer le périphérique au monde sûr (un port Ethernet, par exemple). Cela permet de garantir qu’aucune interception ne soit possible depuis le monde normal.

En associant toutes ces applications, on peut arriver à un cas d’usage intéressant : fournir une plateforme de base sécurisée pour se connecter à un service d’IoT dans le cloud, dont une architecture est proposée en figure 4.

Cette plateforme pourrait par exemple être utilisée pour développer une passerelle sécurisée pour connecter à un service cloud des objets. Dans cet exemple, trois services principaux sont gérés dans le Monde Sûr :

• la mise à jour du firmware, essentielle pour garantir la résilience du système, sa capacité à survivre à une attaque ;
• une pile de communication sécurisée (entourée en rouge), simplifiée pour ne supporter qu’une version d’un seul protocole pour communiquer avec un seul service ;
• un ensemble de filtres de sécurité (entourés en bleu), destinés à appliquer une politique de sécurité en entrée (pour vérifier la validité des commandes) et en sortie (pour vérifier la validité des réponses et pour faire respecter des règles de vie privée).

Cette plateforme de base peut être fournie à des fabricants, à la fois pour protéger leur matériel contre des attaques externes et pour protéger le monde extérieur d’éventuelles failles dans leur matériel.

L’utilisation d’un TEE, et a fortiori d’un micronoyau formellement prouvé, permet de protéger contre les agressions extérieures en réduisant les opportunités d'attaque, et aussi de limiter les dégâts infligés par une plateforme compromise (potentiellement par d’autres chemins, par exemple via un smartphone connecté directement à la passerelle en Bluetooth).

Ces capacités d’isolation, profitant à tous les acteurs, mènent des filières à haut niveau de responsabilité, comme l’automobile ou l’aéronautique, à montrer un intérêt prononcé pour ces solutions. De plus, un tel environnement sûr est un complément intéressant aux solutions de sécurité classiques, et donne un véritable espoir de résistance durable à certaines attaques.

Pour reprendre l’exemple de connexion à un service cloud, une telle plateforme de référence peut permettre de garantir que les objets connectés respectent une politique de sécurité cohérente, avec une combinaison satisfaisante de mesures fonctionnelles et de robustesse contre les attaques.

Conclusion

La sécurité de base proposée par la technologie TrustZone, combinée à l’isolation proposée par un micronoyau et à des preuves formelles des propriétés de sécurité mises en place, a le potentiel de devenir un élément important dans la sécurité de l’IoT. Ce mécanisme peut contribuer à la sécurité des objets connectés sensibles ou exposés, comme base pour l’implémentation des contremesures fonctionnelles. Il peut également fournir une faculté de résilience à haut niveau d'assurance, qui pourrait servir de base à des objectifs ou contraintes règlementaires pour les objets connectés.

Remerciements

Je remercie la société Prove & Run de m'avoir encouragé à écrire cet article et à mentionner ses produits ProvenCore et Smart, ainsi que les relecteurs du magazine pour leurs retours riches.

Références

[1] Bruce Schneier, Security and the Internet of Things : https://www.schneier.com/blog/archives/2017/02/security_and_th.html

[2] Gérard Berry, Cours au Collège de France : https://www.college-de-france.fr/site/gerard-berry/_course.htm

[3] Gal Beniamini, blog : http://bits-please.blogspot.fr

[4] Article Wikipédia sur les Critères Communs : https://fr.wikipedia.org/wiki/Critères_communs

[5] Portail des Critères Communs (en anglais) : https://www.commoncriteriaportal.org/

[6] Daniel Potts et al., Mathematically Verified Software Kernels : Raising the Bar for High Assurance Implementations : https://sel4.systems/Info/Docs/GD-NICTA-whitepaper.pdf

[7] Stéphane Lescuyer, ProvenCore : Towards a Verified Isolation Micro-Kernel : http://mils-workshop-2015.euromils.eu/downloads/hipeac_literature/04-mils15_submission_6.pdf