Verificando a Configuração do vLLM
com ESBMC
Uma prova de conceito reproduzível pela Cyber-Reasoning Consultancy (CRC) aplicando o frontend Python do ESBMC à aritmética de inteiros e índices do vLLM, o motor de inferência e serving de LLM de alto throughput amplamente implantado. O ESBMC revelou sete defeitos alcançáveis pela CLI; três crashes de divisão por zero foram confirmados e corrigidos upstream pelos mantenedores do vLLM na PR #43794. Fontes, harness e instruções de execução estão publicados em lucasccordeiro/vllm.
PR #43794
Três bugs de crash de CLI no vLLM corrigidos upstream após nosso relatório
7
Descobertas ativas, alcançáveis pela CLI, reveladas ao longo da PoC do vLLM
31
Alvos de verificação em quatro tiers, ~4 min de ponta a ponta
3
Outras lacunas de validação de configuração reportadas upstream e ainda abertas
Contexto
O vLLM é um dos motores open-source mais amplamente usados para servir grandes modelos de linguagem, e sua superfície de configuração é grande: dezenas de flags de linha de comando alimentam diretamente a aritmética de inteiros e índices que dimensiona o cache KV, agenda tokens e organiza blocos de memória. Um único valor fora da faixa, um block size de zero, um threshold negativo, pode escapar do parsing de argumentos e dos validadores e, então, aflorar muito mais tarde como um crash opaco no fundo do motor, onde é difícil atribuir de volta à entrada do operador.
Quisemos saber se o frontend Python do ESBMC conseguia raciocinar diretamente sobre essa aritmética, exaustivamente, em um laptop de desenvolvedor e sem subir uma GPU ou carregar um modelo, e transformar uma classe de defeitos de "lixo-na-entrada, crash-muito-depois" em descobertas que os mantenedores do vLLM aceitariam e corrigiriam.
Abordagem
Modelado em nossa
PoC do AWS Neuron,
o harness fixa o vLLM no commit
4438b6e
e conduz o ESBMC (versão 8.3.0 ou posterior, frontend Python) sobre
31 alvos de verificação em quatro tiers, de verificações focadas em um
único helper de aritmética até alvos que reproduzem um valor ao longo de seu caminho real
da linha de comando até o local do crash. A varredura completa roda de ponta a ponta em
cerca de quatro minutos com zero vereditos inesperados.
Cada defeito candidato é emparelhado com um pequeno programa testemunha em
harness/
que reproduz o contraexemplo do ESBMC e, crucialmente, com um argumento de
alcançabilidade que estabelece se o estado de falha é alcançável a partir de uma invocação
normal de CLI ou apenas de mau uso de API interno. Essa distinção é o que separa um bug
reportável e acionável pelo operador de uma observação de codificação defensiva, e
graduamos cada descoberta com base nela, em vez de reportar vereditos brutos do solver.
Resultados
Três crashes de divisão por zero confirmados e corrigidos upstream pelo vLLM na
PR #43794. --block-size 0
(issue #43496),
--hash-block-size 0
e --max-model-len 0
eram cada um aceitos silenciosamente pelo parsing de argumentos e pelos validadores de
configuração, e então crashavam com um ZeroDivisionError
dentro de cdiv()
durante o dimensionamento do cache KV. A correção integrada rejeita as entradas ruins
em tempo de construção com uma restrição de campo de inteiro positivo (gt=0);
uma quarta descoberta,
--hash-block-size -k,
foi incidentalmente fechada pela mesma restrição.
Outras três lacunas de validação de configuração reportadas upstream e ainda abertas. --num-gpu-blocks-override 0
é aceito, mas falha na init do motor com um
AssertionError nu
em BlockPool.__init__
(issue #43842);
--max-logprobs
e --long-prefill-token-threshold
ambos aceitam silenciosamente valores negativos
(issue #43985).
Cada uma carrega uma testemunha reprodutora e uma restrição de
Field proposta
espelhando a correção da PR #43794.
Escopo honesto, respaldado por provas de alcançabilidade. Dois
candidatos adicionais, um
--block-size
não-potência-de-dois e um
--kv-cache-memory-bytes negativo,
foram investigados e demonstrados não serem bugs ativos, capturados por
guardas existentes antes de qualquer local de crash. Um defeito de
max_num_scheduled_tokens
negativo é real, mas apenas programático, não alcançável pela CLI
(issue #44123),
e uma divisão sem guarda em
get_num_blocks
foi demonstrada inalcançável a partir de invocação normal. Reportamos cada uma destas
como não-descoberta, em vez de inflar a contagem.
Três issues do frontend Python do ESBMC reportadas
(#4926,
#4909,
#4756)
ao longo da PoC, o trabalho de verificação realimentando diretamente o ferramental
open-source que o tornou possível.
O que isso significa
A aritmética de configuração de um motor de inferência de IA de produção é tratável por verificação limitada de modelos com o frontend Python do ESBMC, em velocidades de laptop de desenvolvedor e sem GPU ou modelo no loop. Para equipes que operam ou estendem o vLLM, o ganho é que uma classe de bugs de má configuração do tipo "aceito-e-depois-crasha" pode ser transformada em verificações rápidas e determinísticas, e, como mostra a PR #43794, em correções que o projeto upstream está disposto a integrar.
Referências
- lucasccordeiro/vllm, repositório público da PoC (harness, testemunhas, alvos em tiers, relatório de descobertas). github.com/lucasccordeiro/vllm
- vllm-project/vllm PR #43794, "Validate against some config fields being set to 0" (integrada); corrige os três crashes de divisão por zero. github.com/vllm-project/vllm/pull/43794
-
vllm-project/vllm issue #43496,
--block-size 0ZeroDivisionError (fechada pela PR #43794). github.com/vllm-project/vllm/issues/43496 -
vllm-project/vllm issue #43842,
--num-gpu-blocks-override 0aceito silenciosamente (aberta). github.com/vllm-project/vllm/issues/43842 -
vllm-project/vllm issue #43985,
--max-logprobse--long-prefill-token-thresholdaceitam valores negativos (aberta). github.com/vllm-project/vllm/issues/43985 - 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 projeto vLLM, e a PoC não foi encomendada por ele; todos os relatórios e correções passaram pelo rastreador de issues e pelos pull requests públicos do vLLM. O harness é open source; cada descoberta, testemunha e não-descoberta, incluindo as três correções integradas na PR #43794 e os candidatos demonstrados como não sendo bugs ativos, é reproduzível a partir do repositório público.