Exemplos práticos da Amazon Web Services em correção de sistemas

• A AWS trata a correção de sistemas como uma base essencial para preservar segurança, durabilidade, integridade e disponibilidade, e vem ampliando o escopo de aplicação desde o TLA+ até verificação de modelos, fuzzing, testes baseados em propriedades, verificação em tempo de execução e provas formais
• O TLA+ ajudou a eliminar cedo bugs difíceis de capturar com testes tradicionais e trouxe confiança para otimizações de desempenho, mas, para melhorar a acessibilidade aos desenvolvedores, também foram adotados ferramentas como a linguagem de programação P e o PObserve
• Os testes baseados em propriedades do S3 ShardStore, a simulação determinística e o fuzzing de SQL do Aurora Limitless Database são exemplos de como técnicas formais foram aproximadas do desenvolvimento cotidiano e dos testes de integração
• O Fault Injection Service valida mecanismos de resiliência ao injetar falhas como erros de API, pausas de I/O e falhas de instância, e a Amazon.com executou 733 experimentos com base no FIS na preparação para o Prime Day 2024
• Em áreas em que limites de segurança e otimização de desempenho são críticos, como Cedar, Firecracker e a otimização de RSA no Graviton 2, usam-se provas formais, embora a curva de aprendizado elevada e a acessibilidade das ferramentas ainda limitem a adoção

---

Como a AWS lida com a correção de sistemas

• Para oferecer serviços nos quais os clientes possam confiar, a AWS precisa manter padrões elevados de segurança, durabilidade, integridade e disponibilidade, e a correção de sistemas dá sustentação a isso
• Em 2015, o artigo “How Amazon Web Services Uses Formal Methods”, da CACM, apresentou a abordagem para garantir a correção dos principais serviços da AWS, e desde então esses serviços passaram a ser amplamente usados pelos clientes da AWS
• A principal ferramenta inicial foi a linguagem de especificação formal TLA+, desenvolvida por Leslie Lamport
  • Ela ajudava a encontrar e eliminar, ainda no início do desenvolvimento, bugs sutis que testes tradicionais poderiam deixar passar
  • Também dava confiança para implementar otimizações agressivas de desempenho sem comprometer a correção do sistema
• Há 15 anos, as práticas de teste da AWS dependiam principalmente de testes unitários no momento do build e de testes de integração limitados no momento da implantação
• Desde então, a AWS integrou técnicas formais e semiforais ao processo de desenvolvimento
  • prova de teoremas, verificação dedutiva, verificação de modelos
  • testes baseados em propriedades, fuzzing, monitoramento em tempo de execução

Linguagem de programação P e PObserve

• Ao expandir as técnicas formais para além das equipes iniciais, no começo dos anos 2010, a AWS constatou que muitos engenheiros tinham dificuldade para aprender TLA+ e atingir produtividade
• O ponto forte do TLA+ é ser uma linguagem abstrata de alto nível, próxima da matemática, mas isso também cria uma barreira de entrada para desenvolvedores acostumados com linguagens imperativas
• A linguagem P, baseada em máquinas de estado para modelagem e análise de sistemas distribuídos, surgiu para reduzir esse intervalo
  • Os desenvolvedores modelam o projeto do sistema como máquinas de estado que se comunicam
  • Esse modelo mental é familiar para desenvolvedores da Amazon que trabalham bastante com microsserviços e arquitetura orientada a serviços (SOA)
  • P é desenvolvida na AWS desde 2019 e mantida como um projeto estratégico de código aberto
• Várias equipes de produtos emblemáticos da AWS usam P para revisar a correção do projeto de sistemas
  • armazenamento: Amazon S3, EBS
  • banco de dados: Amazon DynamoDB, MemoryDB, Aurora
  • computação: EC2, IoT
• O S3 usou P na transição de eventual consistency para strong read-after-write consistency
  • O subsistema de índice do S3 é o repositório de metadados de objetos que permite consultas rápidas de dados
  • Para alcançar consistência forte, foram necessárias várias mudanças não triviais na pilha de protocolos de índice do S3
  • P permitiu modelar e verificar formalmente o projeto do protocolo, eliminando cedo bugs de projeto e validando otimizações arriscadas por meio de verificação de modelos
• Em 2023, a equipe de P da AWS criou o PObserve
  • Ele usa logs estruturados gerados pela execução de sistemas distribuídos
  • Faz uma verificação posterior para confirmar se os logs correspondem ao comportamento permitido pela especificação formal em P do sistema
  • Reduz a distância entre implementações de produção escritas em linguagens como Rust ou Java e a especificação em P feita na fase de projeto
  • Ao conectar a verificação em design com o monitoramento em tempo de execução da implementação, aumenta o valor do investimento em especificações formais

Como anexar técnicas formais leves ao fluxo de desenvolvimento

• A AWS adotou técnicas formais leves para aproximar as técnicas formais do fluxo de desenvolvimento e teste das equipes de engenharia

• Testes baseados em propriedades

  • O ShardStore do Amazon S3 usa testes baseados em propriedades ao longo de todo o ciclo de desenvolvimento para testar correção e acelerar o desenvolvimento
  • A equipe combina várias técnicas para que pessoas especifiquem o comportamento esperado, enquanto testes automatizados exploram mais entradas e condições de falha
    • especificações de correção fornecidas por desenvolvedores
    • fuzzing guiado por cobertura, que orienta a distribuição das entradas com métricas de cobertura de código
    • injeção de falhas para simular falhas de hardware e de outros sistemas durante os testes
    • minimização automática de contraexemplos para facilitar o debugging humano

• Simulação determinística

  • Testes com simulação determinística executam sistemas distribuídos em um simulador de thread única e controlam todas as fontes de aleatoriedade
    • agendamento de threads
    • temporização
    • ordem de entrega de mensagens
  • Os desenvolvedores podem escrever cenários específicos de falha e sucesso, como um participante falhando em uma etapa específica de um protocolo distribuído
  • Como o framework de testes controla a não determinismo, é possível especificar ordens de execução interessantes, como a sequência que já disparou um bug no passado
  • O escalonador pode ser expandido com fuzzing de ordens ou exploração de todas as ordens possíveis
  • Ao mover testes de propriedades do sistema sob atraso e falhas para mais perto do momento do build do que dos testes de integração, o desenvolvimento acelera e a cobertura de comportamento aumenta
  • Parte do trabalho da AWS com testes no momento do build para ordem de threads e falhas de sistema foi aberta como código-fonte nos projetos shuttle e turmoil

• Fuzzing contínuo e geração aleatória de entradas de teste

  • O fuzzing contínuo, especialmente a geração escalável de entradas guiada por cobertura, é eficaz para testar a correção de sistemas no momento da integração
  • No desenvolvimento do Aurora Limitless Database, recurso de particionamento de dados do Amazon Aurora, o fuzzing foi usado amplamente para verificar duas propriedades centrais
  • Consultas SQL e transações completas são submetidas a fuzzing para validar se a divisão lógica da execução de SQL entre shards está correta
  • Grandes volumes de esquemas SQL aleatórios, conjuntos de dados e consultas são sintetizados, executados no mecanismo em teste e comparados com um oráculo baseado em um mecanismo sem sharding
  • Outros métodos de verificação, como a abordagem popularizada pelo SQLancer, também são usados em conjunto
  • A combinação de fuzzing com testes de injeção de falhas também é útil para aspectos de correção do banco de dados como atomicidade, consistência e isolamento
    • geração automática de transações
    • definição do comportamento correto com um oráculo de correção formalmente especificado
    • execução, no sistema em teste, de possíveis interleavings entre transações e entre instruções dentro de uma mesma transação
    • verificação posterior de propriedades como isolamento, seguindo abordagens como a Elle

Fault Injection Service e validação sob falhas

• No início de 2021, a AWS lançou o Fault Injection Service (FIS), tornando testes baseados em injeção de falhas disponíveis para diversos clientes da AWS
• O FIS pode injetar falhas simuladas em implantações de teste ou de produção na infraestrutura da AWS
  • erros de API
  • pausas de I/O
  • instâncias com falha
• A injeção de falhas ajuda a confirmar se os mecanismos de resiliência embutidos na arquitetura realmente melhoram a disponibilidade sem criar novos problemas de correção
  • failover
  • health checks
• Os testes de injeção de falhas com FIS são amplamente usados tanto por clientes da AWS quanto internamente na Amazon
• A Amazon.com executou 733 experimentos de injeção de falhas com base no FIS na preparação para o Prime Day 2024
• Em 2014, Yuan e outros analisaram que 92% das falhas fatais em sistemas distribuídos testados foram desencadeadas por tratamento incorreto de erros não fatais
• A razão de falhas fatais no caminho normal serem raras é que esse caminho é executado com frequência, é melhor testado e é muito mais simples do que os caminhos de erro
• Testes de injeção de falhas e o FIS facilitam testar o comportamento do sistema sob falhas e erros, reduzindo a diferença de densidade de bugs entre o caminho normal e os caminhos de erro
• A injeção de falhas em si não é considerada uma técnica formal, mas pode ser combinada com especificações formais
  • o comportamento esperado é definido por uma especificação formal
  • os resultados durante e após a injeção de falhas são comparados com o comportamento especificado
  • isso pode capturar mais bugs do que apenas conferir métricas e erros de log ou depender de inspeção visual humana

Metaestabilidade e comportamento emergente de sistemas

• Nos últimos 10 anos, cresceu o interesse em uma classe específica de falha de sistemas: as falhas metaestáveis (metastable failures)
• Uma falha metaestável ocorre quando um gatilho, como sobrecarga ou esvaziamento de cache, empurra um sistema distribuído para um estado do qual ele não consegue se recuperar sem intervenção
  • um exemplo de intervenção é reduzir a carga para abaixo do normal
• Essa classe de falha é um dos fatores importantes que contribuem para indisponibilidade em sistemas de nuvem
• Em comportamentos metaestáveis típicos, o goodput primeiro cresce com o aumento da carga, depois satura, passa por congestionamento e por fim cai para 0 ou perto de 0
• Depois disso, o sistema não retorna a um estado saudável apenas com uma pequena redução de carga; é necessário reduzir bastante a carga para permitir a recuperação
• Esse comportamento pode aparecer mesmo em sistemas simples e também pode ser disparado, na maioria dos sistemas, por lógica de cliente de timeout seguido de retry
• A modelagem formal tradicional de sistemas distribuídos costuma focar em safety e liveness, mas falhas metaestáveis mostram que há comportamentos que não se encaixam perfeitamente nessa classificação
• Para entender comportamentos emergentes de sistemas, a AWS vem usando mais simulação de eventos discretos
  • investindo em simulações personalizadas de sistemas
  • investindo em ferramentas que permitam usar em simulação modelos de sistemas já feitos em linguagens como TLA+ e P
• Ao estender verificadores de modelos de exploração completa, como o TLC do TLA+, com simulação probabilística, é possível gerar resultados estatísticos, como distribuições de latência observadas depois da execução
• Essas extensões permitem usar verificação de modelos para tarefas como entender a probabilidade de atingir SLAs de latência

Limites de segurança que exigem prova formal

• Em limites de segurança críticos, como autorização e virtualização, as técnicas formais mencionadas até aqui podem não ser suficientes, e provas de correção podem justificar um grande investimento

• Linguagem de políticas de autorização Cedar

  • Em 2023, a AWS introduziu a linguagem de políticas de autorização Cedar para escrever políticas de autorização granular
  • Cedar foi projetada levando em conta raciocínio automatizado e prova formal
  • A implementação foi construída em Dafny, uma linguagem de programação amigável à verificação
  • Com Dafny, foi possível provar que a implementação satisfaz várias propriedades de segurança
  • Trata-se de prova em sentido matemático, indo além de testes
  • A equipe também aplicou testes diferenciais usando o código Dafny como oráculo de correção para validar a implementação em Rust pronta para produção
  • Junto com a implementação do Cedar, a AWS publicou como código aberto o código em Dafny e os procedimentos de teste para que usuários possam verificar o trabalho de correção

• Firecracker VMM

  • O monitor de máquina virtual Firecracker usa um protocolo de baixo nível chamado virtio para expor ao kernel convidado dentro da VM dispositivos de hardware emulados, como placas de rede e SSDs
  • Esses dispositivos emulados representam as interações mais complexas entre o convidado não confiável e o host confiável, sendo portanto um limite de segurança importante
  • A equipe do Firecracker usa o Kani, que permite raciocinar formalmente sobre código Rust, para provar propriedades centrais desse limite de segurança
  • Essa prova garante que propriedades críticas do limite sejam mantidas independentemente do que o convidado tente fazer
  • A AWS apoia o desenvolvimento de ferramentas-base como Kani, Dafny, Lean e os SMT solvers que as sustentam
  • Modelos e especificações formais são reutilizados de várias formas
    • verificação de modelos na fase de projeto
    • papel de oráculo de correção em monitoramento em tempo de execução
    • simulação de comportamento emergente de sistemas
    • construção de provas para propriedades centrais

Desempenho e eficiência de custos além da correção

• Técnicas formais também são importantes para melhorar com segurança o desempenho de sistemas em nuvem
• Ao modelar o protocolo central de commit do mecanismo de banco de dados relacional Aurora com P e TLA+, a equipe encontrou uma oportunidade de reduzir o custo do commit distribuído de 2 idas e voltas de rede para 1,5 ida e volta, sem sacrificar propriedades de safety
• Esse tipo de resultado é comum em equipes que adotam técnicas formais
  • o processo de pensar profundamente sobre protocolos distribuídos e escrevê-los formalmente força um raciocínio estruturado
  • isso traz insights mais profundos sobre a estrutura do protocolo e sobre o problema a ser resolvido
  • quando é possível verificar formalmente ou provar que uma otimização proposta está correta, engenheiros de sistemas distribuídos podem escolher projetos mais ousados sem aumentar o risco
• Ganhos de produtividade e eficiência de custos não se limitam a otimizações de design em alto nível
• Equipes da AWS conseguiram identificar otimizações para a implementação de criptografia de chave pública RSA no processador ARM Graviton 2, aumentando o throughput em até 94%
• A correção dessa otimização foi provada com o provador interativo de teoremas HOL Light
• Como uma alta proporção dos ciclos de CPU em nuvem é consumida por criptografia, esse tipo de otimização pode reduzir custos de infraestrutura, apoiar sustentabilidade e melhorar o desempenho percebido pelos clientes

Desafios restantes e oportunidades futuras

• Embora a AWS tenha ampliado com sucesso métodos de teste formais e semiforais nos últimos 15 anos, a adoção industrial ainda enfrenta desafios
• As principais barreiras das ferramentas de técnicas formais continuam sendo a curva de aprendizado acentuada e a necessidade de conhecimento especializado de domínio
• Muitas ferramentas ainda têm perfil acadêmico e carecem de interfaces amigáveis
• Mesmo abordagens semiforais já bem estabelecidas ainda enfrentam barreiras de adoção
  • simulação determinística é uma técnica central de teste de sistemas distribuídos usada com sucesso na AWS e em projetos como FoundationDB, mas pode ser desconhecida até para desenvolvedores experientes em sistemas distribuídos ao entrarem na AWS
  • lacunas semelhantes existem também em metodologias comprovadas como testes de injeção de falhas, testes baseados em propriedades e fuzzing
• É necessário treinar desenvolvedores de sistemas distribuídos nessas ferramentas e métodos de teste, além de ensinar formas de pensamento rigorosas
• A lacuna educacional começa na academia
  • até abordagens básicas de raciocínio formal raramente são ensinadas
  • mesmo formados em instituições de ponta podem ter dificuldade para adotar essas ferramentas
  • técnicas formais e raciocínio automatizado são importantes para aplicações industriais, mas ainda são vistos como nicho
• Metaestabilidade e outras propriedades emergentes de sistemas em larga escala também são áreas importantes de pesquisa com desafios semelhantes de percepção
  • práticas como “repetir N vezes em caso de timeout”, embora conhecidas por poderem disparar comportamento metaestável, continuam sendo amplamente recomendadas
  • as ferramentas e técnicas atuais para entender comportamento emergente de sistemas ainda estão em estágio inicial
  • modelar a estabilidade de sistemas é caro e complexo
• A AWS acredita que grandes modelos de linguagem e assistentes de IA podem ajudar bastante a reduzir os problemas de adoção prática de técnicas formais
  • assim como testes unitários assistidos por IA ganharam popularidade, essas ferramentas podem ajudar desenvolvedores a criar modelos e especificações formais
  • técnicas avançadas podem se tornar acessíveis para uma comunidade mais ampla de desenvolvedores

A estrutura de correção em que a AWS continua investindo

• Para criar software confiável e seguro, são necessárias várias abordagens para raciocinar sobre a correção de sistemas
• A AWS adota diversas técnicas ao lado de testes padrão da indústria, como testes unitários e de integração
  • verificação de modelos
  • fuzzing
  • testes baseados em propriedades
  • testes de injeção de falhas
  • simulação determinística
  • simulação baseada em eventos
  • verificação em tempo de execução de rastros de execução
• As especificações formais desempenham um papel importante como oráculo de teste, fornecendo a resposta correta em várias práticas de teste da AWS
• Com base no retorno de investimento já obtido, testes de correção e técnicas formais continuam sendo uma área central de investimento para a AWS