- Amazon Web Services (AWS) considera la corrección de sus servicios como un valor central e integra varias formas de metodologías formales en su proceso de desarrollo
- Mediante herramientas de especificación formal como TLA+ y el lenguaje P, puede detectar errores sutiles de forma temprana y mantener la confiabilidad incluso con optimizaciones audaces
- AWS también opera ampliamente con metodologías formales livianas como pruebas basadas en propiedades, simulación determinista y fuzzing continuo
- A través de herramientas de inyección de fallas como Fault Injection Service, automatiza la verificación de confiabilidad incluso en escenarios donde ocurren fallas
- Aunque siguen existiendo la barrera educativa y la complejidad de las herramientas, se espera que la expansión de la IA y de las herramientas de automatización contribuya a una adopción más amplia
Estrategia de AWS para garantizar la corrección de sistemas
Amazon Web Services (AWS) tiene como objetivo ofrecer servicios altamente confiables en los que los clientes puedan confiar por completo
Para ello, busca mantener estándares de seguridad, durabilidad, integridad y disponibilidad, colocando en el centro el concepto de corrección de sistemas
Desde que en 2015 se presentó en Communications of the ACM un caso de aplicación de metodologías formales en AWS, este enfoque ha desempeñado un papel importante en la operación exitosa de servicios clave
En el centro está TLA+, un lenguaje de especificación formal desarrollado por Leslie Lamport
La experiencia de AWS introduciendo TLA+ permitió identificar, en etapas tempranas del desarrollo, errores sutiles que las pruebas convencionales no detectaban
Además, incluso al realizar optimizaciones de rendimiento agresivas, la verificación formal permitió asegurar estabilidad y confiabilidad
Hace 15 años, AWS se quedaba en un nivel básico con pruebas unitarias al momento del build y pruebas de integración limitadas, pero desde entonces ha adoptado de forma integral enfoques formales y semiformales
Este cambio ha contribuido no solo a la corrección, sino también a la verificación de optimizaciones de alto y bajo nivel, a mejorar la velocidad de desarrollo y a reducir costos
En AWS, además de las tradicionales demostraciones formales y la verificación de modelos, también se incluyen dentro de las metodologías formales las pruebas basadas en propiedades, el fuzzing y el monitoreo en tiempo de ejecución
La aparición del lenguaje de programación P
Al principio, TLA+ tenía la ventaja de ser una descripción abstracta poderosa, pero para muchos desarrolladores la barrera de entrada del uso de notación matemática era alta
Por eso, AWS introdujo el lenguaje P, que ofrece un enfoque basado en máquinas de estado familiar para los desarrolladores
El lenguaje P proporciona una forma de modelado con máquinas de estado para el diseño y análisis de sistemas distribuidos
Es un concepto familiar para los desarrolladores de Amazon que usan arquitecturas SOA basadas en microservicios
Desde 2019 se desarrolla en AWS y se mantiene como proyecto estratégico de código abierto
Equipos de servicios principales como Amazon S3, EBS, DynamoDB, Aurora, EC2 e IoT usan P para verificar la corrección del diseño de sistemas
Cuando S3 se migró a una fuerte consistencia read-after-write, se modeló y verificó el protocolo con P, eliminando errores en etapas tempranas del diseño e incorporando optimizaciones de forma segura
En 2023, el equipo de P de AWS desarrolló la herramienta PObserve, que permite verificar la corrección de sistemas distribuidos tanto en pruebas como en entornos reales de producción
PObserve extrae logs de ejecución y permite verificar a posteriori si el comportamiento fue correcto según la especificación, conectando de forma eficaz la especificación de la etapa de diseño con la implementación real en código
Expansión de las metodologías formales livianas
Pruebas basadas en propiedades
La técnica formal liviana más representativa es la prueba basada en propiedades
Por ejemplo, el equipo de desarrollo de ShardStore de S3 usa de forma combinada pruebas basadas en propiedades, fuzzing guiado por cobertura de código, inyección de fallas y minimización de contraejemplos a lo largo de todo el ciclo de desarrollo
Este enfoque se integra con especificaciones de corrección escritas directamente por los desarrolladores y mejora considerablemente la eficiencia al depurar problemas
Simulación determinista
Las pruebas de simulación determinista ejecutan sistemas distribuidos en un simulador de un solo hilo, lo que permite controlar todos los elementos aleatorios, como planificación, tiempos y orden de mensajes
Se aplican de diversas maneras, como pruebas para escenarios específicos de error y éxito, ajuste del orden que provoca bugs y ampliación del fuzzing
Esto permite verificar antes, en la etapa de build, el comportamiento del sistema frente a latencia y fallas, además de ampliar la cobertura de pruebas
AWS publicó este código de pruebas en tiempo de build como los proyectos de código abierto shuttle y turmoil
Fuzzing continuo
El fuzzing continuo, especialmente la generación masiva de entradas basada en cobertura de código, es eficaz para verificar la corrección del sistema en la etapa de pruebas de integración
Por ejemplo, durante el desarrollo de Aurora Limitless Database, se aplicó fuzzing a consultas SQL y transacciones para verificar la corrección de la lógica de particionamiento mediante la generación de grandes cantidades de esquemas, datasets y consultas aleatorias
Los resultados se comparan con el comportamiento del motor non-sharded o con métodos como SQLancer
La combinación de fuzzing e inyección de fallas permite verificar propiedades clave de bases de datos como atomicidad, consistencia y aislamiento
Algunas propiedades, como las transacciones generadas automáticamente y el aislamiento, se garantizan mediante verificación posterior basada en historiales de ejecución
Inyección de fallas con Fault Injection Service
En 2021, AWS lanzó Fault Injection Service (FIS), permitiendo que los clientes experimenten rápidamente distintos escenarios de fallas —como errores de API, interrupciones de I/O y fallas de instancias— en entornos reales o de prueba
Esto ayuda a garantizar la disponibilidad de la arquitectura, revisar la resiliencia ante fallas, cerrar la diferencia de alta densidad de bugs en casos de error y detectar con anticipación problemas graves de alta probabilidad
FIS se usa ampliamente tanto por clientes de AWS como dentro de Amazon; por ejemplo, solo durante la preparación para Prime Day se realizaron 733 experimentos
La inyección de errores es aún más efectiva cuando se combina con especificaciones formales
Al escribir el comportamiento esperado como especificación formal y contrastarlo con los resultados reales provocados por fallas, se pueden detectar más errores que con simples revisiones de logs y métricas
Metaestabilidad y comportamiento emergente del sistema
En sistemas distribuidos, están aumentando los casos en los que una carga excesiva o el agotamiento de caché provocan estados anómalos de los que el sistema no puede recuperarse por sí mismo (metaestables)
En este estado, una simple reducción de carga no basta para volver a la normalidad, y responder a ello es más difícil que en los casos de error habituales
La mayoría de las lógicas de reintento y timeout también son causa de este fenómeno
Las especificaciones formales existentes se centran en seguridad y progreso, pero la metaestabilidad exige considerar además diversos comportamientos emergentes
AWS realiza simulación de eventos discretos basada en modelos de especificación como TLA+ y P, analizando de forma sistemática incluso propiedades probabilísticas como la posibilidad de cumplir SLA de rendimiento y la distribución de latencias
La necesidad de demostraciones formales
En algunos límites de seguridad —como permisos y virtualización— son indispensables demostraciones de nivel matemático, más allá de simples pruebas
Por ejemplo, el lenguaje de políticas de autorización Cedar, introducido por AWS en 2023, está optimizado para demostración automática y verificación formal sobre Dafny, y gracias al código público y a los procedimientos de corrección, cualquier usuario puede verificarlo directamente
Asimismo, propiedades clave de seguridad del VMM Firecracker se están demostrando con herramientas de análisis de código Rust como Kani
De esta forma, al usar ampliamente modelos y especificaciones formales en distintos momentos —diseño, implementación, operación y demostración—, AWS los aprovecha para asegurar la corrección del software y ampliar el valor para la empresa y los clientes
Efectos adicionales más allá de la corrección
Las metodologías formales desempeñan un papel importante tanto en la confiabilidad como en la mejora del rendimiento
Por ejemplo, al verificar con P y TLA+ el protocolo de commit de Aurora, se redujeron los round-trips de red y al mismo tiempo se garantizó la seguridad
Al optimizar el algoritmo de cifrado RSA para ARM Graviton 2, se demostró en HOL Light la corrección matemática de la transformación, logrando un efecto tangible de mejorar al mismo tiempo el rendimiento y los costos de infraestructura
Desafíos y oportunidades futuras
Durante 15 años, AWS ha ampliado considerablemente la aplicación industrial de metodologías formales y semiformales, pero persisten barreras reales de adopción como la curva de aprendizaje, la necesidad de expertos y el carácter académico de las herramientas
Incluso técnicas como las pruebas basadas en propiedades y la simulación determinista siguen siendo poco familiares para muchos desarrolladores
Como la barrera educativa existe desde el nivel universitario, la difusión de herramientas y metodologías, así como su aplicación práctica, avanza lentamente
Las propiedades emergentes de sistemas a gran escala, como la metaestabilidad, también siguen en una etapa temprana de investigación
Se espera que en el futuro la IA y los grandes modelos de lenguaje apoyen la redacción de modelos y especificaciones formales, elevando de manera drástica la accesibilidad para los profesionales en el corto plazo
Conclusión
Para construir software robusto y seguro se necesitan diversos medios para asegurar la corrección de sistemas
AWS ha adoptado de forma integral, además de las técnicas estándar de pruebas, model checking, fuzzing, pruebas basadas en propiedades, pruebas de inyección de fallas, simulación determinista y basada en eventos, y verificación de historiales de ejecución
Las especificaciones y metodologías formales cumplen un importante papel como oráculo de pruebas dentro del proceso de desarrollo de AWS, y ya se han consolidado como una de las áreas de inversión gracias a la validación de sus efectos prácticos y económicos
1 comentarios
Opiniones de Hacker News
Quiero hablar del enfoque de pruebas de simulación determinista. En AWS ejecutan sistemas distribuidos en un simulador de un solo hilo, controlando todos los elementos no deterministas como la planificación de hilos, el timing y el orden de entrega de mensajes. Luego escriben pruebas adaptadas a escenarios específicos de falla o éxito, y la no determinación dentro del sistema queda controlada por el framework de pruebas. Los desarrolladores pueden especificar secuencias concretas que en el pasado provocaron errores. El scheduler puede incluso ampliarse para hacer fuzzing de órdenes o explorar todas las secuencias posibles. Me pregunto si existe alguna biblioteca open source, independiente del lenguaje, que implemente algo así. La idea sería contar con una herramienta de middleware que vuelva “deterministas” durante las pruebas aspectos como networking, storage, etc., dentro de contenedores. antithesis cumple casi exactamente ese rol, pero todavía no he visto algo así en open source. Si las pruebas están bien escritas, se puede resolver parte de esto haciendo stubs del I/O, pero no hay garantía de que todo el mundo escriba buenas pruebas. Creo que sería bueno ofrecer determinismo en una capa más alta, por encima de la aplicación. Por otro lado, espero que la IA realmente pueda destacar en testing. Prompt (requerimientos) - implementación de pruebas - IA - código ejecutable: esos tres ejes podrían encajar de forma ideal. Ojalá la IA facilite más la verificación formal y vuelva el mundo del software un poco más riguroso
Hay dos dificultades para expandir la técnica de pruebas de simulación determinista (DST). La primera es que, hasta ahora, todos los sistemas tenían que montarse directamente sobre un framework de simulación específico, sin depender de nada externo. La segunda es que, si la generación y exploración de entradas es débil, las pruebas pueden aparentar que todo pasa mientras en realidad no validan casi nada. antithesis intenta resolver ambos problemas, pero sigue siendo difícil. Casi nadie tiene una forma realmente sólida de aplicar determinismo a cualquier software. El proyecto Hermit de Facebook también intentó crear un Linux userspace determinista, pero al final se abandonó. Las computadoras deterministas son una base técnica muy útil más allá de las pruebas, y creo que algún día alguien lo publicará como open source
Creo que obtener una máquina determinista ejecutando QEMU en modo 100% emulación y en un solo hilo es relativamente fácil. Pero lo que uno realmente quiere es ejecución determinista “controlada”, y eso es mucho más difícil. Lograr que varios procesos se comporten según un escenario definido es especialmente complejo a nivel de CPU y del scheduler del sistema operativo. También es difícil construir un entorno realmente agnóstico al lenguaje, y es fácil quedar atrapado en detalles finos. Yo mismo hice una vez un sistema simple para ejecutar varios hilos de JVM en lockstep en puntos específicos del flujo, manejando I/O y tiempo del sistema con stubs y control explícito. Así pude probar distintas interacciones entre componentes asíncronos, fallas de I/O, reintentos, etc., y atrapar bugs molestos antes de llegar a producción. Eso sí, fue posible simplificando solo ciertos puntos de sincronización, no controlando todo el sistema. Los data races comunes por errores de sincronización son difíciles de detectar con este enfoque
Comparto la documentación oficial sobre el método de pruebas de FoundationDB y esta charla en YouTube
Si es un lenguaje que se puede depurar con gdb, recomiendo el proyecto https://rr-project.org/
Recuerdo haber visto hace tiempo una charla de Joe Armstrong sobre cómo probaron Dropbox usando property testing
S3 me parece una de las piezas de software más impresionantes que he visto. Hace unos años también agregaron consistencia fuerte de lectura-escritura a todo el sistema de S3, y me pareció una cumbre real de la ingeniería de software enlace al blog post
Trabajé directamente en el ciclo de vida de S3, y coincidió con la época en que el equipo de índices estaba rediseñando la estructura para ofrecer esa consistencia. S3 ya se ve increíble desde afuera, pero internamente tanto la implementación como la estructura organizacional son más impresionantes de lo que uno imaginaría
Google Cloud Storage, de hecho, ya tenía esa funcionalidad (consistencia fuerte) mucho antes que S3. En general, GCS me da la impresión de ser un producto más sistemático y mejor construido
Me identifico con esa cifra del 92% (la mayoría de las fallas de clúster empiezan con errores menores). No suelen ser accidentes espectaculares y llamativos, sino reintentos “sin importancia” que van acumulando estado hasta que terminan explotando como una caída masiva a las 2 de la mañana. Es importante dedicar más tiempo de ingeniería a las fallas poco visibles
Me parece un artículo realmente interesante. El uso de máquinas de estado para construir control planes de infraestructura es indispensable. No estoy seguro de que realmente hiciera falta P. Nosotros también construimos un control plane de infraestructura en Ruby durante más de 13 años, y funcionó excelentemente blog con la experiencia
Tenía curiosidad sobre el lenguaje P. Antes parecía que en Microsoft lo usaban de verdad para generar código C destinado al runtime del stack USB de Windows, pero ahora da la impresión de que ya no se usa para generar código de producción. Incluso dejé una pregunta al respecto en Hacker News enlace a la pregunta. Si el código generado podía llegar hasta el kernel, claramente también debería servir en entornos cloud con condiciones mucho menos estrictas
Como alguien que no viene de AWS ni está familiarizado con TLA+ o P, creo que incluso un ejemplo del nivel de “hola mundo” habría hecho todo más fácil de entender. Leyendo el texto, por momentos se siente simplemente como un proceso doloroso, y queda la duda de si no son problemas que podrían resolverse suficientemente bien con buen diseño y buenas pruebas. Un ejemplo simple habría ayudado más a juzgar qué es lo que realmente se está haciendo
Tengo un ejemplo rápido de demo de TLA+ que me gusta mucho enlace al gist. Modela varios hilos incrementando un contador compartido de forma no atómica, y al verificar propiedades aparece el race condition. En la práctica, este tipo de bug es muy difícil de encontrar solo con pruebas. La mayoría de las especificaciones TLA+ son bastante más complejas, pero este ejemplo sirve bien para captar errores simples
He usado TLA directamente y tuve la experiencia frustrante de que la herramienta gráfica no encajaba bien con los tutoriales. Aun así, sí quería usar TLA, y desde hace tiempo me gusta el trabajo de Lamport (desde LaTeX hasta sus papers)
La premisa de usar métodos formales es, al final, que con pruebas jamás se podrán encontrar absolutamente todos los problemas
Recomiendo el repositorio oficial de GitHub TLA+ Examples. Conviene empezar con algo simple, como el problema de DieHard
Las pruebas demuestran la corrección de una implementación para instancias específicas del problema, mientras que la verificación formal la demuestra para toda una categoría. Por ejemplo, en una función que devuelve anagramas, las pruebas validan algunos pares de palabras, pero para demostrar corrección sobre todos los pares posibles hace falta formal verification. Casos como undefined behavior o bugs de librerías también muchas veces solo se detectan durante un proceso de formal verification
Sobre la mención de “técnicas ligeras cuasi formales como property-based testing, fuzzing y runtime monitoring”, me parece que property-based testing y fuzzing sí son subconjuntos de métodos formales, pero incluir también runtime monitoring dentro de técnicas cuasi formales suena un poco excesivo
Hace tiempo tuve contacto con Leslie Lamport por temas como artículos sobre el principio de Buridan. Hoy aprendí bastante sobre TLA+ y PlusCal en su sitio web página del ejemplo de Peterson. Me parece totalmente natural que alguien que llevó las matemáticas a la programación y fue prácticamente fundador del área de sistemas concurrentes también haya creado un lenguaje de diseño de sistemas (TLA+) que se use en AWS y otros lugares. Ojalá más personas que construyen sistemas distribuidos usaran lo que creó Lamport. En sistemas grandes, demostrar corrección es muy importante
Para convertir código existente en especificaciones TLA+, Claude Opus (Extended Thinking) resulta bastante útil. Me ha servido para encontrar varios bugs en proyectos Rust y en la verificación de componentes centrales en C++. Otros modelos suelen tropezar bastante con la sintaxis y la lógica de las especificaciones, mientras que Opus funciona mucho mejor
No solo en sistemas grandes: demostrar corrección también sería muy valioso en utilidades pequeñas pero críticas, como SSH o terminales, que se usan en todo el mundo
Sobre la frase “demostrar la corrección del sistema”, en realidad no es posible demostrarlo todo. Un model checker solo puede decirte que la especificación dada satisface ciertas propiedades dentro de un espacio de estados acotado
En lo personal, me da curiosidad si alguien ha usado FIS para experimentos en servicios distribuidos. Estoy considerando adoptarlo, pero no tengo experiencia directa haciendo experimentos grandes con eso
Me pregunto si Promela y SPIN son lenguajes de nivel más alto que lo que se trata en el artículo