Les pratiques d’Amazon Web Services en matière de correction des systèmes

• AWS considère la correction des systèmes comme un fondement essentiel pour préserver la sécurité, la durabilité, l’intégrité et la disponibilité, et a élargi son champ d’application en passant de TLA+ à la vérification de modèles, au fuzzing, aux tests fondés sur des propriétés, à la vérification à l’exécution et jusqu’aux preuves formelles
• TLA+ a permis d’éliminer très tôt des bugs difficiles à détecter avec les tests traditionnels et d’apporter de la confiance dans les optimisations de performance, mais pour améliorer l’accessibilité aux développeurs, des outils comme le langage de programmation P et PObserve ont aussi été introduits
• Les tests fondés sur des propriétés de S3 ShardStore, la simulation déterministe et le fuzzing SQL d’Aurora Limitless Database illustrent comment les méthodes formelles ont été rapprochées du développement quotidien et des tests d’intégration
• Fault Injection Service valide les mécanismes de résilience en injectant des pannes comme des erreurs d’API, des pauses d’E/S ou des défaillances d’instance, et Amazon.com a exécuté 733 expériences basées sur FIS lors de la préparation de Prime Day 2024
• Dans des domaines où les frontières de sécurité et les optimisations de performance sont cruciales, comme Cedar, Firecracker ou l’optimisation RSA sur Graviton 2, des preuves formelles sont utilisées, même si la courbe d’apprentissage élevée et l’accessibilité des outils restent des freins à l’adoption

---

Comment AWS aborde la correction des systèmes

• AWS estime que, pour fournir des services dignes de confiance à ses clients, il faut maintenir des standards élevés de sécurité, durabilité, intégrité et disponibilité, et la correction des systèmes soutient cet objectif
• L’article de 2015 du CACM, « How Amazon Web Services Uses Formal Methods », présentait l’approche utilisée pour garantir la correction des services centraux d’AWS, et ces services sont depuis largement utilisés par les clients AWS
• L’outil central au départ était TLA+, le langage de spécification formelle développé par Leslie Lamport
  • Il aide à détecter et éliminer très tôt dans le développement des bugs subtils que les tests traditionnels peuvent laisser passer
  • Il apporte de la confiance dans la possibilité de mettre en œuvre des optimisations de performance agressives tout en préservant la correction du système
• Il y a 15 ans, les pratiques de test d’AWS reposaient principalement sur des tests unitaires au moment du build et sur des tests d’intégration limités au moment du déploiement
• Depuis, AWS a intégré des méthodes formelles et semi-formelles dans le processus de développement
  • preuve de théorèmes, vérification déductive, vérification de modèles
  • tests fondés sur des propriétés, fuzzing, monitoring à l’exécution

Le langage de programmation P et PObserve

• Lorsque AWS a cherché au début des années 2010 à étendre les méthodes formelles au-delà des équipes pionnières, l’entreprise a constaté que de nombreux ingénieurs avaient du mal à apprendre TLA+ et à devenir productifs avec cet outil
• La force de TLA+ réside dans son langage abstrait de haut niveau, proche des mathématiques, mais cela crée aussi une barrière d’accès pour des développeurs habitués aux langages impératifs
• Le langage P, fondé sur des machines à états pour la modélisation et l’analyse des systèmes distribués, sert à réduire cet écart
  • Les développeurs modélisent la conception du système sous forme de machines à états communicantes
  • Ce modèle mental est familier aux développeurs Amazon qui travaillent beaucoup avec les microservices et l’architecture orientée services (SOA)
  • P est développé chez AWS depuis 2019 et maintenu comme projet open source stratégique
• Plusieurs équipes produit majeures d’AWS utilisent P pour examiner la correction de leurs conceptions système
  • stockage : Amazon S3, EBS
  • bases de données : Amazon DynamoDB, MemoryDB, Aurora
  • calcul : EC2, IoT
• S3 a utilisé P lors de sa transition de l’eventual consistency vers la strong read-after-write consistency
  • Le sous-système d’index de S3 est le dépôt de métadonnées d’objets qui permet des recherches rapides
  • Atteindre une forte cohérence a nécessité plusieurs changements non triviaux dans la pile de protocoles d’indexation de S3
  • P permet de modéliser et vérifier formellement la conception du protocole, d’éliminer tôt les bugs de conception et de valider par model checking des optimisations risquées
• En 2023, l’équipe P d’AWS a créé PObserve
  • Il utilise des journaux structurés issus de l’exécution des systèmes distribués
  • Il vérifie a posteriori que les journaux sont cohérents avec les comportements autorisés par la spécification formelle P du système
  • Il réduit l’écart entre les implémentations de production écrites en Rust ou Java et les spécifications P définies à la conception
  • Il relie la vérification au moment de la conception et le monitoring à l’exécution des implémentations, augmentant la valeur des investissements dans les spécifications formelles

Intégrer des méthodes formelles légères dans le flux de développement

• AWS a introduit des méthodes formelles légères pour rapprocher les méthodes formelles des flux de développement et de test des équipes d’ingénierie

• Tests fondés sur des propriétés

  • ShardStore d’Amazon S3 utilise des tests fondés sur des propriétés tout au long du cycle de développement pour tester la correction et accélérer le rythme de développement
  • Plusieurs techniques sont combinées pour permettre aux humains de spécifier le comportement attendu, tandis que des tests automatisés explorent davantage d’entrées et de conditions d’échec
    • spécifications de correction fournies par les développeurs
    • fuzzing guidé par la couverture, avec distribution des entrées pilotée par les métriques de couverture du code
    • injection de pannes pour simuler pendant les tests des défaillances matérielles et d’autres systèmes
    • minimisation automatique des contre-exemples pour faciliter le débogage humain

• Simulation déterministe

  • Les tests par simulation déterministe exécutent un système distribué dans un simulateur mono-thread et contrôlent toutes les sources d’aléa
    • ordonnancement des threads
    • timing
    • ordre de livraison des messages
  • Les développeurs peuvent écrire des scénarios précis de succès ou d’échec, comme la défaillance d’un participant à une étape particulière d’un protocole distribué
  • Comme le framework de test contrôle la non-détermination, il permet de spécifier des ordres d’exécution intéressants, par exemple ceux qui ont déjà déclenché des bugs
  • L’ordonnanceur peut être étendu au fuzzing d’ordonnancement ou à l’exploration de tous les ordres possibles
  • Cela rapproche les tests de propriétés système en situation de latence ou de panne du moment du build plutôt que des tests d’intégration, accélérant le développement et élargissant la couverture comportementale
  • Une partie des travaux d’AWS sur les tests au moment du build liés à l’ordre des threads et aux défaillances système a été publiée en open source via les projets shuttle et turmoil

• Fuzzing continu et génération aléatoire d’entrées de test

  • Le fuzzing continu, notamment la génération extensible d’entrées guidée par la couverture, est efficace pour tester la correction des systèmes au moment de l’intégration
  • Dans le développement de Aurora Limitless Database, la fonctionnalité de sharding des données d’Amazon Aurora, le fuzzing a été largement utilisé pour vérifier deux propriétés clés
  • Des requêtes SQL et des transactions complètes sont fuzzées afin de vérifier que la séparation logique de l’exécution SQL entre shards est correcte
  • De grands volumes de schémas SQL, jeux de données et requêtes aléatoires sont synthétisés, exécutés sur le moteur testé, puis comparés à un oracle fondé sur un moteur non shardé
  • D’autres approches de vérification sont aussi utilisées, comme celle popularisée par SQLancer
  • La combinaison du fuzzing et des tests par injection de panne est également utile pour des aspects de correction des bases de données comme l’atomicité, la cohérence et l’isolation
    • génération automatique de transactions
    • définition du comportement correct via un oracle de correction formellement spécifié
    • exécution sur le système testé des interleavings possibles entre transactions et entre instructions au sein des transactions
    • vérification a posteriori de propriétés comme l’isolation, selon une approche proche d’Elle

Fault Injection Service et la validation en situation de panne

• AWS a lancé début 2021 Fault Injection Service (FIS), rendant les tests fondés sur l’injection de pannes accessibles à un large éventail de clients AWS
• FIS peut injecter des pannes simulées dans des déploiements de test ou de production sur l’infrastructure AWS
  • erreurs d’API
  • pauses d’E/S
  • instances défaillantes
• L’injection de pannes permet de vérifier que les mécanismes de résilience intégrés dans l’architecture améliorent réellement la disponibilité sans créer de nouveaux problèmes de correction
  • basculement
  • health checks
• Les tests d’injection de panne reposant sur FIS sont largement utilisés par les clients AWS et en interne chez Amazon
• Amazon.com a exécuté 733 expériences d’injection de panne basées sur FIS lors de la préparation de Prime Day 2024
• En 2014, Yuan et ses collègues ont analysé que 92 % des pannes fatales dans les systèmes distribués testés étaient déclenchées par une mauvaise gestion d’erreurs non fatales
• Si les pannes fatales sur le chemin nominal sont rares, c’est parce que ce chemin est exécuté fréquemment, mieux testé et bien plus simple que les chemins d’erreur
• Les tests par injection de panne et FIS facilitent les tests du comportement système en cas de panne ou de défaillance, réduisant l’écart de densité de bugs entre chemin nominal et chemin d’erreur
• L’injection de panne n’est pas en soi considérée comme une méthode formelle, mais elle peut être combinée à des spécifications formelles
  • définir le comportement attendu via une spécification formelle
  • comparer les résultats pendant et après l’injection de panne avec le comportement spécifié
  • détecter davantage de bugs qu’une simple vérification de métriques, d’erreurs dans les logs ou une inspection manuelle

Métastabilité et comportements système émergents

• Au cours des dix dernières années, l’attention portée à une classe particulière de pannes système, les pannes métastables (metastable failures), a fortement augmenté
• Une panne métastable survient lorsqu’un déclencheur comme une surcharge ou une purge de cache pousse un système distribué dans un état dont il ne peut pas se remettre sans intervention
  • Un exemple d’intervention consiste à réduire la charge en dessous du niveau normal
• Cette classe de pannes est l’un des facteurs majeurs d’indisponibilité dans les systèmes cloud
• Dans un comportement métastable typique, le goodput augmente d’abord avec la charge, puis sature, passe par une phase de congestion, et finit par tomber à zéro ou presque
• Ensuite, le système ne retrouve pas un état sain avec une simple légère baisse de charge ; il faut réduire fortement la charge pour qu’il se rétablisse
• Ce comportement peut apparaître même dans des systèmes simples et peut être déclenché dans la plupart des systèmes par une logique client de retry après timeout
• La modélisation formelle traditionnelle des systèmes distribués se concentre en général sur la safety et la liveness, mais les pannes métastables montrent qu’il existe des comportements qui ne s’intègrent pas proprement dans cette classification
• AWS utilise davantage la simulation à événements discrets pour comprendre les comportements émergents des systèmes
  • investissement dans des simulations système sur mesure
  • investissement dans des outils permettant d’utiliser en simulation des modèles système existants écrits dans des langages comme TLA+ et P
• Étendre un model checker à exploration exhaustive comme TLC de TLA+ avec de la simulation probabiliste permet de produire des résultats statistiques, comme des distributions de latence a posteriori
• De telles extensions permettent d’utiliser le model checking pour comprendre, par exemple, la probabilité d’atteindre des SLA de latence

Des frontières de sécurité qui exigent des preuves formelles

• Sur des frontières de sécurité importantes comme l’autorisation ou la virtualisation, les méthodes formelles précédentes peuvent ne pas suffire, et la preuve de correction peut justifier un investissement important

• Le langage de politiques d’autorisation Cedar

  • AWS a introduit en 2023 le langage de politiques d’autorisation Cedar pour écrire des politiques définissant des permissions fines
  • Cedar a été conçu en tenant compte du raisonnement automatique et de la preuve formelle
  • L’implémentation a été construite en Dafny, un langage de programmation favorable à la vérification
  • Dafny a permis de prouver que l’implémentation satisfait plusieurs propriétés de sécurité
  • Il s’agit ici d’une preuve au sens mathématique, au-delà des simples tests
  • L’équipe a aussi appliqué des tests différentiels utilisant le code Dafny comme oracle de correction afin de valider la correction de l’implémentation Rust prête pour la production
  • Avec l’implémentation de Cedar, AWS a publié en open source le code Dafny et les procédures de test afin que les utilisateurs puissent examiner le travail de correction

• Le VMM Firecracker

  • Le moniteur de machine virtuelle Firecracker utilise un protocole bas niveau appelé virtio pour exposer au noyau invité dans la VM des périphériques matériels émulés comme des cartes réseau ou des SSD
  • Ces périphériques émulés constituent l’interaction la plus complexe entre un invité non fiable et un hôte de confiance, ce qui en fait une frontière de sécurité critique
  • L’équipe Firecracker utilise Kani, qui permet de raisonner formellement sur du code Rust, pour prouver des propriétés clés de cette frontière de sécurité
  • Cette preuve garantit que, quoi que tente l’invité, les propriétés essentielles de la frontière restent préservées
  • AWS soutient le développement d’outils de base comme Kani, Dafny, Lean et les solveurs SMT qui les alimentent
  • Les modèles et spécifications formels sont réutilisés de plusieurs façons
    • vérification de modèles à la conception
    • rôle d’oracle de correction dans le monitoring à l’exécution
    • simulation de comportements système émergents
    • construction de preuves de propriétés essentielles

Au-delà de la correction : performance et efficacité économique

• Les méthodes formelles sont aussi importantes pour améliorer en toute sécurité les performances des systèmes cloud
• La modélisation en P et TLA+ du protocole central de commit du moteur de base de données relationnelle Aurora a permis d’identifier une opportunité de réduire le coût du commit distribué de 2 allers-retours réseau à 1,5 aller-retour réseau sans sacrifier les propriétés de sécurité
• Ce type de résultat est fréquent dans les équipes qui adoptent les méthodes formelles
  • Le fait de réfléchir en profondeur à un protocole distribué et de l’écrire formellement impose une pensée structurée
  • Cela apporte une compréhension plus fine de la structure du protocole et du problème à résoudre
  • Si l’on peut vérifier ou prouver formellement qu’une optimisation de conception proposée est correcte, les ingénieurs en systèmes distribués peuvent choisir des conceptions plus audacieuses sans augmenter le risque
• Les gains de productivité et d’efficacité économique ne se limitent pas aux optimisations de haut niveau
• Les équipes AWS ont trouvé une optimisation pour l’implémentation du chiffrement à clé publique RSA sur les processeurs ARM Graviton 2, permettant d’améliorer le débit jusqu’à 94 %
• La correction de cette optimisation a été prouvée à l’aide du démonstrateur de théorèmes interactif HOL Light
• Comme une part élevée des cycles CPU du cloud est consacrée au chiffrement, ce type d’optimisation peut contribuer à réduire les coûts d’infrastructure, à soutenir les objectifs de durabilité et à améliorer les performances perçues par les clients

Défis restants et opportunités futures

• AWS a réussi à étendre les méthodes de test formelles et semi-formelles au cours des 15 dernières années, mais l’adoption industrielle reste confrontée à plusieurs défis
• Les principaux obstacles des outils de méthodes formelles restent une courbe d’apprentissage raide et le besoin de connaissances spécialisées du domaine
• Beaucoup d’outils conservent encore une forte dimension académique et manquent d’interfaces conviviales
• Même des approches semi-formelles bien établies rencontrent encore des barrières à l’adoption
  • La simulation déterministe est une technique centrale de test des systèmes distribués utilisée avec succès chez AWS et dans des projets comme FoundationDB, mais elle reste parfois peu familière même pour des développeurs expérimentés en systèmes distribués qui rejoignent AWS
  • Le même décalage existe pour des méthodologies éprouvées comme les tests par injection de panne, les tests fondés sur des propriétés ou le fuzzing
• Il est nécessaire de former les développeurs de systèmes distribués à ces méthodes de test, à ces outils et à des modes de pensée rigoureux
• Le déficit de formation commence dès le monde académique
  • Les approches de base du raisonnement formel sont rarement enseignées
  • Même les diplômés d’établissements de premier plan ont du mal à adopter ces outils
  • Les méthodes formelles et le raisonnement automatique sont importants pour les usages industriels, mais restent perçus comme des domaines de niche
• La métastabilité et d’autres propriétés émergentes des systèmes à grande échelle constituent aussi un domaine de recherche important confronté à des défis de sensibilisation similaires
  • Des pratiques comme « retry N fois après timeout », pourtant connues pour pouvoir déclencher des comportements métastables, continuent d’être largement recommandées
  • Les outils et techniques actuels pour comprendre les comportements émergents des systèmes en sont encore à un stade précoce
  • La modélisation de la stabilité des systèmes est coûteuse et complexe
• AWS estime que les grands modèles de langage et les assistants IA pourraient contribuer de manière significative à atténuer les difficultés d’adoption pratique des méthodes formelles
  • Comme les tests unitaires assistés par IA ont gagné en popularité, ces outils pourraient aider les développeurs à créer des modèles et des spécifications formels
  • Des techniques avancées pourraient ainsi devenir accessibles à une communauté de développeurs beaucoup plus large

Le cadre de correction dans lequel AWS continue d’investir

• Produire des logiciels fiables et sûrs exige une variété d’approches pour raisonner sur la correction des systèmes
• AWS adopte plusieurs techniques en complément des tests standard de l’industrie, comme les tests unitaires et les tests d’intégration
  • vérification de modèles
  • fuzzing
  • tests fondés sur des propriétés
  • tests par injection de panne
  • simulation déterministe
  • simulation événementielle
  • vérification à l’exécution des traces d’exécution
• Les spécifications formelles jouent un rôle important d’oracle de test, fournissant la bonne réponse dans plusieurs pratiques de test d’AWS
• Fortes du retour sur investissement déjà obtenu, les pratiques de test de correction et les méthodes formelles restent un domaine d’investissement central pour AWS