O verificador de modelos limitado em C: criminalmente subutilizado
Ferramentas de verificação formal como o CBMC, um verificador de modelos limitado para C (e backend do Kani da Amazon para Rust), são elogiadas por detectar bugs sutis como estouros de buffer e erros lógicos ao explorar exaustivamente os caminhos do programa dentro de limites dados. Os comentaristas debatem até que ponto essas ferramentas escalam além de código pequeno, no estilo de testes de unidade, como elas se comparam a alternativas como Frama-C, KLEE e sanitizers, e se o esforço que exigem é preferível a trocar para linguagens mais seguras. A conversa se amplia para problemas de longa data em C — comportamento indefinido, ausência de informação de tamanho de array e garantias fracas de segurança — e se a evolução da linguagem ou ferramentas externas são o caminho mais realista para software de baixo nível mais seguro.
Adoção e Casos de Uso do CBMC
- Vários comentaristas argumentam que o CBMC é subutilizado e defendem trazer a verificação formal no estilo de hardware para o software mainstream.
- Exemplos citados: verificar código criptográfico, bibliotecas C da AWS, componentes do FreeRTOS, funções de clientes HTTP e grandes projetos comerciais em C (~500 mil LOC).
- Alguns usuários relatam ter encontrado bugs reais, como estouros de buffer, loops de negação de serviço e problemas em parsers e código de rede.
Escalabilidade e Estilo de Verificação
- Consenso: o CBMC funciona melhor no nível de unidade ou de pequenos módulos, não em sistemas grandes inteiros.
- O uso eficaz exige:
- Projeto baseado em contratos: pré/pós-condições explícitas e asserções.
- Funções “shadow” que substituem chamadas complexas por modelos simplificados e não determinísticos que respeitam o mesmo contrato.
- Manter a profundidade de busca rasa para que cada execução termine rapidamente.
- Adaptar código legado, mal estruturado, é visto como mais difícil do que usar a ferramenta desde o início.
Comparação com Outras Ferramentas
- Frama-C, Coq VST, a abordagem do seL4: mais poderosas, mas exigem mais expertise e não escalam facilmente para código cotidiano.
- KLEE: bom em ferramentas simples como GNU text/coreutils; tem dificuldade com entradas estruturadas complexas (por exemplo, protobufs, contêineres C++).
- Analisadores estáticos (por exemplo, analisadores do compilador mais anotações) podem cobrir alguns problemas de buffer; o CBMC ainda é valorizado como outra camada de segurança.
- O CBMC também é usado como backend para o Kani, uma ferramenta de verificação de Rust.
Arrays em C, Limites e Design de Linguagem
- Debate estendido sobre a perda do tamanho do array em C quando ele decai para ponteiros e os consequentes bugs de buffer.
- Propostas discutidas: ponteiros gordos/slices, arrays com tamanho sem propriedade, e parâmetros ponteiro-para-array; algumas implementadas em outras linguagens.
- Frustração de que os padrões de C não adotaram esses recursos, enquanto incorporaram outros mais obscuros (por exemplo, identificadores Unicode).
Comportamento Indefinido e Memória Não Inicializada
- O CBMC modela variáveis locais não inicializadas como valores não determinísticos, o que pode divergir da semântica de UB de C.
- Alguns argumentam que um verificador deveria tratar qualquer UB (como ler variáveis não inicializadas) como erro imediato; outros observam que o foco atual do CBMC é modelos “semelhantes a C”, não a semântica exata de C.
- Um longo subthread sobre UB, otimizações de compilador, “C amigável/boring”, sanitizers e comportamento do SO mostra preocupação profunda com miscompilações e bugs de segurança motivados por UB.
- Há consenso de que o CBMC deve ser usado junto com avisos do compilador e sanitizers como parte de uma defesa em profundidade.