Nos últimos anos, a Cloudflare começou a aplicar verificação formal para garantir a precisão no comportamento interno do endereçamento DNS.
Esse comportamento determina qual endereço IP uma consulta DNS recebe ao atingir nosso servidor autoritativo de nomes.
Isso significa que, para qualquer possível consulta DNS de um domínio que usamos como proxy, tentamos provar matematicamente propriedades sobre o comportamento do endereçamento DNS, mesmo quando diferentes sistemas (gerenciados por diferentes equipes na Cloudflare) têm visões contraditórias sobre quais endereços IP devem ser retornados.
Verificação Formal no DNS Autoritativo
Para alcançar essa precisão, verificamos formalmente os programas — escritos em uma linguagem de programação personalizada semelhante ao Lisp — que nossos servidores de nomes executam ao receber uma consulta DNS.
Esses programas determinam os endereços IP a serem retornados. Sempre que um engenheiro faz alterações em um desses programas, todos eles são submetidos ao nosso verificador de modelos personalizado (desenvolvido em Racket + Rosette). O verificador busca por falhas potenciais, como um programa se sobrepondo a outro, antes que as alterações sejam implementadas.
Hoje, nosso verificador formal já opera em produção como parte de um sistema maior chamado Topaz. Na verdade, é provável que você tenha feito uma consulta DNS recentemente que acionou um programa verificado formalmente pelo Topaz.
Este artigo técnico descreve como funciona a verificação formal do Topaz. Além de ser uma ferramenta valiosa para os engenheiros da Cloudflare, o Topaz representa um exemplo real de verificação formal aplicada a sistemas em rede. Esperamos que ele inspire outros operadores de rede a incorporarem métodos formais, quando apropriado, para ajudar a tornar a Internet mais confiável para todos.
Os detalhes técnicos completos do Topaz foram revisados por pares e publicados no ACM SIGCOMM 2024, com um artigo e um vídeo curto disponíveis online.
Quando uma consulta DNS para o domínio de um cliente usando proxy atinge o servidor de nomes da Cloudflare, o servidor retorna um endereço IP. Mas como ele decide qual endereço retornar?
Vamos simplificar. Quando um cliente, como example.com, se inscreve na Cloudflare e configura seu tráfego para ser roteado através de nossa infraestrutura, isso torna nosso servidor de nomes autoritativo para o domínio. Isso significa que temos autoridade para responder às consultas DNS para example.com.
Mais tarde, quando um cliente faz uma consulta DNS para example.com, o resolvedor DNS recursivo do cliente (por exemplo, 1.1.1.1) consulta nosso servidor de nomes para obter a resposta autoritativa. Nosso servidor retorna um endereço IP da Cloudflare para o resolvedor, que o encaminha ao cliente. O cliente, por sua vez, usa esse endereço IP para se conectar à rede da Cloudflare, que é uma rede anycast global — cada data center anuncia todos os nossos endereços.
Quando um cliente faz uma consulta DNS para um domínio hospedado na Cloudflare, o servidor de nomes da Cloudflare responde com um endereço IP pertencente à sua infraestrutura global. Esse endereço IP é utilizado pelo cliente para se conectar ao domínio solicitado. Após essa conexão inicial, a Cloudflare pode encaminhar a solicitação HTTPS para o servidor de origem do cliente, caso necessário.
Para domínios configurados com um endereço IP estático, a escolha é direta: o servidor de nomes simplesmente retorna o endereço IP configurado.
Porém, para domínios sem um endereço IP estático, a Cloudflare possui maior flexibilidade. Nesses casos, o servidor de nomes pode responder com qualquer endereço IP que operamos. Isso significa que:
- O mesmo endereço pode ser retornado para diferentes domínios.
- Endereços diferentes podem ser retornados para consultas distintas do mesmo domínio.
Essa abordagem permite maior resiliência e flexibilidade, uma vez que dissociar nomes de domínio de endereços IP possibilita melhor adaptação às necessidades de negócios.
Para domínios sem IP estático, a escolha do endereço depende de objetivos de negócios específicos da Cloudflare, como:
- Mitigação de ataques: Alterar o endereço IP de um domínio sob ataque para desviar o tráfego malicioso.
- Testes de novas funcionalidades: Direcionar frações do tráfego para IPs específicos.
- Reorganização de endereços: Remapear nomes de domínio para novos blocos de endereços IP.
Como o topaz processa consultas DNS para domínios com proxy
O Topaz é o componente da Cloudflare responsável por lidar com consultas DNS para domínios com proxy. Quando uma consulta é recebida, o Topaz executa uma lista de políticas até encontrar uma correspondência. O endereço IP resultante é então retornado ao servidor de nomes da Cloudflare, que o repassa ao resolvedor DNS do cliente.
Cada programa no Topaz possui três componentes principais:
1. Função de Correspondência (Match Function)
Essa função define quando o programa deve ser executado. Ela:
- Recebe como entrada os metadados da consulta DNS, como:
- Informações do datacenter
- Dados da conta
- Retorna um valor booleano (true ou false).
Se a função retornar true para uma consulta DNS, a função de resposta correspondente será executada.
2. Função de Resposta (Response Function)
Essa função define quais endereços IP serão escolhidos. Ela:
- Também recebe como entrada os mesmos metadados da consulta DNS.
- Retorna uma tupla 3D contendo:
- Endereços IPv4
- Endereços IPv6
- Tempo de vida (TTL – Time to Live) dos IPs.
Quando a função de correspondência retorna true, a função de resposta é executada, e os endereços IP resultantes são enviados ao resolvedor que realizou a consulta.
3. Configuração
A configuração de um programa é um conjunto de variáveis que ajusta o comportamento das funções de correspondência e resposta. Essa separação proporciona:
- Clareza: O comportamento geral do programa (funções de correspondência e resposta) pode ser compreendido sem a necessidade de analisar os detalhes específicos.
- Flexibilidade: Permite alterar rapidamente os detalhes operacionais, como endereços IP e nomes, sem modificar a lógica central do programa.
Por que a estrutura topaz é eficiente?
A separação entre lógica e configuração simplifica a manutenção e escalabilidade dos programas:
- Gerenciamento centralizado: Alterações em configurações não exigem mudanças na lógica do programa.
- Compreensão facilitada: A lógica de negócios (quando e como responder) é distinta das informações específicas (endereços IP, TTL, etc.).
- Automação: Permite respostas dinâmicas às consultas DNS, garantindo flexibilidade e resiliência no gerenciamento de tráfego.
O Topaz é uma solução poderosa que combina automação, clareza e eficiência, permitindo à Cloudflare fornecer respostas DNS otimizadas para atender a uma ampla variedade de objetivos e cenários de negócios.
