O que é uma linguagem de programação segura?

54

Linguagens de programação seguras (PL) estão ganhando popularidade. Gostaria de saber qual é a definição formal de PL seguro. Por exemplo, C não é seguro, mas Java é seguro. Suspeito que a propriedade “segura” deva ser aplicada a uma implementação de PL e não ao próprio PL. Nesse caso, vamos discutir uma definição de implementação segura de PL. Minhas próprias tentativas de formalizar essa noção levaram a um resultado estranho, então eu gostaria de ouvir outras opiniões. Por favor, não diga que todo PL possui comandos não seguros. Sempre podemos pegar um subconjunto seguro.

beroal
fonte
Comentários não são para discussão prolongada; esta conversa foi movida para o bate-papo .
Gilles 'SO- stop be evil'
"sempre podemos ter um subconjunto seguro" Como você pode ter certeza de que o idioma resultante ainda está completo em Turing? (que é o que normalmente significa "linguagem de programação")
effeffe
"a propriedade" seguro "deve ser aplicada a uma implementação de PL em vez de ao próprio PL" - você pode chamar um PL de seguro se existir uma implementação segura.
Dmitry Grigoryev

Respostas:

17

Quando chamamos um idioma de "seguro" em algum aspecto , isso significa formalmente que há uma prova de que nenhum programa bem formado no idioma pode fazer algo que consideramos perigoso. A palavra "seguro" também é usada menos formalmente, mas é isso que as pessoas aqui entendem como sua pergunta. Existem muitas definições diferentes de propriedades que queremos que uma linguagem "segura" tenha.

Alguns importantes são:

  • A definição de “sonoridade de tipo” de Andrew Wright e Matthias Felleisen , citada em muitos lugares (incluindo a Wikipedia) como uma definição aceita de “segurança de tipo”, e sua prova de 1994 de que um subconjunto de ML atende a ela.

  • Michael Hicks lista várias definições de "segurança da memória" aqui . Algumas são listas de tipos de erros que não podem ocorrer e outras são baseadas no tratamento de ponteiros como recursos. O Java garante que nenhum desses erros seja possível (a menos que você use explicitamente um recurso marcado unsafe) fazendo com que um coletor de lixo gerencie todas as alocações e desalocações. O Rust faz a mesma garantia (novamente, a menos que você marque explicitamente o código como unsafe), através de seu sistema de tipo afim, que exige que uma variável seja de propriedade ou emprestada antes de ser usada no máximo uma vez.

  • Da mesma forma, o código de thread-safe é geralmente definido como um código que não pode exibir certos tipos de bugs envolvendo threads e memória compartilhada, incluindo raças de dados e deadlocks. Essas propriedades geralmente são aplicadas no nível da linguagem: Rust garante que as corridas de dados não ocorram em seu sistema de tipos, o C ++ garante que seus std::shared_ptrponteiros inteligentes para os mesmos objetos em vários threads não excluam um objeto prematuramente ou falhem em excluí-lo quando a última referência para que seja destruído, C e C ++ adicionalmente possuem atomicvariáveis ​​embutidas na linguagem, com operações atômicas garantidas para impor certos tipos de consistência de memória, se usadas corretamente. O MPI restringe a comunicação entre processos a mensagens explícitas e o OpenMP possui sintaxe para garantir que o acesso a variáveis ​​de diferentes threads seja seguro.

  • A propriedade que a memória nunca vazará é geralmente chamada de espaço seguro. A coleta automática de lixo é um recurso de idioma para garantir isso.

  • Muitos idiomas garantem que suas operações terão resultados bem definidos e que seus programas serão bem-comportados. Como o supercat deu um exemplo acima, C faz isso para aritmética não assinada (garantida a quebra com segurança), mas não aritmética assinada (onde o estouro é permitido para causar erros arbitrários, porque C precisava suportar CPUs que fazem coisas totalmente diferentes quando aritméticas assinadas transborda), mas o idioma algumas vezes converte silenciosamente quantidades não assinadas em quantidades assinadas.

  • As linguagens funcionais têm um grande número de invariantes que qualquer programa bem formado garante, por exemplo, que funções puras não podem causar efeitos colaterais. Estes podem ou não ser descritos como "seguros".

  • Alguns idiomas, como SPARK ou OCaml, foram projetados para facilitar a comprovação da correção do programa. Isso pode ou não ser descrito como "seguro" contra bugs.

  • Prova que um sistema não pode violar um modelo formal de segurança (daí a piada, "Qualquer sistema que seja comprovadamente seguro provavelmente não é".)

Davislor
fonte
11
Isso pode ou não ser descrito como "seguro" contra bugs. Você poderia elaborar um pouco isso? O que você quer dizer com "de bugs"?
Scaaahu 04/07
2
@scaaahu Aqui está um exemplo de site que se refere a software formalmente correto como "comprovadamente seguro". Nesse contexto, refere-se a software para impedir a colisão de aeronaves, o que significa que está protegido contra colisões.
Davislor 04/07/19
11
Estou aceitando esta resposta porque ela lista tipos de segurança. O tipo que eu tinha em mente é a segurança da memória.
beroal 16/07
Enquanto esta resposta lista alguns links úteis e muitos exemplos, a maioria deles está completamente confusa. A coleta de lixo garante que a memória nunca vaze ou não use blocos "inseguros" automaticamente, proporcionando segurança ou estouro assinado, sendo Comportamento indefinido porque os compiladores С precisam suportar algumas CPUs estranhas, sério? E apenas uma breve palavra para Ada / SPARK, que é a única das línguas mencionadas que leva a segurança a sério.
VTT
93

Não existe uma definição formal de "linguagem de programação segura"; é uma noção informal. Em vez disso, os idiomas que alegam fornecer segurança geralmente fornecem uma declaração formal precisa de que tipo de segurança está sendo reivindicada / garantida / fornecida. Por exemplo, o idioma pode fornecer segurança de tipo, segurança de memória ou outra garantia semelhante.

DW
fonte
13
Como um addeumdum, se falarmos de C vs Java como o post do OP: é a segurança da memória garantida em Java e não em C. A segurança de tipo é fornecida por ambos à sua maneira. (Sim, muitas pessoas lendo isso já sabem disso, mas talvez algumas não).
Walfrat 03/07
17
@ Walfrat Faz parte disso. Java também não possui comportamento indefinido, o que é algo que esperamos de uma linguagem que se autodenomina 'segura'. Quanto aos sistemas de tipos, não acho que um sistema de tipos estático forte seja o que as pessoas tendem a dizer com 'seguro'. Linguagens tipicamente dinamizadas como Python geralmente são 'seguras', afinal.
precisa
2
Minha definição de segurança de tipo é a verificação de compilação que trata disso. Essa pode não ser a definição formal. Observe que eu disse "digite segurança", não "seguro". Para mim, a linguagem "segura" refere-se à "minha" definição de "segurança de tipo e memória" e acho que pode ser a mais difundida. Claro que não estou falando de uma armadilha, como ponteiro de reflexão / vazio em C, que a compilação não pode lidar. Outra definição possível de seguro é um programa que não trava com uma falha de segmento, como o ponteiro unitizado em C. Coisas desse tipo geralmente são concedidas em Python e Java.
Walfrat
7
@ Walfrat Tudo o que você recebe é um idioma em que a sintaxe está bem definida. Ele não garante que a execução seja bem definida - e o número de vezes que vi um travamento do JRE, posso dizer claramente que, como sistema, não é "seguro". Em C, por outro lado, o MISRA se esforçou para evitar comportamentos indefinidos para obter um subconjunto mais seguro da linguagem, e a compilação de C no assembler é muito melhor definida. Portanto, depende do que você considera "seguro".
Graham
5
@MaxBarraclough - "Java também não possui comportamento indefinido" - Java não possui comportamento indefinido no sentido usado nas especificações C na definição de linguagem (embora permita que algum código produza valores que não têm um único valor predefinido, por exemplo, acessar uma variável que está sendo modificada em outro encadeamento, ou acessando um doubleou longenquanto está sendo modificado em outro encadeamento, que não garante que não produza metade de um valor misturado de alguma maneira não especificada com metade do outro), mas a especificação da API no entanto, possui comportamento indefinido em alguns casos.
Jules
41

Se você conseguir colocar uma cópia dos Tipos e Linguagens de Programação de Benjamin Pierce , na introdução, ele terá uma boa visão geral sobre várias perspectivas do termo "linguagem segura".

Uma interpretação proposta do termo que você pode achar interessante é:

“Uma linguagem segura é completamente definida pelo manual do programador.” Deixe a definição de uma linguagem ser o conjunto de coisas que o programador precisa entender para prever o comportamento de cada programa na linguagem. Então, o manual para uma linguagem como C não constitui uma definição, pois o comportamento de alguns programas (por exemplo, programas que envolvem acessos não verificados à matriz ou aritmética de ponteiros) não pode ser previsto sem conhecer os detalhes de como um compilador C específico estabelece estruturas na memória , etc., e o mesmo programa pode ter comportamentos bastante diferentes quando executado por compiladores diferentes.

Portanto, eu hesitaria em usar o termo "inseguro" para me referir a uma implementação de linguagem de programação. Se um termo indefinido em um idioma produz um comportamento diferente em diferentes implementações, uma das implementações pode gerar um comportamento mais esperado, mas eu não chamaria de "seguro".

Martin
fonte
7
O Problema da Parada, é claro, diz que, independentemente da linguagem, sempre haverá programas cujo comportamento não é previsível a partir da definição da linguagem. Portanto, qualquer definição que se baseie em "prever o comportamento de todos os programas da linguagem" é fundamentalmente falha para qualquer linguagem completa de Turing.
precisa saber é o seguinte
15
@MSalters Este é um mal-entendido popular sobre o problema da parada. A indecidibilidade do problema de parada implica que é impossível derivar mecanicamente o comportamento de um programa arbitrário em uma linguagem completa de Turing. Mas é possível que para qualquer dado programa, o comportamento é previsível. Só que você não pode criar um programa de computador que faça essa previsão.
Gilles 'SO- stop be evil'
7
@ Giles: Esse não é o caso. Suponha que exista uma prova de não término para cada programa que não termine. Em seguida, você pode enumerar as provas de não término para descobrir se um determinado programa é interrompido. Portanto, o problema da parada é decidível. Contradição. Assim, alguns programas não termináveis ​​não são comprovadamente não termináveis.
Kevin
9
@ Gilles: Estou perfeitamente ciente do fato de que muitos programas são trivialmente parados ou não. Mas a afirmação aqui é literalmente sobre o comportamento de todos os programas. A prova do teorema da parada mostra que existe pelo menos um programa para o qual isso não é verdadeiro. É apenas uma prova não construtiva, não informando qual programa é indecidível.
precisa saber é o seguinte
8
@MSalters Acho que o implícito é que a afirmação é sobre o comportamento em pequena escala do programa, e não em comportamento emergente em larga escala. Por exemplo, considere a conjectura de Collatz . As etapas individuais do algoritmo são simples e bem definidas, mas o comportamento emergente (quantas iterações até parar e, se é que o faz) é tudo menos isso. - "Predict" está sendo usado informalmente aqui. Pode ser melhor escrito como "saber como qualquer declaração em um programa arbitrário será executada".
RM
18

Seguro não é binário, é um continuum .

Informalmente, segurança significa oposição a bugs, sendo os dois mais mencionados:

  • Segurança da memória: o idioma e sua implementação evitam uma variedade de erros relacionados à memória, como acesso após uso livre, duplo-livre, fora dos limites, ...
  • Segurança de tipo: o idioma e sua implementação evitam uma variedade de erros relacionados a tipos, como elencos não verificados, ...

Essas não são as únicas classes de bugs que as linguagens impedem, a liberdade de corrida de dados ou a liberdade de conflito é bastante desejável, as provas de correção são muito boas, etc ...

Porém, programas simplesmente incorretos raramente são considerados "inseguros" (apenas bugs), e o termo segurança é geralmente reservado para garantias que afetam nossa capacidade de raciocinar sobre um programa. Assim, C, C ++ ou Go, com comportamento indefinido, não são seguros.

E, é claro, existem idiomas com subconjuntos inseguros (Java, Rust, ...) que definem propositadamente áreas em que o desenvolvedor é responsável por manter as garantias de idioma e o compilador está no modo "hands-off". As línguas ainda são geralmente ditas seguras , apesar dessa escotilha de escape, uma definição pragmática.

Matthieu M.
fonte
7
Eu diria que é uma treliça.
PatJ 3/07
11
A maioria das implementações de linguagens de programação possui recursos inseguros (por exemplo, Obj.magicno Ocaml). E, na prática, estes são realmente necessários
Basile Starynkevitch
4
@BasileStarynkevitch: De fato. Eu pensaria que qualquer linguagem com FFI necessariamente contém algum nível inseguro, pois chamar uma função C exigirá objetos "pendentes" do GC e garantirá manualmente que as assinaturas dos dois lados correspondam.
Matthieu M.
15

Embora eu não concorde com a resposta da DW, acho que ela deixa uma parte do "seguro" não endereçada.

Como observado, existem vários tipos de segurança promovidos. Eu acredito que é bom entender por que existem várias noções. Cada noção está associada à idéia de que os programas sofrem especialmente com uma determinada classe de erros e que os programadores não seriam capazes de cometer esse tipo específico de erro se a linguagem impedisse o programador de fazê-lo.

Deve-se notar que essas noções diferentes têm, portanto, diferentes classes de bugs, e essas classes não são mutuamente exclusivas nem cobrem todas as formas de bugs. Apenas para pegar os 2 exemplos de DW, a questão de saber se um determinado local de memória contém um determinado objeto é uma questão de segurança de tipo e segurança de memória.

Uma crítica adicional a "linguagens seguras" decorre da observação de que a proibição de certas construções consideradas perigosas deixa o programador com a necessidade de apresentar alternativas. Empiricamente, a segurança é melhor alcançada por boas bibliotecas. o uso de código já testado em campo evita que você cometa novos bugs.

MSalters
fonte
10
É bastante fora de tópico para este site, porque a engenharia de software não é realmente uma ciência, mas eu discordo de sua afirmação empírica. O uso de boas bibliotecas não o salvará em idiomas inseguros, porque você não está protegido contra o uso incorreto. Os idiomas seguros permitem obter mais garantias do autor da biblioteca e obter mais garantias de que você os está usando corretamente.
Gilles 'SO- stop be evil'
3
Estou com MSalters sobre isso. - "Idiomas seguros permitem obter mais garantias do autor da biblioteca e obter mais garantias de que você os está usando corretamente." Esta não é uma sequência para todos os fins práticos.
Captain Giraffe
9

Uma diferença fundamental entre C e Java é que, se evitarmos certos recursos facilmente identificáveis ​​do Java (por exemplo, aqueles no Unsafeespaço de nomes), todas as ações possíveis que se possa tentar - incluindo as "errôneas" - terão um alcance limitado de resultados possíveis . Embora isso limite o que se pode fazer em Java - pelo menos sem usar o Unsafenamespace, também é possível limitar o dano que pode ser causado por um programa incorreto ou, mais importante, por um programa que processaria corretamente arquivos válidos, mas não é particularmente protegido contra arquivos errados.

Tradicionalmente, os compiladores C processavam muitas ações da maneira definida pelo padrão em casos "normais", enquanto processavam muitos casos de canto "de uma maneira característica do ambiente". Se alguém estivesse usando uma CPU que poderia causar um curto-circuito e pegar fogo se ocorresse um excesso numérico e quisesse evitar que a CPU pegasse fogo, seria necessário escrever um código para evitar o excesso numérico. Se, no entanto, alguém estivesse usando uma CPU que truncaria perfeitamente os valores da maneira complemento dois, não seria necessário evitar estouros nos casos em que esse truncamento resultaria em comportamento aceitável.

O C moderno leva as coisas um passo adiante: mesmo que alguém tenha como alvo uma plataforma que naturalmente definiria um comportamento para algo como excesso numérico em que o Padrão não impõe requisitos, o excesso em uma parte do programa pode afetar o comportamento de outras partes do programa de maneira arbitrária, não vinculada às leis do tempo e da causalidade. Por exemplo, considere algo como:

 uint32_t test(uint16_t x)
 {
   if (x < 50000) foo(x);
   return x*x; // Note x will promote to "int" if that type is >16 bits.
 }

Um compilador C "moderno", dado algo como o acima, pode concluir que, como o cálculo de x * x excederia se x for maior que 46340, ele poderá executar a chamada para "foo" incondicionalmente. Observe que, mesmo que seja aceitável que um programa termine de forma anormal se x estiver fora da faixa ou se a função retornar qualquer valor, nesses casos, chamar foo () com uma faixa fora da faixa x pode causar danos muito além qualquer uma dessas possibilidades. O tradicional C não forneceria nenhum equipamento de segurança além do fornecido pelo programador e pela plataforma subjacente, mas permitiria que o equipamento de segurança limite os danos causados ​​por situações inesperadas. O C moderno ignora qualquer equipamento de segurança que não seja 100% eficaz em manter tudo sob controle.

supercat
fonte
3
@ DavidThornley: Talvez o meu exemplo tenha sido muito sutil. Se inttiver 32 bits, xserá promovido a assinado int. A julgar pela lógica, os autores da Norma esperavam que implementações não estranhas tratassem tipos assinados e não assinados de maneira equivalente fora de alguns casos específicos, mas o gcc às vezes "otimiza" de maneiras que quebram se a multiplicar uint16_tpor uint16_tum resultado além de INT_MAX , mesmo quando o resultado estiver sendo usado como um valor não assinado.
Supercat
4
Bom exemplo. Essa é uma das razões pelas quais devemos sempre compilar (no GCC ou no Clang) -Wconversion.
Davislor
2
@ Davidislor: Ah, eu acabei de notar que o godbolt inverteu a ordem em que as versões do compilador estão listadas, portanto, selecionar a última versão do gcc na lista produz a mais recente, e não a mais antiga. Não acho que o aviso seja particularmente útil, pois é propenso a sinalizar muitas situações como as return x+1;que não devem ser problemáticas, e transmitir o resultado para uint32_t sufocaria a mensagem sem corrigir o problema.
Supercat
2
Eliminar testes não faz sentido se o compilador precisar colocar os testes novamente em um local diferente.
user253751
3
@immibis: Uma diretiva "marcada assume" pode permitir que um compilador substitua muitos testes, ou uma verificação que seria realizada várias vezes dentro de um loop, com um único teste que pode ser içado fora de um loop. É melhor do que exigir que os programadores adicionem verificações que não seriam necessárias no código de máquina para que um programa atenda aos requisitos, com o objetivo de garantir que um compilador não "otimize" as verificações necessárias para atender aos requisitos.
Supercat
7

Existem várias camadas de correção em um idioma. Em ordem crescente de abstração:

  • Poucos programas estão livres de erros (somente aqueles cuja correção pode ser comprovada). Outros já mencionaram que a contenção de erros é, portanto, o aspecto de segurança mais concreto. Os idiomas que são executados em uma máquina virtual como Java e .net geralmente são mais seguros nesse aspecto: os erros do programa são normalmente interceptados e tratados de uma maneira definida. 1
  • No próximo nível, erros detectados no tempo de compilação em vez de no tempo de execução tornam um idioma mais seguro. Um programa sintaticamente correto também deve estar semanticamente correto, tanto quanto possível. Obviamente, o compilador não pode conhecer o quadro geral, portanto isso diz respeito ao nível de detalhe. Tipos de dados fortes e expressivos são um aspecto da segurança nesse nível. Pode-se dizer que o idioma deve dificultar alguns tipos de erros(erros de tipo, acesso fora dos limites, variáveis ​​não inicializadas etc.). Informações do tipo em tempo de execução, como matrizes que carregam informações de comprimento, evitam erros. Programei o Ada 83 na faculdade e descobri que um programa Ada compilador normalmente continha talvez uma ordem de magnitude menos erros que o programa C correspondente. Apenas considere a capacidade de Ada de definir tipos inteiros que não são atribuíveis sem conversão explícita: Naves espaciais inteiras caíram porque pés e metros estavam confusos, o que se poderia evitar com Ada.

  • No próximo nível, o idioma deve fornecer meios para evitar o código padrão. Se você precisar escrever seus próprios contêineres, ou sua classificação ou concatenação, ou se precisar escrever seus próprios string::trim()erros, cometerá erros. Como o nível de abstração aumenta, esse critério envolve o idioma apropriado e a biblioteca padrão do idioma.

  • Atualmente, o idioma deve fornecer meios para programação simultânea no nível do idioma. É difícil acertar a simultaneidade e talvez impossível fazer corretamente sem o suporte ao idioma.

  • A linguagem deve fornecer meios para modularização e colaboração. Os tipos fortes, elaborados e definidos pelo usuário acima ajudam a criar APIs expressivas.

De certa forma ortogonalmente, a definição da linguagem deve ser inteligível; a linguagem e as bibliotecas devem estar bem documentadas. Documentação incorreta ou ausente leva a programas ruins e errados.


1 Mas, como geralmente a correção da máquina virtual não pode ser comprovada, essas linguagens podem paradoxalmente não ser adequadas para requisitos de segurança muito rígidos.

Peter - Restabelecer Monica
fonte
11
+1 Para uma explicação clara de camada por camada. Uma pergunta para você: naves espaciais inteiras caíram porque pés e metros estavam confusos, o que se poderia evitar com Ada. , você está falando sobre o Mars Probe Lost devido a um erro de matemática simples ? Você conhece o idioma que eles estavam usando para aquela nave espacial?
Scaaahu
2
@scaaahu Sim, acho que estava me referindo a isso. Não, eu não sei o idioma. Na verdade, lendo o relatório, parece que os dados enviados pela sonda foram processados ​​por um software na Terra, produzindo um arquivo de dados que foi usado para determinar os níveis de empuxo. A digitação de idioma simples não é aplicável neste cenário. Aliás, eles tinham vários problemas com o software de solo e o formato de arquivo de dados, uma confusão que impedia a detecção precoce do problema. Portanto, a história não é um argumento direto para digitação forte, mas ainda é uma história de advertência.
Peter - Restabelece Monica
1

Por favor, não diga que todo PL possui comandos não seguros. Sempre podemos pegar um subconjunto seguro.

Todo idioma que eu conheço tem maneiras de escrever programas ilegais que podem ser (compilados e) executados. E todo idioma que eu conheço tem um subconjunto seguro. Então, qual é a sua pergunta mesmo?


A segurança é multidimensional e subjetiva.

Alguns idiomas têm muitas operações "inseguras". Outros têm menos operações desse tipo. Em alguns idiomas, a maneira padrão de fazer algo é inerentemente insegura. Em outros, a maneira padrão é segura. Em alguns idiomas, há um subconjunto "inseguro" explícito. Em outros idiomas, não existe esse subconjunto.

Em alguns idiomas, "segurança" refere-se exclusivamente à segurança da memória - um serviço oferecido pela biblioteca padrão e / ou o tempo de execução em que as violações do acesso à memória são dificultadas ou impossíveis. Em outros idiomas, "segurança" inclui explicitamente a segurança do thread. Em outros idiomas, "segurança" refere-se à garantia de que um programa não falha (um requisito que inclui não permitir exceções não capturadas de qualquer tipo). Finalmente, em muitos idiomas, "segurança" refere-se à segurança de tipo - se o sistema de tipos for consistente de certas maneiras, é dito que ele é "sólido" (aliás, Java e C # não possuem sistemas de tipos completamente sonoros).

E em alguns idiomas, todos os significados diferentes de "segurança" são considerados subconjuntos do tipo segurança (por exemplo, Rust e Pony atingem a segurança do encadeamento através das propriedades do sistema de tipos).

Theodoros Chatzigiannakis
fonte
-1

Essa resposta é um pouco mais ampla. As palavras segurança e segurança foram mutiladas nas últimas décadas por certas partes politicamente orientadas da sociedade de língua inglesa, de modo que seu uso comum quase não tem definição. No entanto, para assuntos técnicos, ainda volto a definir "segurança" e "seguro" como: um dispositivo que impede o uso não intencional de algo ou que dificulta substancialmente o uso acidental e o estado de estar sob a proteção desse dispositivo .
Portanto, uma linguagem segura possui algum dispositivo para limitar uma classe específica de bugs. É claro que os limites são inconvenientes ou até incapazes em alguns casos, e isso não significa que idiomas "inseguros" resultem em bugs. Por exemplo, não tenho rolhas de segurança nos garfos e, durante décadas, consegui, sem muito esforço, evitar esfaquear meus olhos enquanto comia. Certamente menos esforço do que seria gasto com as rolhas. Portanto, a segurança tem um custo com o qual deve ser julgada. (garfo de cortiça é uma referência a um personagem de Steve Martin)

Poder maximo
fonte