Práticas de correção de sistemas na Amazon Web Services
(cacm.acm.org)- A Amazon Web Services (AWS) coloca a correção dos serviços como um valor central e integra várias formas de métodos formais ao processo de desenvolvimento
- Com ferramentas de especificação formal como TLA+ e a linguagem P, é possível encontrar bugs sutis cedo e garantir confiabilidade mesmo em otimizações ousadas
- A AWS também usa amplamente métodos formais leves, como testes baseados em propriedades, simulação determinística e fuzzing contínuo
- Com ferramentas de injeção de falhas como o Fault Injection Service, a verificação de confiabilidade é automatizada incluindo até cenários de indisponibilidade
- Embora a barreira educacional e a complexidade das ferramentas ainda persistam, a expansão de IA e ferramentas de automação tende a ampliar a adoção
Estratégia da AWS para garantir a correção de sistemas
A Amazon Web Services (AWS) tem como objetivo oferecer serviços altamente confiáveis nos quais os clientes possam confiar plenamente
Para isso, busca manter padrões de segurança, durabilidade, integridade e disponibilidade, colocando no centro o conceito de correção de sistemas
Desde que o caso de aplicação de métodos formais da AWS foi apresentado em 2015 na Communications of the ACM, essa abordagem vem desempenhando um papel importante na operação bem-sucedida de serviços centrais
No centro está o TLA+, uma linguagem de especificação formal desenvolvida por Leslie Lamport
A experiência da AWS com a adoção do TLA+ permitiu identificar, nos estágios iniciais do desenvolvimento, bugs sutis que os testes convencionais não capturavam
Além disso, mesmo ao realizar otimizações agressivas de desempenho, foi possível garantir estabilidade e confiabilidade por meio de verificação formal
Há 15 anos, a AWS ficava em um nível básico, com testes unitários no momento do build e testes de integração limitados, mas desde então passou a adotar de forma abrangente abordagens formais e métodos semiformalizados
Essa mudança contribuiu não apenas para a correção, mas também para a validação de otimizações de alto e baixo nível, aumento da velocidade de desenvolvimento e redução de custos
Na AWS, além de provas formais e verificação de modelos, também são incluídos no escopo de métodos formais recursos como testes baseados em propriedades, fuzzing e monitoramento em tempo de execução
O surgimento da linguagem de programação P
No início, o TLA+ tinha a vantagem de ser uma técnica abstrata poderosa, mas, para muitos desenvolvedores, a barreira de entrada do uso de notação matemática era alta
Por isso, a AWS adotou a linguagem P, que oferece uma abordagem baseada em máquinas de estado mais familiar aos desenvolvedores
A linguagem P fornece uma forma de modelagem por máquinas de estado para o projeto e a análise de sistemas distribuídos
É um conceito familiar para desenvolvedores da Amazon que usam arquitetura SOA baseada em microsserviços
Desde 2019, ela é desenvolvida na AWS e mantida como um projeto estratégico de código aberto
Equipes de serviços importantes como Amazon S3, EBS, DynamoDB, Aurora, EC2 e IoT usam P para verificar a correção do projeto de sistemas
Ao migrar o S3 para uma forte consistência read-after-write, a equipe modelou e verificou o protocolo com P, eliminando bugs ainda nos estágios iniciais do projeto e incorporando otimizações com segurança
Em 2023, a equipe de P da AWS desenvolveu a ferramenta PObserve, tornando possível verificar a correção de sistemas distribuídos tanto em testes quanto em ambientes reais de produção
O PObserve extrai logs de execução e permite verificar posteriormente se o comportamento ocorreu corretamente de acordo com a especificação, conectando de forma eficaz a especificação da fase de projeto com a implementação real em código
Expansão dos métodos formais leves
Testes baseados em propriedades
A técnica formal leve mais representativa são os testes baseados em propriedades
Por exemplo, a equipe de desenvolvimento do ShardStore do S3 usa de forma combinada, ao longo de todo o ciclo de desenvolvimento, testes baseados em propriedades, fuzzing com base em cobertura de código, injeção de falhas e minimização de contraexemplos
Esse modelo se integra às especificações de correção escritas pelos próprios desenvolvedores e melhora bastante a eficiência de depuração de problemas
Simulação determinística
Os testes de simulação determinística executam sistemas distribuídos em um simulador de thread única, permitindo controlar todos os elementos aleatórios, como agendamento, tempo e ordem de mensagens
Eles são aplicados de várias formas, como testes para cenários específicos de falha e sucesso, ajuste de sequências que provocam bugs e expansão do fuzzing
Com isso, a validação do comportamento do sistema sob latência, falhas e outras condições pode ser feita mais cedo, ainda na fase de build, e o alcance dos testes é ampliado
A AWS disponibilizou esse código de teste de build time como os projetos open source shuttle e turmoil
Fuzzing contínuo
O fuzzing contínuo, especialmente a geração em larga escala de entradas baseada em cobertura de código, é eficaz para verificar a correção do sistema na etapa de testes de integração
Por exemplo, no desenvolvimento do Aurora Limitless Database, consultas SQL e transações foram submetidas a fuzzing para validar a correção da lógica de particionamento por meio da geração de grandes volumes de esquemas, conjuntos de dados e consultas aleatórios
Os resultados são comparados com o comportamento do engine sem sharding ou com métodos como o SQLancer
Ao combinar fuzzing e injeção de falhas, são verificadas propriedades essenciais de bancos de dados como atomicidade, consistência e isolamento
Algumas propriedades, como transações geradas automaticamente e isolamento, são garantidas por verificação posterior baseada no histórico de execução
Injeção de falhas com o Fault Injection Service
Em 2021, a AWS lançou o Fault Injection Service (FIS), permitindo que clientes também experimentem rapidamente, em ambientes reais ou de teste, diversos cenários de falha, como erros de API, interrupções de I/O e falhas de instância
Com isso, é possível melhorar a disponibilidade da arquitetura e verificar a resiliência a falhas, reduzir a diferença na alta densidade de bugs em casos de erro e detectar antecipadamente problemas graves e prováveis
O FIS é amplamente usado não apenas por clientes da AWS, mas também internamente na Amazon; por exemplo, só na preparação para o Prime Day foram realizados 733 experimentos
A injeção de erros é ainda mais eficaz quando combinada com especificações formais
Ao escrever o comportamento esperado como uma especificação formal e comparar com ela os resultados das falhas induzidas na prática, é possível detectar mais erros do que com a simples inspeção tradicional de logs e métricas
Metaestabilidade e comportamento emergente dos sistemas
Em sistemas distribuídos, estão aumentando os casos em que situações como carga excessiva ou exaustão de cache levam o sistema a um estado anormal “incapaz de se recuperar por conta própria”, ou seja, metaestável
Nesse estado, a simples redução de carga não restaabelece o funcionamento normal, e a resposta é mais difícil do que em casos típicos de erro
Grande parte da lógica convencional de retry e timeout também é causa desse fenômeno
As especificações formais tradicionais focam em segurança e progresso, mas a metaestabilidade exige considerar também vários outros comportamentos emergentes
Com base em modelos de especificação como TLA+ e P, a AWS realiza simulação de eventos discretos para analisar de forma sistemática até características probabilísticas, como a possibilidade de atingir SLAs de desempenho e a distribuição de latência
A necessidade de prova formal
Em alguns limites de segurança (permissões, virtualização etc.), é indispensável uma prova de nível matemático, além de testes simples
Por exemplo, a linguagem de política de autorização Cedar, introduzida pela AWS em 2023, foi otimizada para prova automática e verificação formal com base em Dafny, e, por meio de código público e procedimentos de correção, permite que todos os usuários façam a verificação diretamente
Além disso, propriedades-chave do limite de segurança do Firecracker VMM estão sendo provadas com ferramentas de análise de código Rust como o Kani
Dessa forma, ao usar amplamente modelos e especificações formais em diferentes momentos — projeto, implementação, operação e prova —, a AWS os aproveita para garantir a correção do software e ampliar o valor para a empresa e os clientes
Efeitos adicionais além da correção
Os métodos formais desempenham um papel importante tanto na confiabilidade quanto na melhoria de desempenho
Por exemplo, o protocolo de commit do Aurora foi verificado com P e TLA+, reduzindo o número de round trips de rede e, ao mesmo tempo, garantindo a segurança
Na otimização do algoritmo de criptografia RSA para ARM Graviton 2, a correção matemática da transformação foi provada no HOL Light, gerando um efeito prático de melhoria simultânea de desempenho e custo de infraestrutura
Desafios e oportunidades para o futuro
Ao longo de 15 anos, a AWS ampliou bastante a aplicação industrial de métodos formais e semiformalizados, mas ainda persistem obstáculos reais à adoção, como curva de aprendizado, necessidade de especialistas e caráter acadêmico das ferramentas
Mesmo testes baseados em propriedades e simulação determinística ainda são pouco familiares para muitos desenvolvedores
Como a barreira educacional já existe desde a graduação, a disseminação dessas ferramentas e metodologias e sua aplicação prática avançam lentamente
Características emergentes de sistemas de larga escala, como a metaestabilidade, também ainda estão em estágio inicial de pesquisa
No futuro, espera-se que IA e grandes modelos de linguagem apoiem a criação de modelos e especificações formais, elevando drasticamente a acessibilidade para profissionais em pouco tempo
Conclusão
Construir software robusto e seguro exige diversos meios para garantir a correção dos sistemas
A AWS adota de forma abrangente, além das técnicas padrão de teste, model checking, fuzzing, testes baseados em propriedades, testes de injeção de falhas, simulação determinística e baseada em eventos, e verificação de históricos de execução
As especificações e metodologias formais desempenham um papel importante de oráculo de teste no processo de desenvolvimento da AWS e, por já terem comprovado efeitos práticos e econômicos, se consolidaram como uma das áreas de investimento
1 comentários
Opiniões no Hacker News
Quero falar sobre a abordagem de testes com simulação determinística. Na AWS, eles executam sistemas distribuídos em um simulador single-thread, controlando todos os elementos não determinísticos, como escalonamento de threads, temporização e ordem de entrega de mensagens. Depois, escrevem testes voltados para cenários específicos de falha ou sucesso, e a não determinística dentro do sistema é controlada pelo framework de testes. O desenvolvedor pode especificar uma sequência exata que já causou bugs no passado. O scheduler pode até ser expandido para fuzzing de sequências ou exploração de todas as ordens possíveis. Fico curioso se existe alguma biblioteca open source que implemente algo assim de forma independente de linguagem. A ideia seria ter uma ferramenta de middleware que também tornasse “determinísticos” aspectos como rede e armazenamento dentro de containers no momento do teste. O antithesis faz quase exatamente esse papel, mas ainda não vi algo assim em open source. Se os testes forem bem escritos, dá para contornar parte disso com stubs de I/O e similares, mas não dá para assumir que todo mundo escreve bons testes. Acho que seria bom oferecer determinismo em uma camada mais alta, acima da aplicação. Ao mesmo tempo, espero que a IA possa realmente brilhar em testes. Os três eixos prompt (requisitos) - implementação de testes - IA - código executável poderiam se encaixar de forma ideal. Tenho a expectativa de que a IA torne a verificação formal mais acessível e deixe o mundo do software ainda mais rigoroso
Existem duas dificuldades para a disseminação da técnica de deterministic simulation testing (DST). Primeiro, até agora era necessário colocar todo o sistema diretamente sobre um framework de simulação específico, sem outras dependências. Segundo, se a geração e exploração de entradas forem fracas, os testes podem parecer todos bem-sucedidos sem fazer uma validação real. O antithesis tenta resolver ambos os pontos, mas ainda há muita dificuldade. Quase ninguém tem um método realmente confiável para aplicar determinismo a qualquer software. O projeto Hermit, do Facebook, também tentou isso com um espaço de usuário Linux determinístico, mas acabou sendo descontinuado. Computadores determinísticos são uma base técnica muito útil também fora de testes, e acho que em algum momento alguém ainda vai liberar isso em open source
Acho relativamente fácil obter uma máquina determinística rodando o QEMU em modo 100% emulação, single-thread. Mas o que se quer de verdade é uma execução determinística “controlada”, e isso é bem mais difícil. Fazer vários processos seguirem um cenário especificado é especialmente complicado no nível de CPU e scheduler do sistema operacional. Também é difícil criar um ambiente que seja de fato independente de linguagem, e é fácil ficar preso em detalhes minuciosos. Eu mesmo já criei um sistema simples para fazer várias threads da JVM avançarem em lockstep em pontos específicos de execução, tratando I/O e tempo do sistema com stubs e controle. Assim, consegui testar várias interações entre componentes assíncronos, falhas de I/O, retries etc. e pegar bugs incômodos antes de ir para produção. Mas isso só foi possível simplificando pontos específicos de sincronização, em vez de controlar o sistema inteiro. Corridas de dados mais gerais causadas por erros de sincronização não são fáceis de capturar desse jeito
Compartilhando a documentação oficial dos testes do FoundationDB e uma apresentação no YouTube
Se a linguagem puder ser depurada com gdb, recomendo o projeto https://rr-project.org/
Lembro de ter visto há muito tempo uma apresentação do Joe Armstrong sobre testar o Dropbox usando property testing
Acho que o S3 é uma das coisas mais impressionantes que já vi em software. O fato de terem adicionado consistência forte de leitura após escrita ao sistema inteiro do S3 alguns anos atrás também me parece o auge da engenharia de software de verdade link do post no blog
Já trabalhei diretamente com o lifecycle do S3, e coincidiu com a época em que a equipe de índice estava redesenhando a estrutura para oferecer essa consistência. O S3 já parece incrível por fora, mas internamente tanto a implementação quanto a estrutura organizacional são impressionantes além do que se imagina
O Google Cloud Storage, na verdade, já tinha essa funcionalidade (consistência forte) muito antes do S3. No geral, fico com a impressão de que o GCS é um produto mais sistemático e melhor construído
Concordo com o número de 92% (a maioria das falhas de cluster começa com falhas triviais). Na maioria das vezes, não é um grande desastre dramático, mas um retry “sem importância” que vai acumulando estado até explodir em uma pane grande às 2 da manhã. É importante dedicar mais tempo de engenharia a falhas pouco visíveis
Achei o texto realmente interessante. O uso de máquinas de estado para construir control planes de infraestrutura é essencial. Não sei se era necessário usar exatamente o P. Nós também construímos um control plane de infraestrutura em Ruby por mais de 13 anos, e funciona muito bem post compartilhando a experiência
Eu tinha curiosidade sobre a linguagem P. Antes, parecia que a Microsoft usava P para gerar código C para o runtime da stack USB do Windows e usava isso de verdade, mas hoje parece que ela não é mais usada para gerar código de produção. Já deixei uma pergunta relacionada no Hacker News link da pergunta. Se código gerado pode até entrar no kernel, então certamente também poderia ser usado em ambientes de nuvem com restrições muito mais leves
Para quem não veio da AWS e não está familiarizado com TLA+ ou P, teria sido bem mais fácil entender se houvesse ao menos um exemplo no nível de “hello world”. Lendo o texto, chega a parecer apenas um processo doloroso, e dá a impressão de que talvez não sejam problemas que bom design e bons testes já resolveriam. Um exemplo simples ajudaria muito mais a avaliar o que isso realmente faz
Tenho um exemplo rápido de demonstração de TLA+ de que gosto muito link do gist. É um modelo em que várias threads incrementam um contador compartilhado de forma não atômica, e a verificação de propriedades encontra a race condition. Na prática, é muito difícil descobrir esse tipo de bug só com testes. A maioria das especificações TLA+ é bem mais complexa, mas esse exemplo é bom para capturar erros simples
Já usei TLA diretamente, mas tive uma experiência decepcionante porque a ferramenta gráfica não combinava bem com o tutorial. Eu queria usar TLA mesmo assim, e já gostava do trabalho do Lamport havia tempos, de LaTeX a artigos
A premissa de usar métodos formais é justamente que testes, sozinhos, jamais conseguem encontrar todos os problemas
Recomendo o repositório oficial TLA+ Examples no GitHub. Vale começar por algo simples, como o problema DieHard
Testes provam a correção de uma implementação para instâncias específicas do problema, enquanto a verificação formal prova para a classe inteira. Por exemplo, no caso de uma função que retorna anagramas, testes verificam apenas alguns pares de palavras, mas para provar a correção para todos os pares possíveis é preciso formal verification. Casos como undefined behavior ou bugs de biblioteca também muitas vezes só aparecem durante o processo de verificação formal
Sobre a menção a “técnicas leves semi-formais como property-based testing, fuzzing e runtime monitoring”, sinto que property-based testing e fuzzing realmente são subconjuntos de métodos formais, mas incluir runtime monitoring como técnica semi-formal talvez seja forçar um pouco
No passado, tive contato com Leslie Lamport por causa do Buridan's Principle e de outros artigos. Hoje aprendi bastante sobre TLA+ e PlusCal no site dele página do exemplo Peterson. Parece totalmente natural que alguém que trouxe matemática para a programação, foi um dos pioneiros em sistemas concorrentes e criou uma linguagem de projeto de sistemas (TLA+) tenha isso sendo usado na AWS e em outros lugares. Gostaria que mais gente que constrói sistemas distribuídos usasse mais as ferramentas criadas pelo Lamport. Em sistemas de larga escala, provar correção é muito importante
Para converter código existente em especificações TLA+, o Claude Opus (Extended Thinking) é bem útil. Já encontrei vários bugs verificando projetos Rust e componentes centrais em C++. Outros modelos frequentemente travam na sintaxe e na lógica da especificação, enquanto o Opus funciona de forma muito mais fluida
Não só em sistemas de larga escala, mas também em utilitários pequenos porém críticos, como SSH e terminais, que são usados no mundo todo, provar correção é extremamente valioso
Sobre a afirmação “provar a correção do sistema”, na prática é impossível provar tudo. O model checker só consegue dizer que, dentro de um espaço de estados limitado, a especificação declarada satisfaz certas propriedades
Pessoalmente, tenho curiosidade se alguém aqui já usou o FIS para experimentos com serviços distribuídos. Estou considerando adotar, mas ainda não tive experiência prática com experimentos em larga escala
Fico curioso se Promela e SPIN são linguagens de nível mais alto do que o que o texto aborda