As técnicas de verificação de programa poderiam impedir a ocorrência de erros do gênero Heartbleed?

9

Sobre o problema do Heartbleed, Bruce Schneier escreveu em seu Crypto-Gram de 15 de abril: '"Catastrófico" é a palavra certa. Na escala de 1 a 10, esse é um 11. ' Li vários anos atrás que um núcleo de um determinado sistema operacional foi rigorosamente verificado com um sistema de verificação de programa moderno. Poderia, portanto, impedir que erros do gênero Heartbleed ocorram através da aplicação de técnicas de verificação de programas hoje em dia ou isso ainda é irrealista ou mesmo principalmente impossível?

Mok-Kong Shen
fonte
2
Aqui está uma análise interessante desta questão por J. Regehr.
Martin Berger

Respostas:

6

Para responder sua pergunta da maneira mais concisa - sim, esse bug pode ter sido potencialmente detectado por ferramentas formais de verificação. De fato, a propriedade "nunca envia um bloco maior que o tamanho da pulsação enviada" é bastante simples de formalizar na maioria das linguagens de especificação (por exemplo, LTL).

O problema (que é uma crítica comum contra métodos formais) é que as especificações que você usa são escritas por humanos. De fato, os métodos formais apenas mudam o desafio da caça de bugs de encontrar os bugs para definir o que são. Esta é uma tarefa difícil.

Além disso, a verificação formal de software é notoriamente difícil devido ao problema de explosão do estado. Nesse caso, é especialmente relevante, pois muitas vezes, para evitar a explosão do estado, abstraímos os limites. Por exemplo, quando queremos dizer "toda solicitação é seguida por uma concessão, dentro de 100000 etapas", precisamos de uma fórmula muito longa, então a abstraímos para a fórmula "toda solicitação é eventualmente seguida por uma concessão".

Assim, no caso de coração partido, mesmo ao tentar formalizar os requisitos, o limite em questão poderia ter sido abstraído, resultando no mesmo comportamento.

Para resumir, potencialmente esse bug poderia ter sido evitado usando métodos formais, mas teria que haver um humano especificando essa propriedade com antecedência.

Shaull
fonte
5

Os verificadores de programas comerciais como Klocwork ou Coverity podem ter encontrado o Heartbleed, pois é relativamente simples "esquecer de fazer um erro de verificação de limites", que é um dos principais problemas que eles devem verificar. Mas há uma maneira muito mais simples: use tipos de dados abstratos opacos que são bem testados para estarem livres de saturação de buffer.

Há vários tipos de dados abstratos "string segura" disponíveis para programação em C. O que eu estou mais familiarizado é o Vstr . O autor, James Antill, tem uma grande discussão sobre por que você precisa de um tipo de cadeia abstrato de dados com seus próprios construtores / métodos de fábrica e também uma lista de outras cordas tipos de dados abstratos para C .

Lógica Errante
fonte
2
A cobertura não encontra Heartbleed, veja esta análise de John Regehr.
Martin Berger
Belo link! Isso demonstra a verdadeira moral da história: a verificação do programa não pode compensar abstrações mal projetadas (ou inexistentes).
Wandering Logic
2
Depende do que você quer dizer com verificação do programa. Se você quer dizer análise estática, sim, isso é sempre uma aproximação, como uma conseqüência direta do teorema de Rice. Se você verificar o comportamento completo em um processador de teoremas interativo, terá uma garantia de ferro fundido de que o programa atenda às especificações, mas isso é extremamente trabalhoso. E você ainda enfrenta o problema de que suas especificações podem estar erradas (veja, por exemplo, a explosão do Ariane 5).
Martin Berger
11
@MartinBerger: A Coverity encontra agora .
Restabeleça Monica - M. Schröder
4

Se você contar como uma "  técnica de verificação de programa  " a combinação de verificação de limite de tempo de execução e difusão, sim , esse bug em particular poderia ter sido detectado .

Fuzzing adequado fará com que o agora infame memcpy(bp, pl, payload);leia além do limite do bloco de memória plao qual pertence. A verificação de limite de tempo de execução pode, em princípio, capturar qualquer acesso desse tipo e, na prática, nesse caso específico, até mesmo uma versão de depuração mallocque se preocupa em verificar os parâmetros de memcpyteria feito o trabalho (não há necessidade de mexer com a MMU aqui) . O problema é que é necessário realizar testes de difusão em cada tipo de pacote de rede.

fgrieu
fonte
11
Embora sejam verdadeiros em geral, o IIRC, no caso do OpenSSL, os autores implementaram seu próprio gerenciamento de memória interna, de modo que era muito menos provável memcpyque atingissem o verdadeiro limite da região (grande) originalmente solicitada pelo sistema malloc.
William Price
Sim, no caso do OpenSSL, como era no momento do bug, memcpy(bp, pl, payload)teria que verificar os limites usados ​​pela mallocsubstituição do OpenSSL , não o sistema malloc. Isso exclui a verificação automática de limites no nível binário (pelo menos sem um profundo conhecimento da mallocsubstituição). Deve haver recompilação com a magia no nível da fonte usando, por exemplo, macros C substituindo o token mallocou qualquer outra substituição que o OpenSSL tenha usado; e parece que precisamos do mesmo, memcpyexceto com truques MMU muito inteligentes.
precisa saber é
4

O uso de uma linguagem mais restrita não apenas move as postagens de meta, de obter a implementação correta para a especificação correta. É difícil fazer algo que está muito errado, mas consistente logicamente; é por isso que os compiladores capturam tantos bugs.

A aritmética dos ponteiros, como é normalmente formulada, é doentia porque o sistema de tipos não significa realmente o que deveria significar. Você pode evitar esse problema completamente trabalhando em um idioma de coleta de lixo (a abordagem normal que também faz você pagar pela abstração). Ou você pode ser muito mais específico sobre os tipos de ponteiros que está usando, para que o compilador possa rejeitar qualquer coisa que seja inconsistente ou que não consiga se provar correta como está escrita. Essa é a abordagem de alguns idiomas como o Rust.

Tipos construídos são equivalentes a provas; portanto, se você escrever um sistema de tipos que esquece isso, todos os tipos de coisas darão errado. Suponha por um tempo que, quando declaramos um tipo, na verdade queremos dizer que estamos afirmando a verdade sobre o que está na variável.

  • int * x; // Uma afirmação falsa. x existe e não aponta para um int
  • int * y = z; // Verdadeiro apenas se for comprovado que z aponta para um int
  • * (x + 3) = 5; // Verdadeiro apenas se (x + 3) apontar para um int na mesma matriz que x
  • int c = a / b; // Verdadeiro apenas se b for diferente de zero, como: "diferente de zero int b = ...;"
  • nulo int * z = NULL; // nulo int * não é o mesmo que um int *
  • int d = * z; // Uma afirmação falsa, porque z é anulável
  • if (z! = NULL) {int * e = z; } // Ok, porque z não é nulo
  • livre (y); int w = * y; // Declaração falsa, porque y não existe mais em w

Neste mundo, ponteiros não podem ser nulos. As desreferências NullPointer não existem e os ponteiros não precisam ser verificados quanto à nulidade em nenhum lugar. Em vez disso, um "int nulo *" é um tipo diferente que pode ter seu valor extraído para nulo ou para um ponteiro. Isso significa que, no ponto em que a suposição não nula é iniciada, você registra sua exceção ou desativa uma ramificação nula.

Nesse mundo, também não existem erros de matriz fora dos limites. Se o compilador não puder provar que está dentro dos limites, tente reescrever para que o compilador possa provar isso. Se não puder, você terá que inserir manualmente a Assunção nesse local; o compilador pode encontrar uma contradição mais tarde.

Além disso, se você não puder ter um ponteiro que não seja inicializado, não terá ponteiros para a memória não inicializada. Se você tiver um ponteiro para liberar memória, ele deverá ser rejeitado pelo compilador. No Rust, existem diferentes tipos de ponteiros para tornar razoável esse tipo de prova. Existem indicadores de propriedade exclusiva (ou seja, sem aliases), indicadores de estruturas profundamente imutáveis. O tipo de armazenamento padrão é imutável etc.

Há também o problema de impor uma gramática bem definida nos protocolos (que inclui membros da interface), para limitar a área da superfície de entrada exatamente ao que é esperado. A questão da "correção" é: 1) Livre-se de todos os estados indefinidos 2) Garanta consistência lógica . A dificuldade de chegar lá tem muito a ver com o uso de ferramentas extremamente ruins (do ponto de vista da correção).

É exatamente por isso que as duas piores práticas são variáveis ​​globais e gotos. Essas coisas evitam colocar condições pré / pós / invariantes em torno de qualquer coisa. É também por isso que os tipos são tão eficazes. À medida que os tipos se fortalecem (finalmente, usando Tipos Dependentes para levar em consideração o valor real), eles se aproximam de serem provas construtivas de correção; programas inconsistentes falham na compilação.

Lembre-se de que não se trata apenas de erros estúpidos. Também se trata de defender a base de código de infiltradores inteligentes. Haverá casos em que você precisará rejeitar um envio sem uma prova convincente gerada por máquina de propriedades importantes como "segue o protocolo formalmente especificado".

Roubar
fonte
1

a verificação de software formal / automatizada é útil e pode ajudar em alguns casos, mas, como outros já apontaram, não é uma bala de prata. pode-se apontar que o OpenSSL é vulnerável, pois seu código-fonte aberto e ainda utilizado comercialmente e em todo o setor, é amplamente utilizado e não é altamente revisado por pares antes do lançamento (pode-se perguntar se existem desenvolvedores pagos no projeto). o defeito foi descoberto basicamente por meio da revisão de código após o lançamento e o código foi revisado aparentemente antes do lançamento (observe que provavelmente não há como rastrear quem fez a revisão de código interna). o "momento ensinável" com heartbleed (entre muitos outros) é basicamente uma melhor revisão de código, idealmente antes do lançamento esp de código altamente sensível, possivelmente melhor rastreado. talvez o OpenSSL agora esteja sujeito a mais escrutínio.

mais bkg da mídia detalhando suas origens:

vzn
fonte