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

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?

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.

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 .

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.

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".

Ferramentas de análise estática como o Coverity podem realmente encontrar HeartBleed e defeitos semelhantes. Divulgação completa: Eu cofundei a Coverity.

Veja meu post sobre nossa investigação do HeartBleed e como nossa análise foi aprimorada para detectá-lo:

http://security.coverity.com/blog/2014/Apr/on-detecting-heartbleed-with-static-analysis.html

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:

• Heartbleed foi um acidente: o desenvolvedor confessa ter causado um erro de codificação e admite que seu efeito é 'claramente grave' "O desenvolvedor alemão Dr. Robin Seggelmann admitiu que escreveu o código, que foi revisado por outros membros e adicionado ao software OpenSSL"

• Como a Codenomicon encontrou o bug heartbleed que agora assola a Internet "O chefe da empresa de segurança explica como a falha foi encontrada, qual a profundidade do risco e o que as pessoas podem fazer agora".

• 3 grandes lições a aprender com Heartbleed "A devastadora vulnerabilidade do OpenSSL prova a importância da orquestração do data center, a sabedoria de executar versões mais antigas e a necessidade de retribuir ao projeto OpenSSL"