- Amazon Web Services (AWS) place la justesse de ses services au rang de valeur fondamentale et intègre plusieurs formes de méthodes formelles dans son processus de développement
- Grâce à des outils de spécification formelle comme TLA+ et le langage P, l’entreprise peut détecter très tôt des bugs subtils et garantir la fiabilité même lors d’optimisations ambitieuses
- AWS déploie aussi largement des méthodologies formelles allégées comme les tests basés sur les propriétés, la simulation déterministe et le fuzzing continu
- Avec des outils d’injection de pannes comme Fault Injection Service, l’automatisation de la validation de la fiabilité s’étend jusqu’aux situations d’incident
- Malgré des barrières pédagogiques et la complexité persistante des outils, la diffusion de l’IA et des outils d’automatisation devrait favoriser une adoption plus large
La stratégie d’AWS pour garantir la justesse des systèmes
Amazon Web Services (AWS) vise à fournir des services hautement fiables auxquels les clients peuvent accorder une confiance totale
Pour cela, l’entreprise cherche à maintenir des critères de sécurité, durabilité, intégrité et disponibilité, en plaçant au centre la notion de justesse des systèmes
Depuis la présentation en 2015 dans Communications of the ACM d’un cas d’usage des méthodes formelles chez AWS, cette approche joue un rôle important dans l’exploitation réussie de services critiques
Au cœur de cette démarche se trouve TLA+, un langage de spécification formelle développé par Leslie Lamport
L’expérience d’AWS avec TLA+ a permis d’identifier dès les premières étapes du développement des bugs subtils que les tests classiques ne détectaient pas
Elle a aussi permis d’assurer stabilité et fiabilité, même lors d’optimisations de performances audacieuses, grâce à la vérification formelle
Il y a 15 ans, AWS se limitait encore à des pratiques de base comme les tests unitaires au moment du build et des tests d’intégration restreints, puis a progressivement adopté de façon large des approches formelles et semi-formelles
Cette évolution a contribué non seulement à la justesse, mais aussi à la validation des optimisations de haut et de bas niveau, à l’accélération du développement et à la réduction des coûts
Chez AWS, le périmètre des méthodes formelles ne se limite pas aux preuves formelles et au model checking : il inclut aussi les tests basés sur les propriétés, le fuzzing et le monitoring à l’exécution
L’émergence du langage de programmation P
Au départ, TLA+ présentait l’avantage d’une expression abstraite très puissante, mais pour de nombreux développeurs, la notation mathématique constituait une barrière d’entrée importante
AWS a donc adopté le langage P, qui propose une approche fondée sur les machines à états, plus familière pour les développeurs
Le langage P fournit une méthode de modélisation par machines à états pour la conception et l’analyse des systèmes distribués
C’est un concept familier pour les développeurs Amazon travaillant avec des architectures SOA basées sur les microservices
Il est développé et géré depuis 2019 chez AWS comme projet open source stratégique
Des équipes de services majeurs comme Amazon S3, EBS, DynamoDB, Aurora, EC2 et IoT utilisent P pour vérifier la justesse de leurs conceptions système
Lors du passage de S3 à une forte cohérence read-after-write, le protocole a été modélisé et vérifié avec P, ce qui a permis d’éliminer des bugs dès la phase initiale de conception et d’intégrer des optimisations de manière sûre
En 2023, l’équipe AWS P a développé l’outil PObserve, qui permet de vérifier la justesse des systèmes distribués aussi bien dans les tests qu’en environnement de production réel
PObserve extrait les logs d’exécution afin de permettre une vérification a posteriori du bon comportement au regard de la spécification, et relie efficacement les spécifications de conception à l’implémentation réelle du code
Extension des méthodologies formelles allégées
Tests basés sur les propriétés
La technique formelle allégée la plus représentative est celle des tests basés sur les propriétés
Par exemple, l’équipe de développement de ShardStore pour S3 combine tout au long du cycle de développement tests basés sur les propriétés, fuzzing guidé par la couverture de code, injection de pannes et minimisation de contre-exemples
Cette approche s’articule avec les spécifications de justesse rédigées directement par les développeurs et améliore fortement l’efficacité du débogage
Simulation déterministe
Les tests par simulation déterministe exécutent un système distribué dans un simulateur mono-thread, ce qui permet de contrôler tous les éléments aléatoires comme l’ordonnancement, le timing ou l’ordre des messages
Ils sont appliqués de multiples façons : test de scénarios précis d’échec et de réussite, ajustement des séquences déclenchant des bugs, extension du fuzzing, etc.
Cela permet de vérifier très tôt dans la phase de build le comportement du système en présence de latence ou de panne, tout en élargissant la couverture des tests
AWS a publié ce code de test utilisé au build sous forme des projets open source shuttle et turmoil
Fuzzing continu
Le fuzzing continu, en particulier la génération massive d’entrées basée sur la couverture de code, est efficace pour vérifier la justesse d’un système au stade des tests d’intégration
Par exemple, lors du développement d’Aurora Limitless Database, des requêtes SQL et des transactions ont été soumises à du fuzzing afin de vérifier la justesse de la logique de partitionnement via la génération de grands volumes de schémas, jeux de données et requêtes aléatoires
Les résultats sont comparés soit au comportement du moteur non sharded, soit à des méthodes telles que SQLancer
La combinaison du fuzzing et de l’injection de pannes permet de vérifier des propriétés essentielles des bases de données comme l’atomicité, la cohérence et l’isolation
Certaines propriétés, comme les transactions générées automatiquement ou l’isolation, sont garanties par une vérification a posteriori fondée sur l’historique d’exécution
Injection de pannes avec Fault Injection Service
En 2021, AWS a lancé Fault Injection Service (FIS), permettant aussi aux clients d’expérimenter rapidement dans des environnements réels ou de test divers scénarios de défaillance, comme des erreurs d’API, des interruptions d’E/S ou des pannes d’instance
Cela aide à garantir la disponibilité des architectures et à vérifier leur résilience, à réduire l’écart de densité de bugs entre cas normaux et cas d’erreur, et à détecter à l’avance des problèmes graves très probables
FIS est largement utilisé aussi bien par les clients AWS qu’en interne chez Amazon ; par exemple, 733 expérimentations ont été menées rien que lors de la préparation du Prime Day
L’injection d’erreurs est encore plus efficace lorsqu’elle est combinée à des spécifications formelles
Après avoir rédigé le comportement attendu sous forme de spécification formelle, on peut comparer à celle-ci les résultats provoqués par des défaillances réelles, ce qui permet de détecter davantage d’erreurs qu’avec de simples vérifications de logs ou de métriques
Métastabilité et comportements émergents des systèmes
Dans les systèmes distribués, les cas où une surcharge excessive, un épuisement du cache ou d’autres facteurs entraînent un état anormal « impossible à auto-réparer » — un état métastable — sont de plus en plus fréquents
Dans cet état, une simple baisse de charge ne suffit pas à rétablir un fonctionnement normal, et la réponse à apporter est plus difficile que pour des cas d’erreur ordinaires
La plupart des logiques de retry et de timeout sont aussi à l’origine de ce phénomène
Les spécifications formelles classiques se concentrent sur la sûreté et la progression, mais la métastabilité impose de prendre en compte une variété plus large de comportements émergents
AWS s’appuie sur des modèles de spécification comme TLA+ et P pour effectuer des simulations à événements discrets et analyser de manière systématique jusqu’aux caractéristiques probabilistes, comme la capacité à respecter les SLA de performance ou la distribution des latences
La nécessité des preuves formelles
Pour certaines frontières de sécurité — comme les autorisations ou la virtualisation — une preuve de niveau mathématique, au-delà de simples tests, est indispensable
Par exemple, le langage de politique d’autorisation Cedar, introduit par AWS en 2023, est optimisé pour la preuve automatique et la vérification formelle sur une base Dafny, et son code public ainsi que sa procédure de correction permettent à l’ensemble des utilisateurs de procéder eux-mêmes à la vérification
Par ailleurs, pour les propriétés de sécurité clés du VMM Firecracker, des travaux de preuve sont menés avec des outils d’analyse de code Rust tels que Kani
Ainsi, l’utilisation étendue de modèles et de spécifications formels à différents moments — conception, implémentation, exécution et preuve — sert à garantir la justesse logicielle et à accroître la valeur pour l’entreprise comme pour les clients
Des effets positifs au-delà de la justesse
Les méthodes formelles jouent un rôle majeur tant dans la fiabilité que dans l’amélioration des performances
Par exemple, le protocole de commit d’Aurora a été vérifié avec P et TLA+, ce qui a permis de réduire le nombre d’allers-retours réseau tout en garantissant la sûreté
Lors de l’optimisation de l’algorithme de chiffrement RSA pour ARM Graviton 2, la justesse mathématique des transformations a été prouvée dans HOL Light, produisant un effet concret : amélioration simultanée des performances et des coûts d’infrastructure
Défis et opportunités pour l’avenir
En 15 ans, AWS a fortement élargi l’application industrielle des méthodologies formelles et semi-formelles, mais des freins à l’adoption très concrets persistent : courbe d’apprentissage, besoin d’expertise et nature académique des outils
Même les tests basés sur les propriétés ou la simulation déterministe restent encore peu familiers à de nombreux développeurs
Comme la barrière éducative existe dès le cursus universitaire, la diffusion des outils et des méthodes ainsi que leur adoption en pratique avancent lentement
Les propriétés émergentes des systèmes à grande échelle, comme la métastabilité, n’en sont encore qu’aux premiers stades de la recherche
À l’avenir, l’IA et les grands modèles de langage devraient aider à rédiger des modèles et spécifications formels, ce qui pourrait améliorer radicalement l’accessibilité pour les praticiens à court terme
Conclusion
Construire des logiciels robustes et sûrs exige divers moyens pour garantir la justesse des systèmes
Au-delà des techniques de test classiques, AWS a adopté de manière large le model checking, le fuzzing, les tests basés sur les propriétés, les tests d’injection de pannes, les simulations déterministes et orientées événements, ainsi que la vérification des historiques d’exécution
Les spécifications et méthodologies formelles jouent le rôle d’oracle de test important dans le processus de développement d’AWS et, leurs effets concrets et économiques ayant déjà été démontrés, elles se sont imposées comme un domaine d’investissement à part entière
1 commentaires
Avis Hacker News
J’aimerais parler de l’approche des tests par simulation déterministe. Chez AWS, ils exécutent des systèmes distribués dans un simulateur mono‑thread tout en contrôlant tous les éléments non déterministes comme l’ordonnancement des threads, le timing ou l’ordre de livraison des messages. Ils écrivent ensuite des tests ciblant des scénarios précis d’échec ou de réussite, et c’est le framework de test qui contrôle la non‑déterminisme du système. Les développeurs peuvent spécifier des séquences particulières ayant déjà provoqué des bugs. L’ordonnanceur peut même être étendu pour faire du fuzzing des séquences ou explorer toutes les séquences possibles. Je me demande s’il existe une bibliothèque open source, indépendante du langage, qui implémente ce genre de chose. L’idée serait d’avoir un outil intermédiaire qui rende aussi « déterministes » au moment du test des éléments comme le réseau ou le stockage dans des conteneurs. antithesis joue presque ce rôle, mais je ne l’ai pas encore vu en open source. Avec de bons tests, on peut résoudre une partie du problème en remplaçant l’I/O par des stubs, mais rien ne garantit que tout le monde écrive bien ses tests. Je pense qu’il serait utile d’apporter le déterminisme à un niveau plus élevé, au‑dessus de l’application. D’un autre côté, j’espère que l’IA pourra vraiment briller dans les tests. Les trois axes prompt (exigences)‑implémentation des tests‑IA‑code exécutable pourraient idéalement s’articuler. J’espère aussi que l’IA rendra la vérification formelle plus accessible et fera du logiciel un domaine encore plus rigoureux
La diffusion des techniques de simulation déterministe de test (DST) se heurte à deux difficultés. Premièrement, historiquement, il fallait faire tourner tout le système directement sur un framework de simulation spécifique, sans autres dépendances. Deuxièmement, si la génération et l’exploration des entrées sont faibles, tous les tests peuvent sembler réussir sans fournir de vraie validation. antithesis essaie de résoudre ces deux problèmes à la fois, mais cela reste difficile. Il existe encore peu d’approches vraiment fiables pour appliquer le déterminisme à n’importe quel logiciel. Le projet Hermit de Facebook a aussi tenté la voie d’un espace utilisateur Linux déterministe, mais a fini par être abandonné. Les ordinateurs déterministes constituent une base technique très utile au‑delà des seuls tests, et je pense que quelqu’un finira par en publier une version open source
Je pense qu’il est relativement facile d’obtenir une machine déterministe en faisant tourner QEMU en mode 100 % émulation sur un seul thread. Mais ce qu’on veut vraiment, c’est une exécution déterministe « contrôlée », et c’est bien plus difficile. Faire fonctionner plusieurs processus selon un scénario donné est particulièrement complexe au niveau du CPU et de l’ordonnanceur de l’OS. Il est aussi difficile de construire un environnement lui‑même indépendant du langage, et on se retrouve vite piégé par les détails. J’ai moi‑même déjà construit un système simple où plusieurs threads JVM avançaient en lockstep à des points précis, avec l’I/O et l’horloge système remplacés par des stubs et des mécanismes de contrôle. Cela m’a permis de tester diverses interactions entre composants asynchrones, des pannes I/O, des retries, etc., et d’attraper des bugs pénibles avant la production. En revanche, cela n’était possible qu’en simplifiant certains points de synchronisation, pas en contrôlant tout le système. Cette approche a aussi du mal à attraper les data races classiques dues à des erreurs de synchronisation
Partage de la documentation officielle sur les méthodes de test de FoundationDB et d’une présentation vidéo sur YouTube
Si c’est un langage débogable avec gdb, je recommande le projet https://rr-project.org/
Je me souviens avoir vu autrefois une présentation de Joe Armstrong sur l’usage du property testing pour tester Dropbox
Je pense que S3 est l’un des logiciels les plus impressionnants que j’aie jamais vus. Le fait d’avoir ajouté il y a quelques années une forte cohérence en lecture‑après‑écriture à l’ensemble du système S3 me semble aussi être un sommet de l’ingénierie logicielle lien vers le billet de blog
J’ai directement travaillé sur le cycle de vie de S3, et cela coïncidait avec la période où l’équipe index repensait l’architecture pour fournir cette cohérence. Même vu de l’extérieur, S3 est impressionnant, mais en interne, l’implémentation comme l’organisation dépassent tout ce qu’on peut imaginer
Google Cloud Storage disposait en fait de cette fonctionnalité (forte cohérence) bien avant S3. Globalement, GCS donne aussi l’impression d’être un produit plus structuré et mieux conçu
Je suis d’accord avec le chiffre de 92 % (la plupart des pannes de cluster commencent par des échecs mineurs). Ce ne sont généralement pas les gros incidents spectaculaires, mais des retries « sans importance » qui accumulent de l’état jusqu’à exploser en panne majeure à 2 h du matin. Il est important d’allouer davantage de temps d’ingénierie à ces échecs peu visibles
Je trouve cet article vraiment intéressant. L’usage de machines à états pour construire des control planes d’infrastructure est indispensable. Je ne sais pas s’il fallait absolument P. De notre côté, nous avons aussi construit des control planes d’infrastructure en Ruby pendant plus de 13 ans, et cela fonctionne très bien retour d’expérience associé
J’avais une question sur le langage P. Il me semble qu’autrefois, chez Microsoft, P servait à générer du code C pour la stack USB de Windows en production réelle, mais qu’il n’est apparemment plus utilisé aujourd’hui pour générer du code de production. J’avais déjà posé la question sur Hacker News lien vers la question. Si du code généré pouvait même entrer dans le noyau, cela devrait clairement aussi être utilisable dans des environnements cloud soumis à des contraintes bien plus souples
En n’étant ni issu d’AWS ni familier avec TLA+ ou P, j’aurais trouvé plus facile à comprendre qu’il y ait au moins un exemple de type « hello world ». À lire le texte seul, cela peut donner l’impression d’un processus simplement douloureux, et on peut se demander si ce ne sont pas des problèmes qu’une bonne conception et de bons tests suffiraient à éviter. Un exemple simple aurait mieux aidé à juger ce qui est réellement fait
Il existe un exemple de démo rapide de TLA+ que j’aime bien lien vers le gist. Il modélise plusieurs threads qui incrémentent de façon non atomique un compteur partagé, et la vérification de propriétés y détecte une race condition. En pratique, ce genre de bug est très difficile à trouver uniquement par des tests. La plupart des spécifications TLA+ sont bien plus complexes, mais cet exemple est très bon pour montrer la capture d’erreurs simples
J’ai déjà essayé TLA moi‑même, mais j’ai été déçu de voir que l’outil graphique s’accordait mal avec le tutoriel. Je voulais pourtant vraiment utiliser TLA, et j’apprécie depuis longtemps le travail de Lamport, de LaTeX jusqu’aux articles
Le principe même des méthodes formelles repose finalement sur le fait qu’il est impossible d’attraper absolument tous les problèmes par les seuls tests
Je recommande le dépôt GitHub officiel TLA+ Examples. Je conseille de commencer par quelque chose de simple comme le problème de DieHard
Les tests prouvent la correction d’une implémentation pour certaines instances particulières d’un problème, tandis que la vérification formelle la prouve pour toute une classe. Par exemple, pour une fonction qui renvoie des anagrammes, les tests ne vérifient que quelques paires de mots, alors que prouver sa correction pour toutes les paires de mots nécessite de la formal verification. Des cas comme un undefined behavior ou des bugs de bibliothèque ne sont souvent détectés que lors d’un processus de formal verification
À propos de la mention des « techniques quasi formelles légères comme le property-based testing, le fuzzing et le runtime monitoring », j’ai l’impression que property-based testing et fuzzing sont bien des sous‑ensembles des méthodes formelles, mais inclure le runtime monitoring dans les techniques quasi formelles me paraît un peu excessif
J’ai autrefois eu des échanges avec Leslie Lamport autour d’articles sur le Buridan's Principle, entre autres. Aujourd’hui, j’ai beaucoup appris sur TLA+ et PlusCal via son site personnel page de l’exemple Peterson. Le fait qu’une personne qui a introduit les mathématiques dans la programmation, qui est l’une des figures fondatrices des systèmes concurrents, ait ensuite créé un langage de conception de systèmes (TLA+) utilisé chez AWS et ailleurs, me paraît parfaitement naturel. J’aimerais que davantage de personnes qui construisent des systèmes distribués utilisent ce que Lamport a créé. À grande échelle, prouver la correction est extrêmement important
Pour convertir du code existant en spécifications TLA+, Claude Opus (Extended Thinking) est très utile. Je l’ai déjà utilisé pour vérifier des projets Rust et des composants cœur en C++, et il y a trouvé plusieurs bugs. D’autres modèles butent souvent sur la syntaxe et la logique des specs, alors qu’Opus est beaucoup plus fluide
La preuve de correction n’est pas seulement utile pour les grands systèmes, mais aussi pour de petits utilitaires critiques comme SSH ou les terminaux, largement utilisés dans le monde entier
À propos de l’expression « prouver la correction du système », en pratique il est impossible de tout prouver. Un model checker peut seulement indiquer que, dans un espace d’états borné, la spécification décrite satisfait certaines propriétés
Je me demande si certains ont déjà utilisé FIS pour des expérimentations sur des services distribués. J’envisage son adoption, mais je n’ai pas encore d’expérience directe d’expériences à grande échelle
Je me demande si Promela et SPIN sont des langages de plus haut niveau que ce qui est décrit dans l’article