Dois Bugs no Parser DateTime
do AWS SDK for C++

Contexto

Aws::Utils::DateTime é o tipo de timestamp do AWS SDK for C++, e quase nada que uma aplicação faça com a AWS escapa dele. Prazos de validade de credenciais, timestamps de assinatura de requisição, cabeçalhos Last-Modified do S3 e todo campo com data em toda resposta de serviço passam por um dos seus três parsers: RFC822, ISO-8601 e ISO-8601 Basic. Os três operam sobre bytes que chegaram pela rede.

Cada parser é uma máquina de estados escrita à mão, que percorre a string um caractere por vez. Os campos são acumulados dígito a dígito, valor = valor * 10 + (c - '0'), e a máquina muda de estado ao encontrar um delimitador. Esse formato é compacto e rápido, e tem uma fraqueza característica: o laço é guiado por onde está o delimitador, não pela largura permitida do campo.

Abordagem

Analisamos os parsers com o ESBMC, nosso verificador de modelos de software, usando a mesma técnica que produziu os achados do Base64: em vez de alimentar os parsers com uma lista de strings de timestamp, nós os conduzimos com entrada simbólica e perguntamos ao solver se alguma string até um dado limite poderia alcançar um estouro aritmético ou um resultado silenciosamente errado.

O parsing de timestamps é um bom alvo para isso. As entradas são curtas, o espaço de estados é pequeno, e as propriedades de interesse são exatamente as que um verificador de modelos limitado decide diretamente: um acumulador sai da faixa do seu tipo, e uma conversão produz um valor que quem chama vai ler como válido sem que ele seja.

Resultados

Se você usa o SDK

Atualize para o AWS SDK for C++ 1.11.877 ou posterior. Vale notar que a segunda correção muda um comportamento observável, e não apenas endurece um caminho interno: um timestamp fora da faixa do relógio do sistema agora resulta em parsing inválido, em vez de produzir um valor errado. Se o seu código faz parsing de sentinelas muito distantes no futuro e não verifica WasParseSuccessful(), a atualização vai expor isso, o que é o objetivo, mas convém saber antes da troca de versão, e não depois.

O que isso significa

Os dois defeitos são de naturezas diferentes, e só um deles é do tipo que uma ferramenta de segurança de memória apontaria. A acumulação de dígitos é comportamento indefinido, e um sanitizador poderia capturá-la dada a entrada certa. O bug de conversão não produz travamento nem diagnóstico: a função retorna, a verificação de sucesso de quem chamou passa, e o número errado se propaga. A verificação de modelos limitada trata os dois do mesmo jeito, porque ambos são apenas propriedades a decidir sobre o espaço de entradas, e nenhum depende de alguém ter adivinhado a entrada ao escrever um teste.

É também o segundo trabalho sobre a mesma base de código, e essa é a parte que vale generalizar. Uma vez modelado um decodificador ou um parser, o próximo da mesma biblioteca custa bem menos, e os achados se acumulam. Rotinas pequenas e autocontidas que ficam sobre bytes não confiáveis são onde essa técnica se paga mais rápido.