Prácticas de corrección de sistemas en Amazon Web Services

• AWS toma la corrección de sistemas como una base central para preservar la seguridad, durabilidad, integridad y disponibilidad, y ha ampliado su alcance de aplicación desde TLA+ hacia la verificación de modelos, fuzzing, pruebas basadas en propiedades, verificación en tiempo de ejecución y pruebas formales
• TLA+ ayudó a eliminar temprano bugs difíciles de detectar con pruebas tradicionales y dio confianza sobre las optimizaciones de rendimiento, pero para mejorar la accesibilidad para desarrolladores también se introdujeron herramientas como el lenguaje de programación P y PObserve
• Las pruebas basadas en propiedades de S3 ShardStore, la simulación determinista y el fuzzing de SQL de Aurora Limitless Database son ejemplos de cómo las técnicas formales se acercaron más al desarrollo cotidiano y a las pruebas de integración
• Fault Injection Service inyecta fallas como errores de API, pausas de I/O y fallas de instancias para validar mecanismos de resiliencia, y Amazon.com ejecutó 733 experimentos basados en FIS durante la preparación de Prime Day 2024
• En áreas donde los límites de seguridad y las optimizaciones de rendimiento son críticos, como Cedar, Firecracker y la optimización RSA de Graviton 2, se usan pruebas formales; la curva de aprendizaje elevada y la accesibilidad de las herramientas siguen siendo limitaciones para su adopción

---

Cómo AWS aborda la corrección de sistemas

• Para ofrecer servicios en los que los clientes puedan confiar, AWS debe mantener estándares altos de seguridad, durabilidad, integridad y disponibilidad, y la corrección de sistemas sostiene esos objetivos
• En 2015, el artículo de CACM “How Amazon Web Services Uses Formal Methods” presentó el enfoque para garantizar la corrección de los servicios centrales de AWS, que desde entonces pasaron a ser ampliamente usados por clientes de AWS
• La herramienta inicial central fue TLA+, un lenguaje de especificación formal desarrollado por Leslie Lamport
  • Ayuda a detectar y eliminar temprano, durante el desarrollo, bugs sutiles que podrían pasar desapercibidos con pruebas tradicionales
  • Da confianza para implementar optimizaciones de rendimiento agresivas manteniendo la corrección del sistema
• Hace 15 años, las prácticas de prueba de AWS dependían principalmente de pruebas unitarias en tiempo de build y de pruebas de integración limitadas en tiempo de despliegue
• Desde entonces, AWS integró técnicas formales y semiformalas en el proceso de desarrollo
  • Demostración de teoremas, verificación deductiva, verificación de modelos
  • Pruebas basadas en propiedades, fuzzing, monitoreo en tiempo de ejecución

El lenguaje de programación P y PObserve

• A comienzos de la década de 2010, al expandir las técnicas formales más allá de los equipos iniciales, AWS identificó que a muchos ingenieros les costaba aprender TLA+ y lograr productividad
• La fortaleza de TLA+ es ser un lenguaje abstracto de alto nivel, cercano a las matemáticas, pero eso se vuelve una barrera de entrada para desarrolladores acostumbrados a lenguajes imperativos
• El lenguaje basado en máquinas de estados P, para modelar y analizar sistemas distribuidos, cumple el papel de cerrar esa brecha
  • Los desarrolladores modelan el diseño del sistema como máquinas de estados que se comunican
  • Ese modelo mental es familiar para desarrolladores de Amazon que trabajan mucho con microservicios y arquitecturas orientadas a servicios (SOA)
  • P se desarrolla en AWS desde 2019 y se mantiene como proyecto open source estratégico
• Varios equipos de productos representativos de AWS usan P para revisar la corrección del diseño de sistemas
  • Almacenamiento: Amazon S3, EBS
  • Bases de datos: Amazon DynamoDB, MemoryDB, Aurora
  • Cómputo: EC2, IoT
• S3 usó P durante la migración de eventual consistency a strong read-after-write consistency
  • El subsistema de índices de S3 es un almacén de metadatos de objetos que permite búsquedas rápidas de datos
  • Para lograr consistencia fuerte fueron necesarios varios cambios no triviales en la pila de protocolos del índice de S3
  • P permitió modelar y verificar formalmente el diseño del protocolo para eliminar temprano bugs a nivel de diseño, y confirmar mediante verificación de modelos optimizaciones riesgosas
• En 2023, el equipo de AWS P construyó PObserve
  • Usa logs estructurados generados por ejecuciones de sistemas distribuidos
  • Verifica a posteriori si los logs coinciden con los comportamientos permitidos por la especificación formal en P del sistema
  • Reduce la brecha entre implementaciones de producción escritas en lenguajes como Rust o Java y las especificaciones en P definidas en tiempo de diseño
  • Aumenta el valor de la inversión en especificaciones formales al conectar la verificación en tiempo de diseño con el monitoreo en tiempo de ejecución de la implementación

Cómo acercar técnicas formales ligeras al flujo de desarrollo

• AWS adopta técnicas formales ligeras para acercar las técnicas formales al flujo de desarrollo y pruebas de los equipos de ingeniería

• Pruebas basadas en propiedades

  • ShardStore de Amazon S3 usa pruebas basadas en propiedades durante todo el ciclo de desarrollo para pruebas de corrección y para aumentar la velocidad de desarrollo
  • Combina varias técnicas para que las personas especifiquen el comportamiento esperado y las pruebas automatizadas exploren más entradas y condiciones de falla
    • Especificaciones de corrección provistas por desarrolladores
    • Fuzzing guiado por cobertura, que orienta la distribución de entradas mediante métricas de cobertura de código
    • Inyección de fallas, que simula durante las pruebas fallas de hardware y de otros sistemas
    • Minimización, que reduce automáticamente los contraejemplos para facilitar la depuración humana

• Simulación determinista

  • Las pruebas con simulación determinista ejecutan sistemas distribuidos en un simulador de un solo hilo y controlan todas las fuentes de aleatoriedad
    • Planificación de hilos
    • Tiempos
    • Orden de entrega de mensajes
  • Los desarrolladores pueden escribir escenarios específicos de falla o éxito, como situaciones en las que un participante falla en una etapa concreta de un protocolo distribuido
  • Como el framework de pruebas controla el no determinismo, se pueden especificar órdenes de ejecución interesantes, como secuencias que causaron bugs en el pasado
  • El scheduler puede extenderse con fuzzing de órdenes o exploración de todos los órdenes posibles
  • Traslada las pruebas de propiedades del sistema bajo latencias y fallas más cerca del tiempo de build que de las pruebas de integración, acelerando el desarrollo y ampliando la cobertura de comportamiento
  • Parte del trabajo de AWS en pruebas en tiempo de build de orden de hilos y fallas del sistema se publicó como open source en los proyectos shuttle y turmoil

• Fuzzing continuo y generación aleatoria de entradas de prueba

  • El fuzzing continuo, especialmente la generación escalable de entradas de prueba basada en cobertura, es eficaz para pruebas de corrección de sistemas en tiempo de integración
  • En el desarrollo de Aurora Limitless Database, la funcionalidad de particionamiento de datos de Amazon Aurora, se usó ampliamente fuzzing para verificar dos propiedades centrales
  • Se aplicó fuzzing a consultas SQL y transacciones completas para verificar que la partición lógica de la ejecución SQL entre shards fuera correcta
  • Se sintetizan grandes volúmenes de esquemas SQL, datasets y consultas aleatorias, se ejecutan en el motor bajo prueba y se comparan los resultados con un oráculo basado en un motor sin sharding
  • También se usan otros métodos de verificación, como el enfoque iniciado por SQLancer
  • La combinación de fuzzing y pruebas de inyección de fallas también resulta útil para aspectos de corrección de bases de datos como atomicidad, consistencia y aislamiento
    • Genera transacciones automáticamente
    • Define el comportamiento correcto mediante un oráculo de corrección especificado formalmente
    • Ejecuta en el sistema bajo prueba las posibles intercalaciones de transacciones y de sentencias internas de transacciones
    • Verifica a posteriori propiedades como el aislamiento siguiendo enfoques como Elle

Fault Injection Service y verificación de situaciones de falla

• A comienzos de 2021, AWS lanzó Fault Injection Service(FIS) para poner las pruebas basadas en inyección de fallas a disposición de diversos clientes de AWS
• FIS puede inyectar fallas simuladas en despliegues de prueba o producción de infraestructura de AWS
  • Errores de API
  • Pausas de I/O
  • Instancias fallidas
• La inyección de fallas permite confirmar si los mecanismos de resiliencia incorporados en la arquitectura realmente mejoran la disponibilidad y no generan nuevos problemas de corrección
  • Failover
  • Health checks
• Las pruebas de inyección de fallas basadas en FIS se usan ampliamente entre clientes de AWS y dentro de Amazon
• Amazon.com ejecutó 733 experimentos de inyección de fallas basados en FIS durante la preparación de Prime Day 2024
• En 2014, Yuan y otros analizaron que el 92% de las fallas catastróficas en los sistemas distribuidos probados fueron disparadas por un manejo incorrecto de errores no fatales
• La razón por la que las fallas catastróficas en el camino normal son raras es que ese camino se ejecuta con frecuencia, se prueba mejor y es mucho más simple que los caminos de error
• Las pruebas de inyección de fallas y FIS facilitan probar el comportamiento del sistema bajo fallas y situaciones de error, reduciendo la brecha de densidad de bugs entre el camino normal y los caminos de error
• La inyección de fallas en sí no se considera una técnica formal, pero puede combinarse con especificaciones formales
  • Define el comportamiento esperado mediante una especificación formal
  • Compara los resultados durante y después de la inyección de fallas con el comportamiento especificado
  • Puede detectar más bugs que revisar solo métricas y errores en logs, o que depender del juicio visual de una persona

Metaestabilidad y comportamiento emergente de sistemas

• Durante los últimos 10 años creció el interés por una clase particular de fallas de sistemas: las fallas metaestables (metastable failures)
• Una falla metaestable ocurre cuando un disparador, como una sobrecarga o el vaciado de caché, empuja a un sistema distribuido a un estado del que no puede recuperarse sin intervención
  • Un ejemplo de intervención es reducir la carga por debajo de lo normal
• Esta clase de fallas es uno de los factores importantes que contribuyen a la indisponibilidad en sistemas cloud
• En un comportamiento metaestable típico, al aumentar la carga, el goodput primero aumenta, luego se satura, pasa por congestión y cae a cero o casi cero
• Después, el sistema no puede volver a un estado saludable reduciendo apenas un poco la carga; necesita una reducción importante para recuperarse
• Este comportamiento puede aparecer incluso en sistemas simples, y en la mayoría de los sistemas también puede ser provocado por lógica de cliente de reintentos tras timeout
• El modelado formal tradicional de sistemas distribuidos suele enfocarse en seguridad (safety) y vivacidad (liveness), pero las fallas metaestables muestran que hay comportamientos que no encajan limpiamente en esa clasificación
• AWS usa cada vez más simulación de eventos discretos para entender comportamientos emergentes de sistemas
  • Invierte en simulaciones de sistemas a medida
  • Invierte en herramientas que permiten usar en simulación modelos de sistemas existentes creados con lenguajes como TLA+ y P
• Si los verificadores de modelos de exploración completa como TLC de TLA+ se extienden con simulación probabilística, pueden generar resultados estadísticos como distribuciones de latencia a posteriori
• Estas extensiones permiten usar la verificación de modelos para tareas como entender la posibilidad de cumplir SLA de latencia

Límites de seguridad que requieren pruebas formales

• En límites de seguridad importantes como autorización y virtualización, las técnicas formales anteriores pueden no ser suficientes, y las pruebas de corrección pueden justificar una gran inversión

• Lenguaje de políticas de autorización Cedar

  • En 2023, AWS introdujo Cedar, un lenguaje de políticas de autorización para escribir políticas con permisos granulares
  • Cedar fue diseñado teniendo en cuenta el razonamiento automático y las pruebas formales
  • La implementación se construyó con Dafny, un lenguaje de programación amigable para la verificación
  • Con Dafny se demuestra que la implementación satisface varias propiedades de seguridad
  • Esta demostración es una prueba en sentido matemático, más allá de las pruebas de software
  • El equipo también aplica pruebas diferenciales usando el código Dafny como oráculo de corrección para verificar la corrección de la implementación en Rust lista para producción
  • Junto con la implementación de Cedar, publicó como open source el código Dafny y los procedimientos de prueba para que los usuarios puedan revisar el trabajo de corrección

• Firecracker VMM

  • El monitor de máquinas virtuales Firecracker usa un protocolo de bajo nivel llamado virtio para exponer dispositivos de hardware emulados, como tarjetas de red o SSD, al kernel invitado dentro de la VM
  • Estos dispositivos emulados son la interacción más compleja entre un invitado no confiable y un host confiable, por lo que son un límite de seguridad importante
  • El equipo de Firecracker usa Kani, que permite razonar formalmente sobre código Rust, para probar propiedades centrales de este límite de seguridad
  • Esta prueba garantiza que las propiedades importantes del límite se mantengan sin importar lo que intente el invitado
  • AWS apoya el desarrollo de herramientas base como Kani, Dafny, Lean y los SMT solver que las impulsan
  • Los modelos y especificaciones formales se reutilizan de varias maneras
    • Verificación de modelos en tiempo de diseño
    • Como oráculos de corrección en monitoreo en tiempo de ejecución
    • Simulación de comportamiento emergente de sistemas
    • Construcción de pruebas de propiedades centrales

Efectos en rendimiento y costos más allá de la corrección

• Las técnicas formales también son importantes para mejorar de forma segura el rendimiento de sistemas cloud
• Al modelar con P y TLA+ el protocolo central de commit del motor de base de datos relacional Aurora, se encontró una oportunidad para reducir el costo del commit distribuido de 2 viajes de ida y vuelta de red a 1.5 viajes de ida y vuelta de red sin sacrificar propiedades de seguridad
• Este tipo de resultados es común en equipos que adoptan técnicas formales
  • El proceso de pensar profundamente en protocolos distribuidos y escribirlos formalmente impone un pensamiento estructurado
  • Aporta una comprensión más profunda de la estructura del protocolo y del problema a resolver
  • Poder confirmar o demostrar formalmente que una optimización de diseño propuesta es correcta permite a ingenieros de sistemas distribuidos elegir diseños más audaces sin aumentar el riesgo
• Los efectos en productividad y costos no se limitan a optimizaciones de diseño de alto nivel
• Un equipo de AWS encontró una optimización de la implementación de criptografía de clave pública RSA en procesadores Graviton 2 basados en ARM que pudo mejorar el throughput hasta en 94%
• Usó el demostrador interactivo de teoremas HOL Light para probar la corrección de esta optimización
• Como una alta proporción de los ciclos de CPU en la nube se usa en criptografía, estas optimizaciones pueden contribuir a reducir costos de infraestructura, apoyar la sostenibilidad y mejorar el rendimiento percibido por los clientes

Desafíos pendientes y oportunidades futuras

• Aunque AWS tuvo éxito durante los últimos 15 años al escalar métodos de prueba formales y semiformalas, todavía quedan desafíos para la adopción industrial
• Las principales barreras de las herramientas de técnicas formales son la curva de aprendizaje pronunciada y la necesidad de conocimiento especializado del dominio
• Muchas herramientas siguen teniendo un carácter académico y carecen de interfaces amigables para usuarios
• Incluso enfoques semiformalos bien establecidos aún enfrentan barreras de adopción
  • La simulación determinista es una técnica central de prueba de sistemas distribuidos usada con éxito en AWS y en proyectos como FoundationDB, pero puede resultar desconocida incluso para desarrolladores experimentados de sistemas distribuidos que se incorporan a AWS
  • Existen brechas similares en metodologías probadas como pruebas de inyección de fallas, pruebas basadas en propiedades y fuzzing
• Es necesario capacitar a desarrolladores de sistemas distribuidos en estos métodos y herramientas de prueba, y enseñar una forma de pensamiento rigurosa
• La brecha educativa empieza en el ámbito académico
  • Incluso enfoques básicos de razonamiento formal se enseñan rara vez
  • A egresados de instituciones de primer nivel también les resulta difícil adoptar estas herramientas
  • Las técnicas formales y el razonamiento automático son importantes para la aplicación industrial, pero todavía se consideran áreas de nicho
• La metaestabilidad y otras propiedades emergentes de sistemas a gran escala también son áreas de investigación importantes con desafíos similares de reconocimiento
  • Prácticas que pueden provocar comportamiento metaestable de sistemas, como “reintentar N veces ante un timeout”, siguen recomendándose ampliamente pese a ser problemas conocidos
  • Las herramientas y técnicas actuales para entender el comportamiento emergente de sistemas están en una etapa inicial
  • Modelar la estabilidad de sistemas es costoso y complejo
• AWS considera que los modelos de lenguaje grandes y los asistentes de IA pueden ayudar mucho a aliviar los problemas de adopción práctica de las técnicas formales
  • Así como las pruebas unitarias asistidas por IA ganaron popularidad, pueden ayudar a desarrolladores a crear modelos y especificaciones formales
  • Las técnicas avanzadas pueden volverse accesibles para una comunidad más amplia de desarrolladores

El marco de corrección en el que AWS sigue invirtiendo

• Para crear software confiable y seguro se necesitan distintos enfoques para razonar sobre la corrección de sistemas
• AWS adopta varias técnicas junto con pruebas estándar de la industria, como pruebas unitarias y de integración
  • Verificación de modelos
  • Fuzzing
  • Pruebas basadas en propiedades
  • Pruebas de inyección de fallas
  • Simulación determinista
  • Simulación basada en eventos
  • Verificación en tiempo de ejecución de trazas de ejecución
• Las especificaciones formales cumplen un papel importante como oráculos de prueba que proveen la respuesta correcta en varias prácticas de prueba de AWS
• Las pruebas de corrección y las técnicas formales siguen siendo un área central de inversión para AWS, sobre la base del retorno de inversión ya obtenido