Segurança baseada em linguagem - Language-based security

Na ciência da computação , a segurança baseada em linguagem ( LBS ) é um conjunto de técnicas que podem ser usadas para fortalecer a segurança de aplicativos em um alto nível usando as propriedades das linguagens de programação. O LBS é considerado para reforçar a segurança do computador em um nível de aplicativo, tornando possível prevenir vulnerabilidades que a segurança do sistema operacional tradicional é incapaz de lidar.

Os aplicativos de software são normalmente especificados e implementados em certas linguagens de programação e, para proteger contra ataques, falhas e bugs, o código-fonte de um aplicativo pode ser vulnerável, é necessário segurança no nível do aplicativo; segurança avaliando o comportamento dos aplicativos em relação à linguagem de programação. Esta área é geralmente conhecida como segurança baseada no idioma.

Motivação

O uso de grandes sistemas de software, como o SCADA , está ocorrendo em todo o mundo e os sistemas de computador constituem o núcleo de muitas infraestruturas. A sociedade depende muito de infraestrutura, como água, energia, comunicação e transporte, que, novamente, contam com sistemas de computador funcionando de maneira totalmente funcional. Existem vários exemplos bem conhecidos de quando sistemas críticos falham devido a bugs ou erros no software, como quando a falta de memória do computador fez com que os computadores LAX travassem e centenas de voos atrasassem (30 de abril de 2014).

Tradicionalmente, os mecanismos usados ​​para controlar o comportamento correto do software são implementados no nível do sistema operacional. O sistema operacional lida com várias violações de segurança possíveis, como violações de acesso à memória, violações de estouro de pilha, violações de controle de acesso e muitos outros. Esta é uma parte crucial da segurança em sistemas de computador; no entanto, ao proteger o comportamento do software em um nível mais específico, uma segurança ainda mais forte pode ser alcançada. Uma vez que muitas propriedades e comportamento do software são perdidos na compilação, é significativamente mais difícil detectar vulnerabilidades no código de máquina. Ao avaliar o código-fonte, antes da compilação, a teoria e a implementação da linguagem de programação também podem ser consideradas, e mais vulnerabilidades podem ser descobertas.

"Então, por que os desenvolvedores continuam cometendo os mesmos erros? Em vez de confiar nas memórias dos programadores, devemos nos esforçar para produzir ferramentas que codifiquem o que é conhecido sobre vulnerabilidades de segurança comuns e integrem isso diretamente no processo de desenvolvimento."

- D. Evans e D. Larochelle, 2002

Objetivo da segurança baseada em linguagem

Com o uso do LBS, a segurança do software pode ser aumentada em várias áreas, dependendo das técnicas utilizadas. Erros de programação comuns, como permitir que ocorram estouros de buffer e fluxos de informações ilegais, podem ser detectados e proibidos no software usado pelo consumidor. Também é desejável fornecer alguma prova ao consumidor sobre as propriedades de segurança do software, tornando-o capaz de confiar no software sem ter que receber o código-fonte e verificar se há erros.

Um compilador, tomando o código-fonte como entrada, executa várias operações específicas de linguagem no código para traduzi-lo em código legível por máquina. Análise lexical , pré-processamento , análise sintática , análise semântica , geração de código e otimização de código são operações comumente usadas em compiladores. Ao analisar o código-fonte e usar a teoria e implementação da linguagem, o compilador tentará traduzir corretamente o código de alto nível em código de baixo nível, preservando o comportamento do programa.

Ilustrando um compilador de certificação

Durante a compilação de programas escritos em uma linguagem de tipo seguro , como Java , o código-fonte deve verificar o tipo com êxito antes da compilação. Se a verificação de tipo falhar, a compilação não será executada e o código-fonte precisará ser modificado. Isso significa que, dado um compilador correto, qualquer código compilado a partir de um programa-fonte verificado com sucesso deve estar livre de erros de atribuição inválida. Esta é uma informação que pode ser valiosa para o consumidor do código, pois fornece algum grau de garantia de que o programa não travará devido a algum erro específico.

Um objetivo do LBS é garantir a presença de certas propriedades no código-fonte correspondentes à política de segurança do software. As informações coletadas durante a compilação podem ser usadas para criar um certificado que pode ser fornecido ao consumidor como uma prova de segurança no programa fornecido. Tal prova deve implicar que o consumidor pode confiar no compilador utilizado pelo fornecedor e que o certificado, as informações sobre o código-fonte, podem ser verificados.

A figura ilustra como a certificação e a verificação de código de baixo nível podem ser estabelecidas pelo uso de um compilador de certificação. O fornecedor do software ganha a vantagem de não ter que revelar o código-fonte, cabendo ao consumidor a tarefa de verificar o certificado, tarefa fácil se comparada à avaliação e compilação do próprio código-fonte. A verificação do certificado requer apenas uma base de código confiável limitada contendo o compilador e o verificador.

Técnicas

Análise de programa

Artigo principal: Análise do programa

As principais aplicações da análise de programas são a otimização do programa (tempo de execução, requisitos de espaço, consumo de energia, etc.) e a correção do programa (bugs, vulnerabilidades de segurança, etc.). A análise do programa pode ser aplicada à compilação ( análise estática ), tempo de execução ( análise dinâmica ) ou ambos. Na segurança baseada em linguagem, a análise do programa pode fornecer vários recursos úteis, como: verificação de tipo (estática e dinâmica), monitoramento , verificação de contaminação e análise de fluxo de controle .

Análise de fluxo de informação

Artigo principal: Fluxo de informação

A análise do fluxo de informações pode ser descrita como um conjunto de ferramentas utilizadas para analisar o controle do fluxo de informações em um programa, a fim de preservar a confidencialidade e integridade onde os mecanismos regulares de controle de acesso são insuficientes.

"Ao separar o direito de acesso à informação do direito de disseminá-la, o modelo de fluxo vai além do modelo de matriz de acesso em sua capacidade de especificar o fluxo de informações seguro. Um sistema prático precisa de controle de acesso e fluxo para satisfazer todos os requisitos de segurança."

- D. Denning, 1976

O controle de acesso impõe verificações no acesso às informações, mas não se preocupa com o que acontece depois disso. Um exemplo: um sistema tem dois usuários, Alice e Bob. Alice tem um arquivo secret.txt , que só pode ser lido e editado por ela, e ela prefere guardar essa informação para si mesma. No sistema, também existe um arquivo public.txt , que é de leitura e edição gratuita para todos os usuários do sistema. Agora, suponha que Alice tenha feito download acidentalmente de um programa malicioso. Este programa pode acessar o sistema como Alice, ignorando a verificação de controle de acesso em secret.txt . O programa malicioso então copia o conteúdo do secret.txt e o coloca no public.txt , permitindo que Bob e todos os outros usuários o leiam. Isso constitui uma violação da política de confidencialidade pretendida do sistema.

Não interferência

A não interferência é uma propriedade dos programas que não vaza ou revela informações de variáveis ​​com classificação de segurança superior , dependendo da entrada de variáveis ​​com classificação de segurança inferior . Um programa que satisfaça a não interferência deve produzir a mesma saída sempre que a mesma entrada correspondente nas variáveis inferiores for usada. Isso deve ser válido para todos os valores possíveis na entrada. Isso implica que, mesmo que as variáveis mais altas no programa tenham valores diferentes de uma execução para outra, isso não deve ser visível nas variáveis mais baixas .

Um invasor pode tentar executar um programa que não satisfaça a não interferência repetida e sistematicamente para tentar mapear seu comportamento. Várias iterações podem levar à divulgação de variáveis superiores e permitir que o invasor aprenda informações confidenciais sobre, por exemplo, o estado do sistema.

Se um programa satisfaz ou não a não interferência, pode ser avaliado durante a compilação, assumindo a presença de sistemas de tipo de segurança .

Sistema de tipo de segurança

Artigo principal: Sistema de tipo de segurança

Um sistema de tipo de segurança é um tipo de sistema de tipo que pode ser usado por desenvolvedores de software para verificar as propriedades de segurança de seu código. Em uma linguagem com tipos de segurança, os tipos de variáveis ​​e expressões se relacionam à política de segurança do aplicativo, e os programadores podem ser capazes de especificar a política de segurança do aplicativo por meio de declarações de tipo. Os tipos podem ser usados ​​para raciocinar sobre vários tipos de políticas de segurança, incluindo políticas de autorização (como controle de acesso ou recursos) e segurança do fluxo de informações. Os sistemas de tipo de segurança podem ser formalmente relacionados à política de segurança subjacente, e um sistema de tipo de segurança é válido se todos os programas que verificam o tipo satisfazem a política em um sentido semântico. Por exemplo, um sistema de tipo de segurança para o fluxo de informações pode impor a não interferência, o que significa que a verificação de tipo revela se há qualquer violação de confidencialidade ou integridade no programa.

Protegendo código de baixo nível

Vulnerabilidades em código de baixo nível são bugs ou falhas que levarão o programa a um estado em que o comportamento posterior do programa é indefinido pela linguagem de programação de origem. O comportamento do programa de baixo nível dependerá dos detalhes do compilador, do sistema de execução ou do sistema operacional. Isso permite que um invasor leve o programa a um estado indefinido e explore o comportamento do sistema.

Explorações comuns de código inseguro de baixo nível permitem que um invasor execute leituras ou gravações não autorizadas em endereços de memória. Os endereços de memória podem ser aleatórios ou escolhidos pelo invasor.

Usando linguagens seguras

Uma abordagem para obter um código de baixo nível seguro é usar linguagens de alto nível seguras. Uma linguagem segura é considerada completamente definida pelo seu manual do programador. Qualquer bug que possa levar a um comportamento dependente da implementação em uma linguagem segura será detectado em tempo de compilação ou levará a um comportamento de erro bem definido em tempo de execução. Em Java , se acessar um array fora dos limites, uma exceção será lançada. Exemplos de outras linguagens seguras são C # , Haskell e Scala .

Execução defensiva de linguagens inseguras

Durante a compilação de uma linguagem não segura, as verificações de tempo de execução são adicionadas ao código de baixo nível para detectar o comportamento indefinido no nível da fonte. Um exemplo é o uso de canários , que podem encerrar um programa ao descobrir violações de limites. Uma desvantagem de usar verificações de tempo de execução, como na verificação de limites, é que elas impõem uma sobrecarga de desempenho considerável.

A proteção de memória , como o uso de pilha não executável e / ou heap, também pode ser vista como verificações adicionais de tempo de execução. Isso é usado por muitos sistemas operacionais modernos.

Execução isolada de módulos

A ideia geral é identificar o código confidencial dos dados do aplicativo, analisando o código-fonte. Uma vez feito isso, os diferentes dados são separados e colocados em módulos diferentes. Ao assumir que cada módulo tem controle total sobre as informações confidenciais que contém, é possível especificar quando e como deve deixar o módulo. Um exemplo é um módulo criptográfico que pode impedir que as chaves deixem o módulo sem criptografia.

Certificação de compilação

Certificar a compilação é a ideia de produzir um certificado durante a compilação do código-fonte, usando as informações da semântica da linguagem de programação de alto nível. Este certificado deve ser anexado ao código compilado, a fim de fornecer uma forma de prova ao consumidor de que o código-fonte foi compilado de acordo com um determinado conjunto de regras. O certificado pode ser produzido de diferentes maneiras, por exemplo, por meio de código de prova (PCC) ou linguagem de montagem digitada (TAL).

Código de comprovação

Os principais aspectos do PCC podem ser resumidos nas seguintes etapas:

  1. O fornecedor fornece um programa executável com várias anotações produzidas por um compilador de certificação .
  2. O consumidor fornece uma condição de verificação, com base em uma política de segurança . Isso é enviado ao fornecedor.
  3. O fornecedor executa a condição de verificação em um provador de teorema para produzir uma prova para o consumidor de que o programa de fato satisfaz a política de segurança.
  4. O consumidor então executa a prova em um verificador de prova para verificar a validade da prova.

Um exemplo de compilador de certificação é o compilador Touchstone , que fornece uma prova formal PCC de tipo e segurança de memória para programas implementados em Java.

Linguagem assembly digitada

TAL é aplicável a linguagens de programação que fazem uso de um sistema de tipos . Após a compilação, o código-objeto carregará uma anotação de tipo que pode ser verificada por um verificador de tipo comum. A anotação produzida aqui é em muitos aspectos semelhante às anotações fornecidas pelo PCC, com algumas limitações. No entanto, o TAL pode lidar com qualquer política de segurança que possa ser expressa pelas restrições do sistema de tipo, que pode incluir segurança de memória e fluxo de controle, entre outros.

Seminários

Referências

Livros

  • G. Barthe, B. Grégoire, T. Rezk, Compilação de Certificados , 2008
  • Brian Chess e Gary McGraw, Static Analysis for Security , 2004.

Leitura adicional