Certification d'un processeur intrinsèquement sécurisé

De Ensiwiki
Révision de 13 octobre 2017 à 10:57 par Boulmes (discussion | contributions)

(diff) ← Version précédente | Voir la version courante (diff) | Version suivante → (diff)
Aller à : navigation, rechercher


Certification d'un processeur intrinsèquement sécurisé

Labo Vérimag
Equipe PACSS
Encadrants Sylvain.Boulme@univ-grenoble-alpes.fr,Jean-Louis.Roch@univ-grenoble-alpes.fr,Marie-Laure.Potet@univ-grenoble-alpes.fr

Thème général

Sécurité des systèmes, Architecture des processeurs, Logique appliquée à l'informatique.

Compétences

Mathématiques discrètes, goût pour la programmation assembleur et les langages de haut-niveau.

Contexte du travail

Le projet Nanotrust de l’IRT Nanoelec et du programme PULSE vise à concevoir un processeur basé sur le jeu d’instruction RISC V dédié aux objets communicants qui soit intrinsèquement sécurisé. Il devra répondre aux besoins des industriels en terme de sécurité et permettre la confidentialité, l’authenticité et l’intégrité du programme grâce à un chiffrement authentifié des données et des instructions. Une telle construction permet d’assurer un contrôle du flux d’instructions implicite et d’éviter les attaques logiciels de type malwares et stack/buffer overflow tout en assurant qu’aucun reverse engineering ne sera possible par du chiffrement. De plus, l’ajout de code correcteur/détecteur d’erreur dont certains auront des propriétés d’homomorphisme assurera qu’aucune faute ou erreur n’ait été injectée et ce même pendant l’exécution par l’ALU. Ceci augmente notablement la fiabilité du processeur souvent orthogonale à la sécurité jusqu’à une possible résilience du système.

CompCert est le premier compilateur C optimisant qui soit formellement vérifié (ce compilateur est notamment utilisé pour produire du code embarqué critique, comme celui dans le système de pilotage des Airbus). Pour chacun des processeurs cibles, il y a une preuve mathématique formelle réalisée dans l'assistant de preuves Coq que tout binaire produit par le compilateur a bien le comportement spécifié par le programme source en C. Une telle preuve nécessite en particulier de formaliser complètement le processeur cible. Depuis août 2017, CompCert fournit une formalisation de l'architecture RISC V (ainsi qu'un compilateur certifié pour cette cible).

Sujet

En partant de cette formalisation CompCert du RISC V, on doit pouvoir formaliser le processeur de Nanotrust. On aimerait alors pouvoir prouver formellement une ou plusieurs propriétés de sécurité revendiquées par Nanotrust comme la résistance aux attaques par buffer overflow. Intégrer cette formalisation dans CompCert permettra à terme d'avoir un compilateur certifié pour Nanotrust (et que les propriétés de sécurité de l'architecture soient elles-mêmes formellement certifiées).

Résultats attendus

- Formalisation du processeur intrinsèquement sécurisé de Nanotrust.

- Preuve d'une propriété de sécurité garantit par le processeur.