Quais são os benefícios de segurança de um sistema de tipos?

47

Em JavaScript: The Good Parts, de Douglas Crockford, ele menciona em seu capítulo de herança,

O outro benefício da herança clássica é que ela inclui a especificação de um sistema de tipos. Isso geralmente livra o programador de ter que escrever operações de conversão explícitas, o que é uma coisa muito boa, pois, ao converter, os benefícios de segurança de um sistema de tipos são perdidos.

Então, primeiro de tudo, o que realmente é segurança? proteção contra corrupção de dados, hackers ou mau funcionamento do sistema etc.?

Quais são os benefícios de segurança de um sistema de tipos? O que diferencia um sistema de tipo que permite fornecer esses benefícios de segurança?

type-systems type-safety ErrosWereMade
fonte
Não tenho certeza de que os sistemas de tipos proporcionem qualquer benefício para a linguagem não compilada, mas como usuário de longo prazo das linguagens compiladas, acho que as linguagens compiladas com verificação cuidadosa de tipo são eficazes para impedir que muitos tipos de código ambíguo, indefinido ou incompleto sejam superando o estágio "compilar". Eu acho que você poderia dizer que dicas de tipo e um sistema Lint são valiosos para scripts da Web (JavaScript) e, nesse caso, tenho certeza de que veremos o suficiente. Dardo alguém? Linguagens dinâmicas como Python não parecem piores pela falta de um sistema de tipo estático.
Warren P
1
Hoje entendemos que a digitação deve ser comportamental e não estrutural. Infelizmente, a maioria das linguagens de programação modernas não tem como afirmar o comportamento de um tipo ( veja esta pergunta para uma boa leitura). Isso torna o sistema de tipos bastante inútil na maioria dos casos, especialmente porque os erros de tipo simples que as respostas mencionadas aqui podem ser detectados por um ponteiro inteligente que verifica problemas comuns.
Benjamin Gruenbaum 25/10
4
@BenjaminGruenbaum O que sua descrição já existe em idiomas como OCaml estaticamente. Chama-se tipagem estrutural, na verdade é bastante antiga, a tipagem nominal é mais recente.
jozefg
2
@BenjaminGruenbaum: ... What !? Obviamente, não é indecidível em linguagens de tipo estaticamente, ou então seria impossível escrever um compilador para essas linguagens.
BlueRaja - Danny Pflughoeft 25/10
6
@BenjaminGruenbaum: Seus comentários são valiosos e esse artigo é interessante, mas não confirma a afirmação de que "geralmente é indecidível em linguagens estáticas como Java também", pois demonstra que é decidível em C # e deixa em aberto a questão se é indecidível em Java. (E, de qualquer maneira, IME, quando um compilador para uma linguagem de tipo estaticamente não pode decidir que algo é bem digitado, ele o rejeita (ou falha em compilá-lo); portanto, a indecidibilidade é mais um aborrecimento do que um buraco no tipo. segurança).
ruach

Respostas:

82

Os sistemas de tipos evitam erros

Os sistemas de tipos eliminam programas ilegais. Considere o seguinte código Python.

 a = 'foo'
 b = True
 c = a / b

No Python, este programa falha; isso lança uma exceção. Em uma linguagem como Java, C #, Haskell , qualquer que seja, esse nem é um programa legal. Você evita completamente esses erros porque eles simplesmente não são possíveis no conjunto de programas de entrada.

Da mesma forma, um sistema de tipo melhor exclui mais erros. Se pularmos para sistemas de tipo super avançado, podemos dizer coisas como estas:

 Definition divide x (y : {x : integer | x /= 0}) = x / y

Agora, o sistema de tipos garante que não há erros de divisão por 0.

Que tipo de erros

Aqui está uma breve lista de quais tipos de erros os sistemas podem impedir

  1. Erros fora do intervalo
  2. injeção SQL
  3. Generalizando 2, muitos problemas de segurança (para que serve a verificação de contaminação no Perl )
  4. Erros fora de sequência (esquecendo de chamar init)
  5. Forçando um subconjunto de valores a ser usado (por exemplo, apenas números inteiros maiores que 0)
  6. Gatinhos nefastos (Sim, foi uma piada)
  7. Erros de perda de precisão
  8. Erros de memória transacional de software (STM) (isso requer pureza, o que também exige tipos)
  9. Generalizando 8, controlando efeitos colaterais
  10. Invariantes sobre estruturas de dados (uma árvore binária é equilibrada?)
  11. Esquecendo uma exceção ou lançando a errada

E lembre-se, isso também é em tempo de compilação . Não há necessidade de escrever testes com 100% de cobertura de código para simplesmente verificar erros de tipo, o compilador faz isso por você :)

Estudo de caso: cálculo lambda digitado

Tudo bem, vamos examinar o mais simples de todos os sistemas de tipos, simplesmente digitado cálculo lambda .

Basicamente, existem dois tipos,

Type = Unit | Type -> Type

E todos os termos são variáveis, lambdas ou aplicativo. Com base nisso, podemos provar que qualquer programa bem digitado termina. Nunca há uma situação em que o programa fique preso ou faça um loop para sempre. Isso não é possível no cálculo lambda normal porque, bem, não é verdade.

Pense nisso: podemos usar sistemas de tipos para garantir que nosso programa não fique em loop para sempre, é bem legal, certo?

Desvio para tipos dinâmicos

Os sistemas dinâmicos podem oferecer garantias idênticas aos sistemas estáticos, mas em tempo de execução, em vez de tempo de compilação. Na verdade, como é tempo de execução, você pode oferecer mais informações. No entanto, você perde algumas garantias, principalmente sobre propriedades estáticas, como rescisão.

Portanto, tipos dinâmicos não descartam determinados programas, mas direcionam programas malformados para ações bem definidas, como lançar exceções.

TLDR

Portanto, o longo e o curto são os sistemas de tipos que excluem certos programas. Muitos dos programas são interrompidos de alguma forma, portanto, com sistemas de tipos, evitamos esses programas interrompidos.

jozefg
fonte
25
+1 para compilar como o equivalente a escrever muitos testes.
Dan Neely 24/10
3
@ DanNeely É apenas para ilustrar que, em uma linguagem dinâmica, você precisa exercitar todas as partes do código para detectar os erros que um sistema de tipo verifica gratuitamente. E em uma linguagem de tipo dependente, você pode substituir completamente os testes por tipos. Muitas vezes você precisa provar teoremas adicionais de correção embora
jozefg
3
Se o seu sistema de tipos provou que seu programa deve terminar, é provável que seja feito provando que ele está computando uma função primitiva-recursiva. O que é legal, suponho, mas uma classe de complexidade significativamente menos interessante do que aquela que uma verdadeira máquina de Turing pode resolver. (Isso não significa que os valores intermédios não são grandes; a função de Ackermann é primitivo-recursiva ...)
Donal Fellows
5
@DonalFellows A função Ackermann não é recursiva primitiva, embora seja uma função computável total.
Taymon
4
@sacundim Exatamente, idiomas como o agda permitem a verificação opcional da totalidade e, nos raros casos em que você deseja uma recursão arbitrária, pode pedir com simpatia, é um sistema bastante eficiente.
Jozefg 25/10/2013
17

A própria realidade é digitada. Você não pode adicionar comprimentos a pesos. E embora você possa adicionar pés aos metros (ambos são unidades de comprimento), você deve escalar pelo menos um dos dois. Não fazer isso pode travar sua missão em Marte, literalmente.

Em um sistema typesafe, adicionar dois comprimentos expressos em unidades diferentes teria sido um erro ou teria causado uma conversão automática.

MSalters
fonte
15

Um sistema de tipos ajuda a evitar erros simples de codificação ou permite ao compilador capturar esses erros para você.

Por exemplo, em JavaScript e Python, o problema a seguir geralmente será detectado apenas em tempo de execução - e, dependendo do teste de qualidade / raridade da condição, ele poderá realmente ser produzido:

if (someRareCondition)
     a = 1
else
     a = {1, 2, 3}

// 10 lines below
k = a.length

Enquanto uma linguagem fortemente tipada forçará você a declarar explicitamente que aé uma matriz e não permitirá que você atribua um número inteiro. Dessa forma, não há nenhuma chance de anão ter length- mesmo nos casos mais raros.

Eugene
fonte
5
E um linter inteligente em um IDE como o WebStorm JavaScript pode dizer "Possível referência indefinida a.length para o número a". Isso não nos é dado por ter um sistema de tipos explícito.
Benjamin Gruenbaum 25/10
4
1. Estaticamente, não fortemente 2. @BenjaminGruenbaum Sim, mas isso é feito seguindo um gráfico de tarefas em segundo plano, pense nisso como um mini intérprete tentando descobrir para onde as coisas estão indo. Muito mais difícil do que quando os tipos o oferecem gratuitamente
jozefg 25/10
6
@BenjaminGruenbaum: Não confunda implícito / explícito com forte / fraco. Haskell, por exemplo, tem um sistema de tipos incrivelmente forte que envergonha a maioria das outras linguagens, mas devido a certas decisões de design de linguagem tomadas, ele também é capaz de inferência quase universal de tipos, tornando-a essencialmente uma linguagem tipicamente fortemente implícita, com suporte para digitação explícita. (que você deve usar, porque o tipo inferencer só pode deduzir o que você escreveu, não o que você quis dizer!)
Phoshi
6
“Uma linguagem fortemente tipada forçará você a declarar explicitamente que a é uma matriz” Isso está errado. Python é fortemente tipado e não exige isso. Mesmo os idiomas de tipo estaticamente e fortemente não exigem que, se eles suportam inferência de tipo (e a maioria dos idiomas comuns atualmente, pelo menos em parte).
Konrad Rudolph
1
@BenjaminGruenbaum: Ah, é justo. Mesmo assim, haverá casos em que nenhum analisador estático JS pode executar os mesmos tipos de verificação tipográfica que uma linguagem fortemente tipada forneceria, resolvendo que, no caso geral, é necessário solucionar o problema de parada. Haskell teve que tomar algumas decisões de design para obter quase 100% de inferência de tipo, e C # / Scala não pode inferir tudo. É claro que, nesses casos, não importa, porque você pode especificar explicitamente tipos - em Javascript, isso significa que mesmo o melhor analisador estático não pode mais verificar seu código.
Phoshi
5

Quanto mais cedo você detectar um erro no ciclo de desenvolvimento de software, menos caro será o reparo. Considere um erro que faz com que seu maior cliente ou todos os seus clientes percam dados. Esse erro pode ser o fim da sua empresa se for detectado apenas depois que os clientes reais perderem dados! É claramente mais barato encontrar e corrigir esse bug antes de movê-lo para a produção.

Mesmo para erros menos dispendiosos, mais tempo e energia são gastos se os testadores estiverem envolvidos do que se os programadores puderem encontrar e consertá-lo. É mais barato se não for verificado no controle de origem, onde outros programadores podem criar software que depende dele. A segurança de tipo evita que certas classes de erros sejam compiladas, eliminando quase todo o custo potencial desses erros.

Mas essa não é a história toda. Como qualquer um que programa em uma linguagem dinâmica lhe dirá, algumas vezes é bom se o seu programa apenas compila para que você possa experimentar parte dele sem fazer com que cada pequeno detalhe funcione. Existe uma troca entre segurança e conveniência. Os testes de unidade podem atenuar parte do risco de usar uma linguagem dinâmica, mas escrever e manter bons testes de unidade tem seu próprio custo, que pode ser maior do que o uso de uma linguagem de tipo seguro.

Se você estiver experimentando, se seu código será usado apenas uma vez (como um relatório único), ou se você estiver em uma situação em que não se preocuparia em escrever um teste de unidade, então uma linguagem dinâmica provavelmente é perfeita para voce. Se você tem um aplicativo grande e deseja alterar uma parte sem interromper o restante, digite segurança para salvar a vida. Os tipos de erros que as capturas de segurança são exatamente o tipo de erro que os humanos tendem a ignorar ou cometer erros ao refatorar.

GlenPeterson
fonte
Isso vende digitação dinâmica curta, sem mencionar seus principais benefícios (os mencionados são úteis por relativamente sem importância). Também parece implicar algo estranho nos testes de unidade - sim, eles são difíceis de fazer e têm um custo, e isso se aplica também a linguagens de tipo estaticamente. O que isso está tentando dizer? Ele também falha em mencionar as limitações (por design) dos sistemas de tipos atuais, tanto no que eles podem expressar quanto em quais erros eles podem detectar.
@MattFenwick, quais são os principais benefícios da digitação dinâmica?
GlenPeterson
Os sistemas típicos de tipo estático rejeitam muitos programas bem tipificados por design. ( uma alternativa ) (BTW, minhas críticas foram direcionadas apenas para os parágrafos 3 e 4). #
4

Introdução

A segurança do tipo pode ser alcançada com os idiomas de tipo estático (compilado, verificação estática de tipo) e / ou idiomas de tempo de execução (avaliado, verificação dinâmica de tipo). De acordo com a Wikipedia, um sistema de tipo forte é descrito como aquele em que não há possibilidade de um erro de tipo de tempo de execução não verificado (ed Luca Cardelli). Em outros escritos, a ausência de erros de tempo de execução não verificados é chamada de segurança ou segurança de tipo ... '

Segurança - Verificação de tipo estático

Classicamente, a segurança de tipo é sinônimo de digitação estática, em idiomas como C, C ++ e Haskell, projetados para detectar erros de correspondência de tipo quando são compilados. Isso tem o benefício de evitar condições potencialmente indefinidas ou propensas a erros quando o programa é executado. Isso pode ser inestimável quando existe o risco de que os tipos de ponteiros sejam incompatíveis, por exemplo, uma situação que pode levar a consequências catastróficas se não for detectada. Nesse sentido, a digitação estática é considerada sinônimo de segurança da memória.

A digitação estática não é totalmente segura, mas aumenta a segurança . Mesmo sistemas estaticamente tipificados podem ter consequências catastróficas. Muitos especialistas consideram que o tipo estaticamente pode ser usado para escrever sistemas mais robustos e menos propensos a erros (de missão crítica).

Idiomas de tipo estático podem ajudar a reduzir o risco de perda de dados ou de precisão no trabalho numérico, que pode ocorrer devido à correspondência incorreta ou truncada dos tipos duplo e flutuante de integral ou flutuante.

Há uma vantagem no uso de linguagens de tipo estaticamente para eficiência e velocidade de execução. O tempo de execução é beneficiado por não precisar determinar os tipos durante a execução.

Segurança - Verificação do tipo de tempo de execução

Erlang, por exemplo, é uma linguagem verificada de tipo declarativo e dinamicamente executada em uma máquina virtual. O código Erlang pode ser compilado em bytes. O Erlang é considerado talvez o idioma mais importante, tolerante a falhas e de missão crítica disponível, e é relatado que o Erlang possui uma confiabilidade de nove 9's (99,999999999% ou não mais do que 31,5 msegs por ano).

Certos idiomas, como o Common Lisp, não são estaticamente tipados, mas os tipos podem ser declarados, se desejado, o que pode ajudar a melhorar a velocidade e a eficiência. Também é preciso notar que muitas das linguagens interpretadas mais usadas, como Python, estão, abaixo do loop de avaliação, escritas em linguagens de tipo estatístico, como C ou C ++. O Commom Lisp e o Python são considerados seguros para o tipo pela definição acima.

AsymLabs
fonte
2
Eu me oponho a "fortemente digitado". Você quer dizer digitado estaticamente. Fortemente tipo carrega praticamente nenhum significado, ele é usado para basicamente dizer "eu gosto deste tipo de sistema"
jozefg
@ jozefg Bom ponto. Vou alterar o post.
AsymLabs
3
Também não é útil dizer linguagem interpretada ... sobre uma implementação de linguagem sim, mas não a própria linguagem. Qualquer idioma pode ser interpretado ou compilado. E mesmo após a edição, você está usando os termos digitação forte e fraca.
Esailija 24/10
3
@jozefg: Eu sempre pensei que digitar fortemente significava que cada valor tem um tipo fixo (por exemplo, número inteiro, string, etc.), enquanto que digitar pouco significa que um valor pode ser coagido a um valor de outro tipo, se for considerado conveniente fazer tão. Por exemplo, em Python (fortemente tipado), 1 + "1"lança uma exceção, enquanto que em PHP (tipicamente fraco) 1 + "1"produz 2(string "1"é automaticamente convertida em número inteiro 1).
Giorgio
1
@Giorgio com essa definição, por exemplo, Java não é fortemente tipado. Mas em muitos casos, afirma-se ser. Simplesmente não há significado para essas palavras. Os tipos forte / fraco têm uma definição muito mais precisa como "eu gosto / não gosto dessa linguagem", como diz jozefg.
Esailija 24/10
1

os benefícios de segurança de um sistema de tipo são perdidos.

Então, primeiro de tudo, o que realmente é segurança? proteção contra corrupção de dados, hackers ou mau funcionamento do sistema etc.?

Quais são os benefícios de segurança de um sistema de tipos? O que diferencia um sistema de tipo que permite fornecer esses benefícios de segurança?

Eu sinto que os sistemas de tipos têm uma visão tão negativa. Um sistema de tipos tem mais a ver com garantir do que com provar a ausência de erros. Este último é uma consequência do sistema de tipos. Um sistema de tipos para uma linguagem de programação é uma maneira de produzir, em tempo de compilação, uma prova de que um programa atende a algum tipo de especificação.

O tipo de especificação que se pode codificar como um tipo depende da linguagem, ou mais diretamente, da força do sistema de tipos da linguagem.

O tipo mais básico de especificação é uma garantia sobre o comportamento de entrada / saída de funções e a validade do interior de um corpo de função. Considere um cabeçalho de função

f : (Int,Int) -> String

Um sistema de tipo bom garantirá que f seja aplicado apenas a objetos que produzirão um par de Int ao ser avaliado e garantirá que f sempre produzirá uma string.

Algumas declarações em um idioma, como blocos if-then, não têm um comportamento de entrada / saída; aqui o sistema de tipos garante que cada declaração ou declaração no bloco seja válida; isso aplica operações a objetos do tipo correto. Essas garantias são compostáveis.

Além disso, isso fornece uma espécie de condição de segurança da memória. A citação com a qual você está lidando é sobre elenco. Em alguns casos, a transmissão é boa, como transmitir um Int de 32 bits para um Int de 64 bits. No entanto, geralmente, ele falha no sistema de tipos.

Considerar

Foo x = new Foo(3,4,5,6);
f((Int)x,(Int)x);

Por causa da conversão, x é transformado em um Int; portanto, tecnicamente, o acima mencionado verifica o tipo; no entanto, ele realmente derrota o objetivo da digitação.

Uma coisa que poderia criar um sistema de tipos diferente e melhor é desautorizar os modelos (A) x onde x antes do caso ser do tipo B, a menos que B seja um subtipo (ou subobjeto) de A. As idéias da teoria de subtipagem foram usadas em segurança para remover a possibilidade de ataques de overflow / underflow inteiro.

Sumário

Um sistema de tipos é uma maneira de provar que um programa atende a algum tipo de especificação. Os benefícios que um sistema de tipos pode oferecer dependem da força do sistema de tipos usado.

Jonathan Gallagher
fonte
1

Uma vantagem ainda não mencionada para um sistema de tipos centra-se no fato de que muitos programas são lidos mais do que escritos e, em muitos casos, um sistema de tipos pode permitir que muitas informações sejam especificadas de maneira concisa e fácil. digerido por alguém lendo o código. Embora os tipos de parâmetro não substituam os comentários descritivos, a maioria das pessoas achará mais rápido ler: "int Distance;" ouDistance As Int32do que ler "A distância deve ser um número inteiro +/- 2147483647"; as frações passantes podem produzir resultados inconsistentes. "Além disso, os tipos de parâmetros podem ajudar a reduzir a diferença entre o que uma implementação específica de uma API faz e os que os chamadores podem confiar. Por exemplo, se uma implementação Javascript específica de uma API usar seus parâmetros de uma forma que seria coagir qualquer cordas para forma numérica, pode não ser claro se os chamadores estão autorizados a confiar em tal comportamento, ou se outras implementações do mau funcionamento API poder se dado cordas. Ter um método cujo parâmetro é especificado como DoubleWould deixe claro que qualquer valor de string deve ser coagido pelo chamador antes de ser passado; ter um método com uma sobrecarga que aceite Doublee outro que aceiteString tornaria um pouco mais claro que os chamadores que mantinham cordas teriam permissão para passar por elas como tal.

supercat
fonte
0

Então, primeiro de tudo, o que realmente é segurança? Proteção contra corrupção de dados, hackers ou mau funcionamento do sistema etc.?

Todas as outras respostas e muito mais. Em geral, "segurança de tipo" significa simplesmente que nenhum dos programas que um compilador compila com êxito conterá erros de tipo.

Agora, o que é um erro de tipo? Em princípio, você pode especificar qualquer propriedade indesejável como um erro de tipo, e alguns sistemas de tipos poderão garantir estaticamente que nenhum programa tenha esse erro.

Por "propriedade" acima, quero dizer algum tipo de proposição lógica que se aplica ao seu programa, por exemplo, "todos os índices estão dentro dos limites da matriz". Outros tipos de propriedades incluem "todos os ponteiros diferidos são válidos", "este programa não executa E / S" ou "este programa executa E / S apenas para / dev / null" etc. etc. A propriedade pode ser especificada e o tipo verificado dessa maneira, dependendo da expressividade do seu sistema de tipos.

Os sistemas de tipos dependentes estão entre os sistemas de tipos mais gerais, através dos quais você pode impor praticamente qualquer propriedade que desejar. Porém, não é necessariamente fácil, pois as propriedades sofisticadas estão sujeitas à incompletude, cortesia de Gödel .

naasking
fonte