Como a Ciência da Computação Teórica se relaciona com a segurança?

Quando penso em software inseguro, acho que é "muito útil" e pode ser abusado por um invasor. Portanto, de certa forma, proteger software é o processo de tornar o software menos útil. Em Ciência da Computação Teórica, você não está trabalhando com o mundo real. Então, existem preocupações de segurança ao trabalhar com a teoria pura? Ou o outro lado da moeda, a Ciência da Computação Teórica afeta o mundo real das pessoas que são hackeadas? Em caso afirmativo, quais tópicos de segurança são considerados teóricos?

Sua intuição de que "insegurança" é devida a software "muito útil" está correta, em certo sentido. Existe uma literatura teórica ampla e crescente sobre "privacidade diferencial" que formaliza sua intuição. Veja, por exemplo, aqui: research.microsoft.com/en-us/projects/databaseprivacy/dwork.pdf

$\epsilon$$e^\epsilon$

$0$

De várias maneiras:

• Criptografia (uma generalização enormemente ampla da segurança da informação que varia da privacidade à criptografia)
• Verificação formal do código (veja também o projeto seL4 )
• Tolerância a falhas e correção de erros
• Formas teóricas de evitar malware ( outro ), incluindo assinatura de código
• Hardware inviolável
• Ocultação de pontos (uma abordagem teórica da informação de obstrução de código teoricamente segura)
• O aprendizado de máquina ajuda a prevenir e alertar as tentativas de invasão em tempo real (pense em Active Wardens e Spam Filtering ).
• Muito muito mais.

Considere o exemplo Wired Equivalent Privacy , que não existe na realidade: devido a falhas teóricas embaraçosamente básicas (pdf), o WEP é decifrado em questão de minutos.

Em "Por que os computadores são inseguros", brincou Bruce Schneier

A engenharia de segurança envolve a programação do computador de Satanás.

E o computador de Satanás é difícil de testar.

Existe muita motivação no mundo real para o estudo de algoritmos de streaming que vêm da detecção de intrusões na rede. O artigo abaixo usa algoritmos de streaming para entropia empírica para detectar anomolias no tráfego da sua rede.

Yu Gu, Andrew McCallum e Don Towsley. Detectando anomalias no tráfego de rede usando estimativa máxima de entropia. Em IMC '05: Anais da 5ª conferência ACM SIGCOMM sobre medição da Internet, páginas 1–6, 2005

Diferentemente das outras respostas, isso é mais parecido com "coisas com as quais devemos nos preocupar ao dizer que algo é 'comprovadamente seguro'", em oposição a lugares onde o TCS foi usado em segurança. Assim, ele aborda a primeira questão de preocupações de segurança ao trabalhar com a teoria.

Como dizem os hackers, os resultados teóricos costumam ser tangenciais à segurança do mundo real. Esse tipo de argumento foi tornado mais teórico, científico e preciso por Alfred Menezes e Neal Koblitz em sua série de artigos ' Another Look ' (aviso: o site parece um pouco conflituoso para mim, mas acho que a idéia básica de questionar suposições) é muito importante). Eles apontam fraquezas em suposições padrão em criptografia, mesmo em artigos seminais.

Alguns exemplos (citando / parafraseando alguns pontos do site):

1. Um teorema da segurança é condicional - assume a intratabilidade de algum problema matemático.

2. Freqüentemente, a suposição de intratabilidade é feita para um problema complicado e artificial: em alguns casos, o problema é trivialmente equivalente ao problema de análise de criptografia do protocolo cuja segurança está sendo "comprovada".

3. Às vezes, uma prova tem uma grande lacuna de estanqueidade, mas os tamanhos dos parâmetros ainda são recomendados como se a prova tivesse sido estanque. Nesses casos, a prova geralmente fornece um limite inferior inútil no tempo de execução de um ataque bem-sucedido. Além disso, um resultado assintótico não fornece necessariamente nenhuma garantia de segurança para parâmetros no intervalo usado na prática.

4. Um teorema de segurança usa um certo modelo de segurança. Certos ataques - especialmente ataques de canal lateral - são muito difíceis de modelar, e os modelos propostos são lamentavelmente inadequados.

Os provadores de teoremas foram utilizados até certo ponto para comprovar a correção de software, hardware e protocolos. Veja, por exemplo, aqui ou aqui .

O problema dos dados fluindo de formas indesejadas através de programas (causando um possível vazamento) foi modelado teoricamente usando a noção de (não) interferência; obtenha dicas aqui .

A decidibilidade é uma preocupação central na pesquisa em linguagem de programação. Ou seja, muito esforço está sendo investido na construção de linguagens de programação que aceitam apenas códigos que satisfazem certas propriedades. Linguagens estáticas típicas apenas fornecem garantias fracas, como rejeitar um programa se certos métodos não existirem, mas imagine se a linguagem também pudesse jogar fora programas que, por exemplo, usam indevidamente mutexes ou tentam ler além do fim das regiões de memória. É claro que os problemas de decisão ocorrem rapidamente (cenário mais simples: especifique que seu compilador deve aceitar apenas programas de encerramento) e, certamente, há preocupações de eficiência (o verificador de tipo ML tem casos duplamente exponenciais).

De qualquer forma, a comunidade de pesquisa do PL está muito interessada em segurança (você confia que seu navegador executa código estrangeiro arbitrário ?!), e suas perguntas levam a muitas questões clássicas da teoria do CS.