Protocole distribué sous-tendant le cloud computing déterminé automatiquement sûr et sécurisé

Protocole distribué sous-tendant le cloud computing déterminé automatiquement sûr et sécurisé

Illustration conceptuelle d’une chaîne de blocs. Crédit : UM Ingénierie

Dans une étape importante pour garantir que les protocoles qui dictent le fonctionnement de nos services en réseau sont sûrs, sécurisés et fonctionnent comme prévu, les chercheurs de l’Université du Michigan ont automatisé une technique appelée vérification formelle.

Leur système prouve, sans aucun effort humain, que l’un des protocoles informatiques distribués les plus fondamentaux, connu sous le nom de Paxos, répond à ses spécifications. La réalisation réfute une hypothèse commune selon laquelle le protocole Paxos et d’autres du même genre sont trop complexes pour être prouvés sûrs sans des heures de travail manuel.

« Paxos est l’une des premières et des plus célèbres idées qui ont jeté les bases de la façon dont différentes choses parviennent à un accord de manière asynchrone », a déclaré Aman Goel, doctorant en informatique et en ingénierie, qui a présenté le travail à la Formal Methods in Computer- Conférence de conception assistée le 20 octobre.

La domination du cloud computing et les technologies croissantes telles que les applications blockchain ont changé la façon dont les organisations et les individus s’impliquent dans l’informatique, créant un monde alimenté par des machines en réseau sous une charge sans cesse croissante.

En conséquence, notre infrastructure critique est plus que jamais sensible aux retombées généralisées des pannes de serveur, des pirates et du comportement de réseau bogué. Des protocoles distribués étanches sont nécessaires pour garantir que les systèmes logiciels peuvent fonctionner efficacement sur des machines réparties dans le monde entier.

Ces protocoles sont des algorithmes extrêmement complexes qui définissent comment les machines d’un réseau peuvent travailler en collaboration en tant que système unique. Paxos est l’un des exemples les plus importants de la catégorie, décrivant une approche appelée consensus qui a été utilisée dans presque tous les systèmes distribués critiques, y compris toutes les applications prises en charge par le cloud computing.

Plus récemment, le consensus a suscité une large attention pour l’activation d’applications blockchain telles que les crypto-monnaies. De tels protocoles forment l’épine dorsale d’une blockchain en aidant tous les nœuds du réseau à vérifier les transactions au fur et à mesure qu’elles se produisent.

« La plupart des algorithmes de consensus, sinon tous, dérivent fondamentalement des concepts de Paxos », a déclaré Goel.

La vérification formelle est une classe de techniques utilisées pour démontrer que quelque chose est correct et fiable avec l’élégance d’une preuve logique. Le processus est très utile pour les logiciels et le matériel, fournissant un certificat qu’un certain algorithme, un logiciel ou une puce informatique fonctionnera toujours comme ses spécifications l’indiquent. Théoriquement, cela permettrait de publier des logiciels avec beaucoup moins de tests que ce qui est actuellement nécessaire.

« Avoir un système infaillible qui dit : vous le développez, vous le vérifiez automatiquement et vous obtenez un certificat d’exactitude, c’est ce qui vous donne l’assurance que vous pouvez déployer un programme sans problème », a déclaré Karem Sakallah, professeur d’informatique et d’ingénierie.

Malheureusement, prouver l’exactitude d’un programme avec de nombreux comportements complexes va de fastidieux à impossible, ce qui rend les techniques naissantes pour automatiser le processus extrêmement puissantes. Mais pour les algorithmes à l’échelle de Paxos, l’automatisation de sa vérification formelle était considérée comme un travail tout simplement trop important pour être terminé avec succès.

« Il y a eu de nombreuses tentatives dans le passé pour vérifier Paxos, y compris de nombreuses tentatives manuelles », a déclaré Goel. « Tout le monde pointe vers un résultat théorique antérieur qui dit que l’automatisation est impossible – c’est au-delà des outils d’automatisation de pouvoir le prouver. »

La solution de l’équipe utilise une fonctionnalité commune à tous les protocoles distribués : la régularité. Dans les systèmes considérés, tous les serveurs travaillant sur une fonction particulière traiteront de gros lots de requêtes qui se ressemblent fondamentalement, et la nature de leurs tâches changera très peu au fil du temps.

Cette régularité a permis à Goel et Sakallah de transformer ce qui a commencé comme une tâche incroyablement grande en une tâche qui semble petite et gérable. Ils l’ont fait littéralement – en vérifiant le protocole en supposant qu’il avait un petit nombre de nœuds fixe, puis en généralisant la solution à un « nombre théoriquement illimité » de nœuds.

L’outil que les chercheurs ont conçu pour cette preuve s’appelle IC3PO, un système de vérification de modèle qui examine chaque état dans lequel un programme peut entrer et détermine s’il correspond à une description de comportement sûr. Si le protocole est correct, IC3PO produit ce qu’on appelle un invariant inductif, une preuve par induction que la propriété est valable dans tous les cas. Si à la place un bogue est trouvé dans le protocole, il produira un contre-exemple et une trace d’exécution, montrant étape par étape comment le bogue se manifeste.

L’invariant inductif IC3PO produit pour Paxos en moins d’une heure correspond à l’identique à celui écrit par l’homme précédemment dérivé avec un effort manuel important en utilisant une technique appelée preuve interactive de théorème. En plus d’accélérer le processus, il produit également une preuve avec une documentation très succincte et digeste.

Vérifier l’exactitude de Paxos a automatiquement des ramifications majeures pour l’avenir. Alors que de nouveaux protocoles de consensus sont construits sur ses principes pour des applications en constante évolution, ils devront être prouvés sûrs et sécurisés. L’utilisation d’un vérificateur de modèle comme celui-ci peut permettre aux humains de travailler avec un logiciel complexe qui s’est avéré sûr sans avoir à comprendre chaque détail mineur de son fonctionnement.


Construire un avenir sans tests


Plus d’information:
Vers une preuve automatique de Paxos de Lamport, arXiv:2108.08796 [cs.LO], arxiv.org/abs/2108.08796

Fourni par l’Université du Michigan

Citation: Protocole distribué sous-tendant le cloud computing automatiquement déterminé sûr et sécurisé (2021, 25 octobre) récupéré le 25 octobre 2021 à partir de https://techxplore.com/news/2021-10-protocol-underpinning-cloud-automatically-safe.html

Ce document est soumis au droit d’auteur. En dehors de toute utilisation équitable à 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.