Infraestrutura da Internet

Quero reparar um pequeno equívoco, de minha parte. O Fabio Assolin, em mensagem na lista GTS, em novembro de 2008, (aqui), divulgou uma iniciativa da Linha Defensiva¹ relativa à criação de um logo com o texto “Este sáitio é segúrio! Eu agarântio!”, associado à conhecida figura do Sô Cleyson. Algumas pequenas reações vieram em seguida: a, b (minha), c, d, e, f, g e outras. Não estou preocupado em entrar no mérito das respostas, mas sim adicionar um argumento, para assegurar, que o ponto de vista da Linha Defensiva está correto e preciso. Ao mesmo tempo, na medida da disponibilidade de meu tempo irei colocar a figura abaixo e suas variações, nos meus sítios:

Achei que a Linha Defensiva foi pragmática em mudar o logo. Na realidade usou o bom senso e exibiu uma bela noção de objetividade em relação ao resultado desejado.

A abordagem que segue, está disponível em prosa e vastamente, se fizermos uma pesquisa por “teorema da parada”. Uma interessante, clara e didática prosa, em abordagens de segurança, está em Duklin². Em verso, a bela e famosa prova, do Prof. Geoffrey K. Pullum³.

A questão está em uma simples pergunta, portanto: é possível desenvolver um algoritmo (ou programa) que seja capaz de garantir que um sítio é seguro? Mais simples é a resposta: não!^*.

Duklin² é claríssimo e incisivo: Nenhum programa pode dizer (ou explicar) o que um outro programa poderia fazer.

HTML ou qualquer recurso derivado e usado para desenvolver sítios na Web (PHP, ASP, Java, etc.) são linguagens de programação.

Linguagens de programação são sistemas formais. Gödel, por volta de 1932, ao responder a um dos famosos 23 problemas de Hilbert (apresentados em 8 de agosto de 1900, no Congresso Internacional de Matemática em Paris como um desafio para o novo século que estava iniciando), provou que sistemas formais são inconsistentes e incompletos. Por exemplo, a aritmética (ou matemática) é um sistema formal, logo … Na realidade, a prova de Gödel foi sobre a aritmética. Pouco tempo depois, surgiu Turing, com sua famosa Máquina de Turing que fez Alonso Church propor a tese, em linguagem coloquial: um algoritmo é computável se ele for executável em uma Máquina de Turing. Na sequência surgiu, finalmente, o problema da Parada: é possivel executar em uma Máquina de Turing, um programa que receba como entrada um outro programa e suas respectivas entradas? Executar, no sentido de parar, após um tempo finito. A resposta é não^*, como já sabemos.

Com esta abordagem informativa, mas cheia de referências, nas quais o formalismo pode ser levantado, a Linha Defensiva está correta! E, quem estiver pagando para colocar um logo de sítio seguro em suas páginas de Web ou para avaliar sua segurança está, literalmente, caíndo no conto do vigário.

Uma bela, completa e didática descrição sobre o trabalho de Gödel e outros, pode ser vista em [4].

Referências:
[1] Linha Defensiva, Este site é seguro. Não Duvide.
[2] Duklin, P., CAN STRONG AUHENTICATION SORT OUT PHISHING AND FRAUD?, Virus Bulletin Conference, October 2006.
[3] Pullum, G. K., SCOOPING THE LOOP SNOOPER A proof that the Halting Problem is undecidable, School of Philosophy, Psychology and Language Sciences, University of Edinburgh, 2008.
[4] Singh, S., O último teorema de Fermat: a história do enigma que confundiu as maiores mentes do mundo durante 358 anos, Record, 2004.

* No sentido de indecidível.