Verificando o Chromium
Dashboard do Google com ESBMC
Uma prova de conceito reproduzível pela Cyber-Reasoning Consultancy (CRC) aplicando o frontend Python do ESBMC ao chromium-dashboard, o backend em Google App Engine por trás do Chrome Platform Status (chromestatus.com). O ESBMC confirmou dez achados de validação de API; dois foram confirmados e corrigidos no upstream pelos mantenedores do chromium-dashboard no Google nas PR #6451 e PR #6452. Fontes, harness e instruções de execução estão publicados em lucasccordeiro/chromium-dashboard-esbmc.
2 de 10
achados já confirmados e corrigidos no upstream pelo Google (PR #6451, PR #6452)
10
achados de validação de API confirmados por contraexemplos do ESBMC e reprodução
48
alvos de verificação em cinco tiers, em menos de 30 segundos de ponta a ponta
2
invariantes de segurança formalmente provados corretos, com controles de não-vacuidade
Contexto
O chromium-dashboard é o backend em Python que alimenta o Chrome Platform Status: ele gerencia propostas de funcionalidades do Chrome, origin trials, gates de revisão e as decisões de shipping que movem uma funcionalidade da plataforma web ao longo do processo. Sua camada de API HTTP analisa parâmetros de consulta e corpos de requisição fornecidos pelo operador, e um único valor não validado, um milestone igual a zero, um código de estado falsy, um intervalo malformado, pode escapar dos validadores e surgir como um HTTP 500 opaco em vez de um 400 limpo.
Queríamos saber se o frontend Python do ESBMC conseguiria raciocinar sobre essa lógica de validação de entradas diretamente, exaustivamente e em um laptop de desenvolvedor, e transformar uma classe de defeitos do tipo "aceito-e-depois-quebra" em achados que a equipe do Chrome aceitasse e corrigisse, ao mesmo tempo provando formalmente as partes que já são corretas.
Abordagem
O harness fixa o chromium-dashboard no commit
d0d21c8
(2026-05-26) e conduz o frontend Python do ESBMC sobre
48 alvos de verificação em cinco tiers, desde auxiliares aritméticos
puros (is_weekday,
weekdays_between),
passando por caminhos de validação de entrada da API HTTP e contratos booleanos de
self-certify, até invariantes de segurança de revisão/aprovação e aritmética de
milestones. A verificação roda em duas fases, contratos funcionais expressos como
asserções e uma passagem de
--overflow-check
para CWE-190 (overflow com sinal) e CWE-369 (divisão por zero), e a varredura completa
do make verify
é concluída em menos de 30 segundos sem falhas.
Cada defeito candidato é emparelhado com um contraexemplo do ESBMC e uma reprodução empírica contra a API em execução, de modo que um achado só é reportado quando é, ao mesmo tempo, um contraexemplo do solver e uma resposta incorreta observável. A mesma disciplina é aplicada na direção oposta: onde uma propriedade se mantém, o ESBMC é usado para prová-la correta, em vez de apenas não encontrar um bug.
Resultados
Dois achados confirmados e corrigidos no upstream pelo Google. O
mantenedor do chromium-dashboard integrou a
PR #6451
("Give 400 for bad channel range"), resolvendo o Achado A, um
ValueError
não tratado em api/channels_api.py
que retornava HTTP 500 em vez de 400 em um intervalo inválido, e a
PR #6452
("Fix validation of 0 int parameters"), resolvendo o Achado D, um bypass do
validador para valores falsy em api/reviews_api.py
em que um state
igual a 0
escapava da checagem e quebrava com um HTTP 500. Ambas foram integradas em 2026-06-03.
Dez achados de validação de API no total. Além das duas correções,
os achados foram reportados no rastreador público ou mantidos como rascunhos
reproduzíveis: ?num=0
retornando silenciosamente uma página vazia
(#6442),
?start=0/?end=0
retornando datas nulas
(#6443),
e uma chave feature_changes
ausente levantando um KeyError
em um HTTP 500
(#6464),
entre outros. Cada um carrega um contraexemplo do ESBMC e uma requisição que o reproduz.
Dois invariantes de segurança formalmente provados corretos. O
ESBMC provou a integridade da contagem de votos de gate em
internals/approval_defs.py:_calc_gate_state
e a lógica de autorização de voto em
api/reviews_api.py:require_permissions.
Cada prova acompanhou controles deliberadamente bugados que o ESBMC captura,
confirmando que as provas são não-vacuosas, em vez de passarem trivialmente.
Uma correção no ferramental do ESBMC. A PoC revelou um bug no
próprio frontend Python do ESBMC, nondet_bool()
dentro de list comprehensions, corrigido no upstream em
esbmc/esbmc#5023
(integrado em 2026-06-01), com o trabalho de verificação realimentando diretamente
o ferramental open-source que o tornou possível.
O que isso significa
A superfície de validação de entradas HTTP de um serviço web de produção do Google é tratável por bounded model checking com o frontend Python do ESBMC, em velocidade de laptop de desenvolvedor e sem um deployment no circuito. Para equipes que operam ou estendem serviços como o chromium-dashboard, o retorno é duplo: uma classe de bugs de validação do tipo "aceito-e-depois-500" pode ser transformada em verificações rápidas e determinísticas que, como mostram as PR #6451 e PR #6452, os mantenedores estão dispostos a integrar, e as partes que já estão corretas podem ser respaldadas por uma prova formal e não-vacuosa, em vez de uma ausência de falhas de teste.
Referências
- lucasccordeiro/chromium-dashboard-esbmc, repositório público da PoC (harness, testemunhas, alvos em tiers, relatório de achados). github.com/lucasccordeiro/chromium-dashboard-esbmc
- GoogleChrome/chromium-dashboard PR #6451, "Give 400 for bad channel range" (integrada em 2026-06-03); corrige o Achado A. github.com/GoogleChrome/chromium-dashboard/pull/6451
- GoogleChrome/chromium-dashboard PR #6452, "Fix validation of 0 int parameters" (integrada em 2026-06-03); corrige o Achado D. github.com/GoogleChrome/chromium-dashboard/pull/6452
- GoogleChrome/chromium-dashboard issues #6442, #6443 e #6464, outros achados de validação de API reportados no upstream. github.com/GoogleChrome/chromium-dashboard/issues/6464
- ESBMC, verificador limitado de modelos open-source, com o frontend Python usado nesta PoC. github.com/esbmc/esbmc
Nota. Esta página descreve uma prova de conceito independente e reproduzível publicada pelo fundador da CRC e criador e desenvolvedor líder do ESBMC, Prof. Lucas Cordeiro (University of Manchester). A CRC Ltd não mantém parceria comercial com o Google ou o projeto Chromium, e a PoC não foi encomendada por eles; todos os relatos e correções passaram pelo rastreador público de issues e pelas pull requests do chromium-dashboard. O harness é open source; cada achado, testemunha e prova de correção, incluindo as duas correções integradas nas PR #6451 e PR #6452, é reproduzível a partir do repositório público.