Une nouvelle architecture informatique protège les données privées sensibles

Logiciel

Crédit : domaine public CC0

Comme nos données personnelles sont de plus en plus utilisées dans de nombreuses applications allant de la publicité à la finance en passant par la santé, la protection des informations sensibles est devenue une caractéristique essentielle des architectures informatiques. Les applications qui traitent ces données doivent faire confiance au logiciel système sur lequel elles s’appuient, comme les systèmes d’exploitation et les hyperviseurs, mais ces logiciels système sont complexes et présentent souvent des vulnérabilités qui peuvent mettre en péril la confidentialité et l’intégrité des données.

Au cours des deux dernières années, les chercheurs de Columbia Engineering ont travaillé avec Arm, une société leader dans la conception de logiciels et de propriété intellectuelle pour semi-conducteurs, pour remédier à ces vulnérabilités. L’équipe a maintenant dévoilé des technologies de vérification clés pour l’architecture Arm Confidential Compute Architecture (Arm CCA), une nouvelle fonctionnalité de l’architecture Armv9-A. L’article, présenté le 12 juillet lors du 16e Symposium USENIX sur la conception et la mise en œuvre des systèmes d’exploitation (OSDI ’22) à Carlsbad, en Californie, démontre la première vérification formelle d’un prototype de micrologiciel Arm CCA.

Arm CCA s’appuie sur le micrologiciel pour gérer le matériel afin d’appliquer ses garanties de sécurité, il est donc essentiel que le micrologiciel soit correct et sécurisé. Alors que de nombreux systèmes précédents reposent sur un micrologiciel, aucun d’entre eux ne peut garantir que le micrologiciel n’a pas de bogues. La vérification formelle est une méthodologie relativement nouvelle actuellement utilisée pour garantir l’exactitude des logiciels/matériels. Plutôt que de tester, la vérification formelle utilise des modèles mathématiques pour prouver que le logiciel et le matériel sont absolument corrects, et fournit ainsi le plus haut niveau de garantie d’exactitude.

“Nous avons prouvé, pour la première fois, que le micrologiciel est correct et sécurisé, ce qui a abouti à la première démonstration d’une architecture informatique confidentielle soutenue par un micrologiciel formellement vérifié”, a déclaré l’auteur principal de l’étude, Xupeng Li, titulaire d’un doctorat. élève de Ronghui Gu, professeur adjoint d’informatique de la famille Tang, et de Jason Nieh, professeur d’informatique et codirecteur du laboratoire des systèmes logiciels.

Bien qu’il existe de nombreuses approches pour vérifier l’exactitude des programmes simples, ils ne conviennent pas à quelque chose d’aussi complexe que le micrologiciel CCA. Les chercheurs ont donc dû développer de nouvelles techniques de vérification pour rendre possible la vérification du micrologiciel Arm CCA. Par exemple, le micrologiciel CCA est conçu pour l’évolutivité et les performances, il permet donc un fonctionnement hautement simultané et mélange le code C et le code assembleur. Le fonctionnement simultané est rendu possible en utilisant des méthodes de synchronisation à grain fin et un code avec des courses de données.

C’est un principe de conception d’Arm CCA que les logiciels non fiables doivent conserver le contrôle de la gestion des ressources matérielles, donc un défi clé est de prouver que le système est toujours sécurisé même si un logiciel non fiable peut retirer des ressources matérielles à sa guise. Les approches précédentes n’ont pas été en mesure de vérifier les programmes avec de telles propriétés. Cette nouvelle technique de vérification est suffisamment puissante pour vérifier les micrologiciels simultanés avec le code C et le code assembleur.

“Les bogues sont vraiment difficiles à trouver via les techniques classiques de test de logiciels”, a déclaré Xuheng Li, un autre Ph.D. étudiant de Nieh et Gu qui a co-écrit le travail. “Nous avons donc montré l’importance et la valeur de nos techniques de vérification formelle, le résultat final étant la première démonstration d’une architecture informatique confidentielle soutenue par un micrologiciel vérifié.”

L’équipe est très enthousiasmée par les nouvelles technologies de vérification qui peuvent être utilisées pour prouver l’exactitude des implémentations du micrologiciel sous-jacent à Arm CCA. Les processeurs Arm sont déjà déployés sur des milliards d’appareils à travers le monde. Au fur et à mesure que Arm CCA devient plus couramment utilisé pour protéger les données privées des utilisateurs, en particulier dans les services cloud et au-delà, les techniques de vérification présentées dans ce document apporteront une amélioration significative de la protection et de la sécurité des données.

L’un des défis des méthodologies formelles appliquées aux logiciels est la nécessité d’adapter les preuves lors de la mise à jour du logiciel. Les chercheurs travaillent sur de nouvelles technologies pour les aider à vérifier progressivement et rapidement les mises à jour du micrologiciel Arm CCA et à s’assurer que le dernier micrologiciel disponible est toujours vérifié.

Gu et Nieh ont ajouté qu’ils “voyaient la puissance et le potentiel de la vérification formelle à partir de notre travail, et nous sommes convaincus que la vérification formelle est une technique essentielle qui, dans un proche avenir, supplantera les tests logiciels actuellement utilisés”.


L’équipe construit le premier système logiciel cloud résistant aux pirates


Plus d’information:
Article : www.usenix.org/conference/osdi22/presentation/li

Fourni par l’École d’ingénierie et de sciences appliquées de l’Université de Columbia

Citation: Une nouvelle architecture informatique protège les données privées sensibles (14 juillet 2022) récupéré le 14 juillet 2022 sur https://techxplore.com/news/2022-07-architecture-sensitive-private.html

Ce document est soumis au droit d’auteur. En dehors de toute utilisation loyale à des fins d’étude ou de recherche privée, aucune partie ne peut être reproduite sans l’autorisation écrite. Le contenu est fourni seulement pour information.