Pratiques de correction des systèmes chez AWS : Levier des méthodes formelles et semi-formelles
Amazon Web Services (AWS) s'efforce de fournir des services fiables auxquels les clients peuvent entièrement faire confiance. Cela exige le maintien des normes les plus élevées en matière de sécurité, de durabilité, d'intégrité et de disponibilité, la correction des systèmes servant de pierre angulaire pour atteindre ces priorités. Initialement, AWS a utilisé le langage TLA+ pour modéliser des systèmes critiques, identifiant et éliminant des bogues subtils en amont. Avec sa croissance, AWS a introduit le langage de programmation P, plus convivial pour les développeurs, pour modéliser et analyser des systèmes distribués, essentiel pour des migrations comme celle d'Amazon S3 vers une forte cohérence. Des méthodes légères, telles que les tests basés sur les propriétés, la simulation déterministe et le fuzzing, sont également largement utilisées. AWS a également lancé FIS (Fault Injection Service) pour améliorer la résilience. Pour les limites de sécurité critiques, AWS utilise des preuves formelles, comme dans le développement de Cedar et Firecracker. Cette approche garantit la fiabilité et l'optimisation des performances, réduisant les coûts.